Métodos Formais em Engenharia de Software

Mestrado em Engenharia Informática

Why3 — Logic

The Why3 Platform

Why3 is targeted at deductive formal verification of algorithms and programs.

The most important conceptual components of the platform are the following:

The Why3 tool implements the following functionality:

Note

Previously in this course the Alloy tool was also used for formal verification. However, in Alloy the word verification is used as a synonym for model checking (algorithmic state space exploration), whereas in Why3 it is based on actual deductive proofs. Moreover, Alloy targets systems specified at an abstract level, whereas Why3 is used to verify algorithms

Why3 as a Proof Tool

Although this was probably not the original intention, Why3 has become popular as a proof tool on its own (its logic functionality is also accessible through an API).

This is due to the extremely convenient interfacing with external proof tools, and also to the features of the logic language, which extends standard FOL with a set of features that are highly convenient for applications in computer science.

The logic language includes:

It is possible, for instance, to define a type of binary trees and then define a recursive predicate stating when such a tree is a binary search tree (i.e. it is sorted inorder).

Example: Class Assignment (from Ficha 1)

Recall the assignment:

In a training course there are 5 consecutive classes and 3 teachers (Ana, Beatriz and Carlos), all capable of teaching any class. We want to allocate the teachers to different classes, subject to the following restrictions:

The following is an encoding of this problem in the Why3 logic. The example illustrates:

[Try this example online here]

Unlike an SMT solver, Why3 works with validity rather than satisfiability. The above module contains two goals; Why3 will generate a proof obligation for each one of them, that will be encoded and dispatched to an external proof tool.

Proving that a goal follows from the axioms is a consequence problem; it will be encoded as a satisfiability problem if it is dispatched to an SMT solver.

**goal** g : teaches Beatriz ClassFive -> teaches Ana ClassOne states that it follows from the axioms that if Beatriz teaches ClassFive then it must be the case that Ana teaches ClassOne.

Why3 includes a number of automated strategies that will attempt to prove goals by performing simple proof transformations (such as splitting goals into smaller formulas) and sending the resulting proof obligations in turn to several SMT solvers, if more than one is available.

The line **goal** SAT : false may seem strange; its purpose is to try to establish that there exists at least one model for the theory defined by the previous axioms — if solvers fail to prove the goal and find a counterexample for it, then the theory is not inconsistent.

When solvers find them, Why3 allows for counter-examples to be displayed. In the above example, for instance the Z3 solver will find a counter-example, which corresponds to a model, i.e. an actual assignment of teachers to classes.

Underneath, what Z3 is doing is exactly what we did manually in a previous class, when we solved this puzzle by interacting with Z3 via its Python API.

The online version of Why3 contains a single SMT solver (Alt-Ergo). It allows the user to split goals and increase the time limit allowed to the solver for each goal. This web version does not allow for counter-examples to be inspected.

Example: Class Assignment — alternative encoding

Let us give a second encoding of the same puzzle to illustrate the use of logic functions and of a library theory for sets.

The idea is that the function teachers associates to each class the set of teachers assigned to teach it; the axioms are then written in terms of these sets, using the operators mem, inter, is_empty and cardinal (note that the latter requires importing a specific library module, as well as [int.Int](https://why3.lri.fr/stdlib/int.html) for integer numbers) .

module Classes_alt
  use set.Set     
  use set.Cardinal
  use int.Int

  type class = ClassOne | ClassTwo | ClassThree | ClassFour | ClassFive 
  type teacher = Ana | Beatriz | Carlos

  function teachers (class) : set teacher

  axiom A1 : not mem Carlos (teachers ClassOne) 

  axiom A2 : not mem Beatriz (inter (teachers ClassOne) (teachers ClassFive))

  axiom A3 : forall c :class. not is_empty (teachers c) 
  
  axiom A4 : forall c :class. c <> ClassFive -> cardinal (teachers c) <= 1 

  axiom A5 : cardinal (teachers ClassFive) <= 2

  axiom A6 : forall t :teacher.
               mem t (teachers ClassTwo) /\
               mem t (teachers ClassThree) /\
               mem t (teachers ClassFour) -> 
                 not mem t (teachers ClassOne) /\ not mem t (teachers ClassFive)
                 
  goal SAT : false

  goal g : mem Beatriz (teachers ClassFive) -> mem Ana (teachers ClassOne)

end

[Try this example online here]

Advanced Features of Why3

(things we will not be looking at)