Czy do testowania / weryfikacji SQL można używać relacyjnych dowodów algebry / rachunku różniczkowego?

Czy jest wykonalne lub możliwe jest użycie algebry relacyjnej i / lub rachunku relacyjnego w postaci dowodów do testowania / weryfikacji poprawności instrukcji SQL, funkcji i procedur przechowywanych?

Wydaje mi się, że powinno to być co najmniej możliwe, ale nie wiem, czy brakuje mi jakiegoś szczegółu, który sprawia, że ​​mapowanie 1: 1 między dowodem a kodem jest nieprawidłowe.

Czy ktoś z was próbował takiej metody? Zadziałało? Jakie były twoje doświadczenia?

Istnieje kilka znanych reguł mapowania między relacyjnymi operatorami algebry a instrukcjami SQL. Na przykład operator Sigma odwzorowuje na instrukcję SELECT, istnieje odwzorowanie jeden na jeden dla operatorów łączyć, odwzorowanie Delta na wybór podzbioru kolumn itp.

Czy można użyć algebry relacyjnej do zweryfikowania poprawności instrukcji SQL?

Tak to mozliwe. Oczywiście trzeba mieć przejrzysty schemat bazy danych ze wszystkimi relacjami, kluczami obcymi itp. W niektórych przypadkach łatwiej jest manipulować relacyjnymi instrukcjami algebry niż instrukcjami SQL (istnieją sprawdzone reguły transformacji do modyfikowania i upraszczania instrukcji) .

Ale z drugiej strony nie sądzę, że weryfikacja instrukcji przy użyciu algebry relacyjnej jest znacznie łatwiejsza niż testowanie instrukcji SQL, szczególnie gdy masz bazę danych, w której możesz wykonywać zapytania i wyświetlać wyniki.