On Verifying a Query Optimizer: A Correctness Proof for a Real-World Query Rewrite Rule
Bryan Yongbing Feng · 1994
It is generally accepted that rule-based query optimization is a more flexible approach to supporting high-level query languages. However, current practice involves very limited consideration of the issue of rule validity (or correctness). Consequently, the reliability of rule-based query optimization will tend to diminish as both the expressiveness of query languages and complexity of the underlying data models increase. This has motivated members of the Advanced Database Systems Laboratory at our institution to develop a refinement calculus that enables a formal specification of rewrite rules used in current relational and object-oriented optimization technology. This essay reports on an experiment to apply this calculus to capture the intentions underlying a rule used in an optimizer for an experimental object-oriented database system, also developed in our laboratory, and then to attempt proving the validity of this rule. Perhaps most significantly, we learned from this experiment: (1) that our original informal understanding of the intentions underlying the rule was incorrect, and (2) that our first few attempts at a formal specification of this rule were not valid. We believe that this constitutes clear evidence that the issue of rewrite rule valid-ity for existing query optimization technology has now become crucial in achieving essential levels of reliability in database systems. i