Why3: Statebased 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 objectoriented programming (sharing instance variables), smart contracts in blockchain development, or multithreaded 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 type for this purpose. Map types implement dictionaries; the Why3 library https://why3.lri.fr/stdlib/fmap.html makes the following available:
 a logiclevel map type (module
Fmap
) that cannot be extracted to code;  and two programming map types, that can be extracted (typically implemented as hash tables)
 a “functional” type (module
MapApp
)  and an “imperative” type (module
MapImp
)
 a “functional” type (module
Since we want to program with maps we will use programming types.
We start by using the imperative type. The read and write functions on this type are specified in the library as follows. Note that the find
and add
functions used in the contracts are synonymous logiclevel functions: the behavior of programminglevel maps is specified using the Fmap
logic type.
val find (k: key) (m: t 'v) : 'v
requires { mem k m }
ensures { result = m[k] }
ensures { result = find k m }
val add (k: key) (v: 'v) (m: t 'v) : unit
writes { m }
ensures { m = add k v (old m) }
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
The type of maps with accNumber
as keys is now available with name t
. The following declares the state variable accounts
as a map with values of type amount
:
val accounts : t amount
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
The next 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 that the above situations do not occur.
So the definitions are really simple:
let open (n :accNumber) : ()
= add n 0 accounts
let deposit (n :accNumber) (x :amount) : ()
= let bal = find n accounts in
add n (bal+x) accounts
Now, 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:
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
We will now also include postconditions in the functions’ contracts. This will not only allow us to prove that the implementations respect the specifications (expressed above in natural language), but also that no calls are made that do not respect the preconditions.
let open (n :accNumber) : ()
requires { not mem n accounts }
ensures { mem n accounts /\ find n accounts = 0 }
ensures { forall a :accNumber. mem a accounts <> mem a (old accounts) \/ a = n }
writes { accounts }
= add n 0 accounts
let deposit (n :accNumber) (x :amount) : ()
requires { mem n accounts /\ x > 0 }
ensures { find n accounts = find n (old accounts) + x }
ensures { forall a :accNumber. mem a accounts /\ a <> n
> find a accounts = find a (old accounts) }
ensures { forall a :accNumber. mem a accounts <> mem a (old accounts) }
writes { accounts }
= let bal = find n accounts in
add n (bal+x) accounts
Note that:

The postcondition highlighted in
deposit
expresses an obvious fact that is implicit in the natural language spec, but should be stated explicitly in the contract: all balances are preserved, with the exception of accountn

The contracts also include postconditions relating the keysets (domains) of the mapping before and after execution of each function

The frame conditions
writes ...
make explicit the effects of the functions, i.e. the parts of the global state that are modified by them
State Invariants
We may wish to prove that certain properties of the global state always hold, i.e. they are invariants of all the statechanging functions.
For instance:
The balance of every account is nonnegative
Such properties may be treated by simply including them simultaneously and pre and postconditions in all functions. We may then add the following to the contracts of the functions defined above:
requires { forall a :accNumber. mem a accounts > find a accounts >= 0 }
ensures { forall a :accNumber. mem a accounts > find a accounts >= 0 }
Exercise Complete the definition of the module by equipping the remaining functions with appropriate contracts and proving their correctness. Also,
let withdraw (n :accNumber) (x :amount) : ()
= let bal = find n accounts in
add n (balx) accounts
let transfer (from :accNumber) (to_ :accNumber) (x :amount) : ()
= let balfrom = find from accounts in
let balto = find to_ accounts in
add to_ (balto +x) accounts ;
add from (balfromx) accounts
Record types and type invariants
We could alternatively used a declarative / functional type for maps. We will illustrate their use with an alternative implementation of the above module
module Accounts_MapApp_Record
use int.Int
type accNumber = int
type amount = int
clone fmap.MapApp 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, which makes it unnecessary to include it explicitly as a pre and postcondition in function definitions (verification conditions will be created automatically for all statechanging 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. Note also the use of the <
assignment operator: since we are now using an applicative map type, the add
function may not have side effects — in functional style, it takes a map and returns a new map).
let open (n :accNumber) : ()
requires { not mem n accounts.bal }
ensures { mem n accounts.bal /\ find n accounts.bal = 0 }
ensures { forall a :accNumber. mem a accounts.bal <> mem a (old accounts.bal) \/ a = n }
writes { accounts.bal }
= accounts.bal < add n 0 accounts.bal
let deposit (n :accNumber) (x :amount) : ()
requires { mem n accounts.bal /\ x > 0 }
ensures { find n accounts.bal = find n (old accounts.bal) + x }
ensures { forall a :accNumber. mem a accounts.bal /\ a <> n
> find a accounts.bal = find a (old accounts.bal) }
ensures { forall a :accNumber. mem a accounts.bal <> mem a (old accounts.bal) }
writes { accounts.bal }
= let baln = find n accounts.bal in
accounts.bal < add n (baln+x) accounts.bal
Exercise Complete the definition of this alternative implementation, by writing all the remaining functions and their contracts (do not include the type invariant in the contracts). Observe carefully all verification conditions, in particular those pertaining to the type invariant.
Challenge
Consider now that we want to prove properties involving the global assets held in the accounts:
 The
create
andtransfer
functions do not modify the total value of these assets; deposit
andwithdraw
increase or decrease the total value byx
In order to state these properties we need a way to compute this global value (at logic level). The problem is that the domain of the map types is a set, and thus not iterable.
We may address this problem by including in the record type a ghost field **of a list type **(i.e. a field that is not meant for programming, only kept for specification/logic purposes), and including in the type invariant information tying the list to the domain of the map;
use list.Mem
type state = { mutable bal: t amount ; mutable ghost domain : list accNumber }
invariant { (forall a :accNumber. mem a bal > find a bal >= 0) /\
(forall a :accNumber. MapApp.mem a bal <> Mem.mem a domain) }
by { bal = create() ; domain = Nil }
val accounts :state
Now write a function to calculate the total value of the assets in the accounts (by traversing the domain list), and use it to extend the contracts with the properties expressed above.