Schimbător, Laura-Andrea (2022) Hoare Logics for Skeletal Semantics. Bachelor's Thesis, Computing Science.
|
Text
bCS_2022_SchimbatorLA.pdf Download (333kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
Toestemming.pdf Restricted to Registered users only Download (120kB) |
Abstract
Proving the correctness of programs is essential for programming languages. A widely used approach for proving the partial correctness of programs is Hoare logic, a concrete formal system using axioms and rules. It is sound and complete, and has since been adapted for numerous languages. A drawback of the system is its low modularity, meaning any alteration of the semantics influences the soundness of the Hoare logic. This implies that a separate Hoare logic must be derived and proved for each individual programming language. A modular way for representing programming languages is skeletal semantics. It was introduced as a meta-language for describing languages specified from natural semantics and has been used to derive correct-by-construction interpreters. In this project we provide a comprehensive presentation of Hoare logic and skeletal semantics. We introduce an imperative language While, and prove the soundness property of its skeletal semantics with respect to Hoare logic. Lastly, we make the first step towards a general way to describe correct-by-construction Hoare logic from skeletal semantics by providing a heuristic for mapping skeletons to Hoare logic rules.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Supervisor name: | Frumin, D. and Perez Parra, J.A. |
| Degree programme: | Computing Science |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 20 Jul 2022 06:15 |
| Last Modified: | 20 Jul 2022 06:15 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/28053 |
Actions (login required)
 |
View Item |