Why3: State-based Development
A deductive verification tool like Why3 can be used to check the behavior of a collection of functions working on a shared state, such as classes in object-oriented programming (sharing instance variables), smart contracts in blockchain development, or multi-threaded concurrent programming (based on shared memory).
We will illustrate this by means of an example where we model functions operating on a bank account.
The global shared state stores the balance of each account, identified by a number.
module Accounts_MapImp
use int.Int
type accNumber = int
type amount = int
val open (n :accNumber) : ()
val deposit (n :accNumber) (x :amount) : ()
val withdraw (n :accNumber) (x :amount) : ()
val transfer (from :accNumber) (to_ :accNumber) (x :amount) : ()
We need a way to associate balances with account numbers. We will use a Why3 finite map (or dictionary) type for this purpose. The Why3 library https://why3.lri.fr/stdlib/fmap.html makes available different logic and programming types for finite maps.
We will use a programming type of imperative maps. The read, write, and key membership functions on this type are specified in the library with the following prototypes:
val find (k: key) (m: t 'v) : 'v
val add (k: key) (v: 'v) (m: t 'v) : unit
val mem (k: key) (m: t 'v) : bool
Programming types are used by cloning the respective module into our own. In this concrete case we will instantiate the type of the map keys:
clone fmap.MapImp with type key = accNumber
type mapAccAmount = t amount
The type of maps with accNumber
as keys is available with name t
; we then define mapAccAmount
as the concrete type of maps from accNumber
to amount
.
The following declares the state variable accounts
as such a map:
val accounts : mapAccAmount
We wish to write functions to do the following tasks:
- open a new account with a given account number
- deposit funds into a given account
- withdraw funds from an account
- transfer funds internally from an account to another
As a first step let us consider a natural language specification of their behavior. For instance:
-
given an account number
n
, the callopen n
will insert the pair (n
→0) in theaccounts
dictionary -
given an account number
n
and an amountx
, the calldeposit n x
will addx
to the current balance of accountn
-
. . .
Preconditions and Implementation
An important step is to discuss what the functions should do in case they receive unexpected argument values. What should happen if
-
in a call
open n
, the account numbern
already exists, i.e. it is already present in the domain ofaccounts
? -
in a call
deposit n x
,- the number
n
is not a valid account number (i.e. it is not in the domain ofaccounts
, - or
x
is a negative number ?
- the number
We will choose not to program defensively : the functions will take for granted, without checking, that unsafe calls do not occur.
In the absence of defensive programming it is the caller’s responsibility to make sure that all calls satisfy the desired conditions, which should be included in the contracts of the callee functions as preconditions.
The four desired functions can be promptly written, including preconditions, as follows, using the dictionary functions add
and find
:
let open (n :accNumber) : ()
requires { not mem n accounts }
= add n 0 accounts
let deposit (n :accNumber) (x :amount) : ()
requires { mem n accounts /\ x > 0 }
= let bal = find n accounts in
add n (bal+x) accounts
let withdraw (n :accNumber) (x :amount) : ()
requires { mem n accounts /\ 0 < x <= accounts n }
= let bal = find n accounts in
add n (bal-x) accounts
let transfer (from :accNumber) (to_ :accNumber) (x :amount) : ()
requires { mem from accounts /\ mem to_ accounts }
requires { from <> to_ }
requires { 0 < x <= accounts from }
= let balfrom = find from accounts in
let balto = find to_ accounts in
add to_ (balto +x) accounts ;
add from (balfrom-x) accounts
Why3 generates verification conditions for find
operations, to guarantee that the keys being read are actually in the domain of the dictionary (finite map). The preconditions ensure that they actually are, so all VCs are proved valid.
State Invariants
We may wish to prove that certain properties of the global state always hold, i.e. they are invariants of all the state-changing functions.
For instance:
The balance of every account is non-negative
This can be written as a predicate on maps (from accounts to amounts) as follows:
predicate inv (accs : mapAccAmount) =
forall a :accNumber. mem a accs -> accs a >= 0
Such properties may be treated by simply including them simultaneously as pre- and postconditions in all functions:
requires { inv accounts }
ensures { inv accounts }
The set of verification conditions for the resulting module (permalink) now contains additional VCs, ensuring that the invariant is preserved by every function.
Postconditions and “Complete” Specs
The specifications in the previous module contain safety preconditions, and can be see as adequate for reasoning about the state invariant described above. However, they are not sufficient for reasoning about programs using the functions, such as:
let main ()
requires { accounts = empty }
ensures { accounts 3333 = 200 }
= open 1111 ;
open 2222 ;
open 3333 ;
deposit 1111 100 ;
deposit 2222 100 ;
transfer 1111 3333 100 ;
transfer 2222 3333 100
The reason for this is that the code of the functions is not visible at the logic level, so there is no way to establish the postcondition of the main function.
Moreover, each of the above function calls will generate safety VCs regarding the presence of the different account numbers in the dictionary, and for the same reason these cannot be proved.
The way to solve this problem is to write more complete specifications for the functions, including postconditions describing exactly what the functions do, in particular:
- which account numbers are in the dictionary after a call to the function;
- and what the balance of each account is
For instance a complete spec for open
can be given as follows:
let open (n :accNumber) : ()
requires { not mem n accounts }
ensures { forall a:accNumber. mem a accounts <-> mem a (old accounts) \/ a = n}
ensures { accounts n = 0 }
ensures { forall a :accNumber. mem a accounts /\ a <> n ->
accounts a = old accounts a }
= add n 0 accounts
Note that:
- The first postcondition relates the keysets (domains) of the mapping before and after execution of each function
- The second postcondition specifies the balance of account n
- The third one expresses an obvious fact that is implicit in the natural language spec, but must be stated explicitly in the contract: with the exception of account
n
, all balances are preserved
The complete module [permalink] , including the above main
function, can be entirely proved with TryWhy3.
Record types and type invariants
Why3 provides a more convenient way to verify state invariants such as the inv
predicate given above. It suffices to encapsulate the state variable(s) inside a record type, and attach a type invariant to it:
module Accounts_MapImp_Record
use int.Int
type accNumber = int
type amount = int
clone fmap.MapImp with type key = accNumber
type state = { mutable bal: t amount }
invariant { forall a :accNumber. mem a bal -> find a bal >= 0 }
by { bal = create() }
val accounts :state
Declaring the state using a record type allows us to include the state invariant directly in the type definition. Verification conditions will be automatically created for all state-changing functions, ensuring the preservation of the type invariant.
Note that:
- The
by
clause is mandatory. Its role is to provide a witness satisfying the type invariant. We simply provide the empty mapping as example (it is returned by thecreate
function) - Record fields are by default immutable (as in functional programming). Mutable fields must be explicitly identified as above
Both in the code and the spec, the balance value will have to be referred using record field notation, for instance:
let open (n :accNumber) : ()
requires { not mem n accounts.bal }
ensures { forall a:accNumber. mem a accounts.bal <->
mem a (old accounts.bal) \/ a = n }
ensures { accounts.bal n = 0 }
ensures { forall a :accNumber. mem a accounts.bal /\ a <> n ->
accounts.bal a = old accounts.bal a }
= add n 0 accounts.bal
The complete module [permalink] can be fully verified using Try Why3.