Gentle Introduction to Formal Methods
- get started by downloading the Why3 platform and at least one SMT solver,
- first order logic,
- contract based verification and Hoare-logic,
- the Why3 platform and the WhyML language (functional and imperative constructs), and
- Why3 and SMT solvers.
Get Started
If you are interested in running and experimenting with the code examples, please visit:
http://why3.lri.fr/ for general information and
https://www.lri.fr/~marche/MPRI-2-36-1/install.html to install the tools needed under
Ubuntu using the
opam package manager.
First-Order Logic
If you are not familiar with the notion of
first-order logic, no worries, you will get it. You may see it as an extension to propositional logic, including functions over values. You may check wikipedia
https://en.wikipedia.org/wiki/First-order_logic for an overview, but it is quite
hard-core. In the below you will find some examples that help you understand.
Contract Based Verification, and Hoare-logic
To be completed.
The Why3 platform and the WhyML language
To be completed.
Why3 and SMT Solvers
To be completed.
/Per Lindgren, September 2015