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: Guest Placement

(from Lecture **2 on propositional logic)

We have three chairs in a row and need to place Anne, Susan and Peter

Implicit generic constraints

We will create a module containing

[Try this example online here]

Unlike a SAT solver, Why3 works with validity rather than satisfiability. The above module contains three 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 consisting of the axioms together with the negation of the goal.

Recall that a satisfiability solver may return one of three possible outcomes:

For instance the second goal **goal** sitsSusanRight : susanMiddle states that it follows from the axioms that Susan can only sit on the rightmost chair. If it is dispatched to Z3, the solver will receive a file ending with the following lines:

( ... )
;; "susanPrefs2"
(assert (=> peterMiddle (not susanLeft)))

;; Goal "sitssusanRight"
;; File "/Users/jorgesousapinto/Documents/Teaching/2o.Ciclo/WHY3/2024-MFES/PUZZLES/guestPlacement_prop.mlw", line 62, characters 7-21
(assert  (not susanMiddle))
(check-sat)

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 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. It does not allow for counter-examples to be inspected.

The purpose of the ```goal PlacementNotPossible: false` , which should be invalid, is to establish that the theory defined by the previous axioms is consistent.

We can ask Why3 to display a counterexample for goals that cannot be proved. Counterexamples are simply models for the satisfiability problems sent to solvers (the theory together with the negation of a given goal).

A model for this satisfiability problem is a counterexample for the original validity problem.

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. It can be visualized as follows:

  predicate anneLeft   (* anneLeft :  = false *)
  predicate anneMiddle  (* anneMiddle :  = false *)
  predicate anneRight  (* anneRight :  = true *)
  predicate susanLeft  (* susanLeft :  = false *)
  predicate susanMiddle  (* susanMiddle :  = true *)
  predicate susanRight  (* susanRight :  = false *)
  predicate peterLeft  (* peterLeft :  = true *)
  predicate peterMiddle  (* peterMiddle :  = false *)
  predicate peterRight  (* peterRight :  = false *)

Example: Guest Placement — first-order encoding

Why3’s logic language is many-sorted and first-order. In the following version we make use of:

[Try this example online here]

Example: Guest Placement — first-order encoding with functions

In this third version we additionally make use of

The idea is that the function sits associates a chair to each person, so the “at least one chair” and “at most one chair” requirements are no longer needed. The function must be injective in order for people to sit on different chairs.

module GuestPlacement
  type person = Anne | Susan | Peter
  type chair = Left | Middle | Right
  function sits person : chair

  (* At most one guest per chair *)
  axiom inj : forall p1 p2 :person. p1 <> p2 -> sits p1 <> sits p2

  (* Preferences *) 
  axiom AnnePrefs1 : sits Anne = Right -> sits Peter <> Middle
  axiom AnnePrefs2 : sits Anne  = Middle ->  sits Peter <> Left /\ sits Peter <> Right
  axiom AnnePrefs3 : not (sits Anne) = Left
  axiom SusanPrefs1 : sits Peter = Right -> sits Susan <> Middle
  axiom SusanPrefs2 : sits Peter = Middle -> sits Susan <> Left

  (* Does this problem have a solution? 
     Yes if the following goal cannot be proved *) 
  goal PlacementNotPossible: false

  (* Is it true that Susan can ONLY sit on the Middle chair? *)
  goal sitsSusanRight : sits Susan = Middle

  (* is it true that Peter cannot sit on the Right? *)
  goal sitsAnneRight : sits Peter <> Right
end

[Try this example online here]

Example: File System Domain Model

We will use types Object, Entry, and Name. The specialized domains Dir, File, and Root will be captured as predicates (since “subtyping” is not supported in many-sorted logic).

In fact, since there is a single Root it makes sense to model Root as a constant, so we no longer need the axioms:

∃x. Root(x)
∀x, y. Root(x) ∧ Root(y) →  x = y

Additionally, the following axioms do not make sense in this typed formalization, since types are disjoint by nature:

∀x. ¬(Object(x) ∧ Entry(x))
∀x. ¬(Object(x) ∧ Name(x))
∀x. ¬(Name(x) ∧ Entry(x))

Also, from the following constraints that were required as axioms in the untyped / Alloy setting:

∀x, y. contains(x, y) → Dir(x) ∧ Entry(y)
∀x, y. refersTo(x, y) → Entry(x) ∧ Object(y)
∀x, y. has(x, y) → Entry(x) ∧ Name(y)

In the typed setting we will require only ∀x, y. contains(x, y) → Dir(x). The others will be typing constraints.

It is important to clarify the meaning of ∀x : A. ϕ in Alloy and in many-sorted logic

[Try this example online here]

Exercise: File System Model with functions

(Total) functions are used for the three associations, since all of them have a unicity constraint. This leads to a more compact model, since the multiplicity constraints do not have to be written as axioms:

module FileSystem
  (...)
  (* Other associations  *)
  function has (entry) : name
  function container (entry) : object
  function refersTo (entry) : object

  (* Typing *)
  axiom type1 : forall e :entry. dir (container e)

  (* Different entries in the same directory have different names *)
  axiom req1 : forall e1 e2 :entry.
                 e1 <> e2 /\ container e1 = container e2 ->
                    has e1 <> has e2
  (...)
end

Complete this model.

Exercise: Photo Sharing Social Network Domain Model

Why3 offers a standard library of theories and data structures that can be used across all the supported proof tools.

We’ll take the above model as an opportunity to introduce the Why3 set theory. The idea will be to model the associations as functions to sets, rather than predicates.

module SocialNetwork
  use set.Set     

  (* Entities *)
  type user
  predicate isInfluencer (user)
  type photo 
  predicate isAd (photo)
  type day 

  (* Associations *)
  function follows (user) : set user
  function sees (user) : set photo
  function posts (user) : set photo
  function suggested (user) : set user
  function date (photo) : day  (* no further multiplicty constraints are needed! *)

  (...)
end

Finish the above model. You can find the available set predicates and functions in the Why3 library, but you can probably solve the exercise using just the membership predicate:

predicate mem (x: 'a) (s: set 'a)