aalto1 untyped-item.component.html
Formal correctness proof of a mapping from a software specification language to the relational algebra
Loading...
URL
Journal Title
Journal ISSN
Volume Title
School of Science |
Master's thesis
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Authors
Date
Department
Major/Subject
Mcode
Language
en
Pages
66
Series
Abstract
This thesis explores the connection between predicate logic and relational algebra, two foundational pillars of database theory.
We introduce a mapping from logical formulae to relational algebra and prove the semantic equivalence between the two domains. This correspondence creates opportunities for query optimization and enables the use of database queries via a declarative approach, arguably more readable and less error-prone.
The logical formulae introduced are part of our language, which is essentially the predicate logic but without function symbols. On the other hand, the relational algebra formalized in this project is the standard one.
Additional features are also presented in this work. In particular, we extend our language, we formalize a type system for our relations and language – and the correspondence proven between these two domains can also be established under our type system.
While still not widely used, theorem provers are getting increasingly important in computer science where software needs to be reliable. Hence, all results and proofs from this project are rigorously formalized using the Isabelle theorem prover, ensuring that our proofs are free from human error.
Description
Supervisor
Rintanen, JussiOther note
Attachment notes
Description:
The appendix 1 contains the Isabelle theory files for all the formalization done during this master's thesis.
Attachments:
Thesis_Stan_appendix1.zip
Description:
Isabelle Theory Files