-
More and more, new formalisms and verification techniques are expected to be formalized, and meta-properties proved with a proof assistant or similar tool (and made available to the community)
-
General programme: given a programming language and a program logic for that language, we aim to
- Prove soundness and (some notion of) completeness of the logic w.r.t to the programming language semantics
- Write a Verification Conditions Generator for the logic: an algorithm that, given a program and a specification, outputs a set of first-order proof obligations
- Prove soundness and completeness of the VCGen
-
Why3: a sweet spot, in terms of expressivity of logic language, degree of automation, and proof management, for formalizing different notions involved in program verification
-
As a case study, we consider a non-standard version of Hoare logic for While programs, based on the notion of update (a notion which is also used in the JavaDL logic of the KeY tool)
-
Even though the programming language is simple, the formalization of updates is quite intricate!
-
fully automatic proofs of soundness and completeness (in the sense that no goals have to be discharged with the help of an interactive proof assistant -- however, some internal proof trasnformations are required)
-
a proved VCGen
- The VCGen is a WhyML program, so its proofs of soundness and completeness are obtained at program-level, not logic
- It is extractable using Why3’s extraction mechanism, into OCaml
- It produces FOL proof obligations, so it is compatible with the use of SMT solvers
- version 1.2.0 was used for this development
This directory contains:
- hl-upd.mlw: the WhyML file containing all theories and modules
- hl-upd.html: html version generated by why3doc
- why3session.html: Why3 Proof Results for Project "hl-upd"