核心概念
SQL クエリの等価性を検証するために、有限バッグと有限関係の理論を拡張し、SQL の結合、射影、選択演算をモデル化する。
摘要
本論文では、SQL クエリの等価性を検証するために、以下の取り組みを行っている:
- 有限バッグの理論を拡張し、SQL の結合、射影、選択演算をサポートする。バッグ意味論とセット意味論の両方をサポートする。
- 代数的データ型の理論を拡張して、NULL 値を扱えるようにする。
- これらの新しい理論をcvc5 SMTソルバーに実装し、SQL クエリの等価性問題などを自動的に解析できるようにする。
- 集計関数のサポートは今後の課題としている。
本手法は、SQLSolverやSPESなどの既存ツールと比べて、以下の利点がある:
- SQL等価性問題以外にも適用可能
- 豊富な背景理論を持つcvc5 SMTソルバーに統合されている
- セットとバッグの混在するSQL クエリの解析にも対応可能