Можно ли использовать доказательства реляционной алгебры / исчисления для проверки / проверки SQL?

9

Возможно ли или даже возможно использовать реляционную алгебру и / или реляционное исчисление в форме доказательств для проверки / проверки правильности операторов, функций и хранимых процедур SQL?

Мне кажется, что это должно быть по крайней мере возможно, но я не знаю, есть ли какая-то деталь, которую я упускаю, которая делает соотношение 1: 1 между доказательством и кодом неверным.

Кто-нибудь из вас пробовал такой метод? Это сработало? Каким был ваш опыт?

Роберт Уинслоу Дальпе
источник
2
Пожалуйста, повторите за мной: SQL не реляционный.
Охотник на оленей

Ответы:

4

Существует несколько известных правил отображения между операторами реляционной алгебры и операторами SQL. Например, оператор Sigma сопоставляется с оператором SELECT, есть взаимно-однозначное сопоставление для операторов соединения, Delta сопоставляется с выбором подмножества столбцов и т. Д.

Можно ли использовать реляционную алгебру для проверки правильности операторов SQL?

Да, это возможно. Конечно, вам нужно иметь четкую схему базы данных со всеми связями, внешними ключами и т. Д. В некоторых случаях манипулировать операторами реляционной алгебры даже проще, чем операторами SQL (существуют проверенные правила преобразования для изменения и упрощения операторов) ,

Но, с другой стороны, я не думаю, что проверка операторов с использованием реляционной алгебры намного проще, чем проверка операторов SQL, особенно когда у вас есть готовая база данных, где вы можете выполнять запросы и просматривать результаты.

superM
источник
1
Просто хотел сказать: реляционные операторы отображаются в «SELECT DISTINCT», поскольку реляционная алгебра использует наборы кортежей и поэтому не может обрабатывать дубликаты. Сама сигма соответствует предложению WHERE, пи - SELECT и так далее.
противоречил
Операторы соединения не являются 1: 1, версии SQL обрабатывают нули специально, и аналогично предикаты не являются логическими.
Philipxy