Software:Why3

Why3

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 (2009)
Repository	gitlab.inria.fr/why3/why3
Written in	OCaml
Operating system	Cross-platform
Type	Proof assistant Theorem prover
License	LGPLv2.1
Website	why3.lri.fr

Why3 is a software environment for verifying properties of programs. It follows the approach of deductive verification, one of the known technique for formal verification of programs. Why3 is a reference software in education and academic research . 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. The ProofInUse consortium 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 purpose, 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 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 online tool. Many more examples can be found on a Web gallery 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 in 2015, 2016, 2017 and 2021.

The CAV award 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 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 was awarded to Why3 in 2020.

See also

• Formal methods
• Formal specification
• Design by contract
• Formal verification
• Formal proof

External links

• Official website
• online interface for tryning Why3 in your browser
• source repository on the Inria Gitlab