Why3
 | This article may be too technical for most readers to understand. Please help improve it to make it understandable to non-experts, without removing the technical details. (November 2023) (Learn how and when to remove this template message) |
| File:Logo-why3.png | |
| Original author(s) | F. Bobot, J.-C. Filliâtre, G. Melquiond, C. Marché, A. Paskevich |
|---|---|
| Developer(s) | Inria, CNRS, Paris-Saclay University |
| Initial release | 2009 |
| Repository | gitlab |
| Written in | OCaml |
| Engine | |
| Operating system | Cross-platform |
| Type | Proof assistant Theorem prover |
| License | LGPLv2.1 |
| Website | why3 |
Search Why3 on Amazon.
Why3 is a software environment for verifying properties of programs. It follows the approach of deductive verification, one of the known techniques for formal verification of programs. Why3 is a reference software in education[1] and academic research[2] [3] [4]. Why3 is also used in industry, for the verification of critical software: it is for example used by the Frama-C environment for verification of C and C++ software, by the SPARK environment for verification of Ada programs, the verification of Ladder charts for Programmable Logic Controllers[5]. The ProofInUse consortium[6] is a laboratory for research and development, joint with academic developers of Why3 and a few private companies, sharing the use of Why3 in their products.
Overview
Why3 is a standalone software which takes as input a computer program annotated with a formal specification under the form of logical assertions: preconditions, postconditions, loop invariants, etc. From a program equipped with its formal specification, Why3 computes verification conditions: mathematical formulas to be proved valid. Why3 is able to send these conditions to a large set of automated reasoning tools, including the automatic theorem provers Alt-Ergo, CVC4, cvc5, Z3, E prover, and the proof assistants Coq, Isabelle/HOL. Why3 can be used on the command line, or through a GTK graphical interface, or a web interface. Moreover, Why3 can be used as a library for the OCaml language, with an API for constructing and manipulating the abstract syntax of logical formulas and programs, to calculate verification conditions, to send logical statements to provers, to store and replay proof sessions, etc. Finally, it is also possible to see Why3 as a development tool. It indeed offers a programming language (WhyML) adapted to program proofs and an automatic translation from this language to the OCaml and C languages. For teaching purposes, Why3 also offers front-ends for verification of programs and C and Python, supporting a reduced fragment of these languages.
The underlying logical framework is typed first-order logic, extended with some flavour of purely functional programming constructions for defining theories with new logic data-types, functions and predicates. The underlying programming language WhyML is a ML-style functional language with some flavour of imperative programming: mutable variables, while loops, exceptions raising and catching. Programs in WhyML must conform to a specific region-based typing system[7] [8] meaning that the set of mutable variables modified by an arbitrary program expression is statically known. This typing constraint allows the verification condition generator to produce formulas following the general frameworks of Hoare logic, Weakest Preconditions and Strongest Postconditions.
Examples
Two short examples below present the main line of usage of Why3. A few introductory examples are available in the Try Why3[9] online tool. Many more examples can be found on a Web gallery[10] of programs verified using Why3.
Checking validity of a logic formula
In this example a WhyML text is introduced to formally describe the famous Syllogism deducing that Socrates is mortal:
(** declaration of a type name *)
type being
(** declaration of two predicates on `being` *)
predicate is_human being
predicate is_mortal being
(** introducing an inhabitant of `being` *)
constant socrates: being
(** a first assumption *)
axiom socrates_is_human: is_human socrates
(** a second, quantified assumption *)
axiom all_humans_are_mortal:
forall x:being. is_human x -> is_mortal x
(** a logic goal to prove *)
goal socrates_is_mortal: is_mortal socrates
Running Why3 on the command line, invoking the Z3 prover, gives the following:
> why3 prove -P Z3 socrates.mlw Goal socrates_is_mortal. Prover result is: Valid (0.01s, 446 steps).
It means that the invocation of Z3 indeed confirmed that the logical deduction is correct.
Proving a program
The following WhyML short file introduces the computation of the maximal element of an array of integers. The formal specification states this expected behavior:
use int.Int
use array.Array
(** `max_array a` returns the maximal value appearing in the array `a` *)
let max_array (a: array int) : int
(** the input array must be non-empty to have a maximal element *)
requires { a.length >= 1 }
(** the return value is larger than all values in `a` *)
ensures { forall k. 0 <= k < a.length -> result >= a[k] }
(** the return value is one of the values in `a` *)
ensures { exists k. 0 <= k < a.length /\ result = a[k] }
= let ref m = a[0] in
let ghost ref im = 0 in (** ghost variable holding the index of the current maximum *)
for i=1 to a.length - 1 do
invariant { forall k. 0 <= k < i -> m >= a[k] }
invariant { 0 <= im < i /\ m = a[im] }
if a[i] > m then (m <- a[i]; im <- i)
done;
m
Running Why3 using the Alt-Ergo prover results in the following
why3 prove -P Alt-Ergo max_array.mlw Goal max_array'vc. Prover result is: Valid (0.02s, 90 steps).
Awards
Teams using Why3 won several prizes at the VerifyThis competition[11] in 2015, 2016, 2017 and 2021.
The CAV award[12] 2019 has been awarded to J.-C. Filliâtre for the initial design and development of Why3 (jointly with R. Leino, awarded for the Dafny tool).
The FIEEC Carnot prize[13] was awarded in 2019 to C. Marché in recognition of the success of ProofInUse joint laboratory.
The Systematic Open Source Hub's coup de cœur prize[14] was awarded to Why3 in 2020.
See also
References
- ↑ Blazy, Sandrine (2019). Teaching Deductive Verification in Why3 to Undergraduate Students. Formal Methods Teaching. pp. 52–66. doi:10.1007/978-3-030-32441-4_4.
- ↑ Filliâtre, Jean-Christophe; Paskevich, Andrei (2013). Why3: where programs meet provers. 22nd European Symposium on Programming. pp. 125–128. doi:10.1007/978-3-642-37036-6_8.
- ↑ Bobot, François; Filliâtre, Jean-Christophe; Marché, Claude; Paskevich, Andrei (2015). "Let's verify this with Why3". International Journal on Software Tools for Technology Transfer. 17 (6): 709–727. doi:10.1007/s10009-014-0314-5. Unknown parameter
|s2cid=ignored (help) - ↑ Melquiond, Guillaume; Rieu-Helft, Raphaël (2020). WhyMP, a formally verified arbitrary-precision integer library. 45th International Symposium on Symbolic and Algebraic Computation. pp. 352–359. doi:10.1145/3373207.3404029.
- ↑ Belo Lourenço, Cláudio; Cousineau, Denis; Faissole, Florian; Marché, Claude; Mentré, David (2022). "Automated Formal Analysis of Temporal Properties of Ladder Programs". International Journal on Software Tools for Technology Transfer. 24 (6): 977–997. doi:10.1007/s10009-022-00680-0. Unknown parameter
|s2cid=ignored (help) - ↑ The ProofInUse consortium and joint laboratory
- ↑ Filliâtre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei (2014). The spirit of ghost code. 26th International Conference on Computer Aided Verification. Lecture Notes in Computer Science. 8859. pp. 1–16. doi:10.1007/s10703-016-0243-x.
- ↑ Filliâtre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei (2016). A pragmatic type system for deductive verification (Report). Université Paris Sud.
- ↑ Try Why3 in your browser
- ↑ Web gallery of verified programs
- ↑ VerifyThis competition
- ↑ List of CAV Awards
- ↑ FIEEC Carnot 2019 prizes for applied research (in French)
- ↑ Systematic Open Source Hub's coup de cœur prize (in French)
External links
- Official website
- online interface for trying Why3 in your browser
- source repository on the Inria Gitlab
This article "Why3" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Why3. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.
