Why3: Implementation of Software Concepts

Recall the Alloy specification of the Notifications software concept:

sig Event {}
sig User {
        var subscriptions : set Event,
        var notifications : set Event 
}

pred subscribe [u : User, e : Event] { // Subscribe to an event
        e not in u.subscriptions
        subscriptions' = subscriptions + u->e
        notifications' = notifications
}

pred unsubscribe [u : User, e : Event] { // Unsubscribe from a event
        e in u.subscriptions
        subscriptions' = subscriptions - u->e
        notifications' = notifications - u->e
}

pred read [u : User] { // Read all notifications
        some u.notifications
        notifications' = notifications - u->Event
        subscriptions' = subscriptions
}

pred occur [e : Event] { // Notify occurrence of an event
        notifications' = notifications + subscriptions :> e
        subscriptions' = subscriptions
}

This is a high-level, relational logic specification.

Alloy allowed us to specify and verify operational principles of this concept, and in particular we identified the following invariant , stating that users only receive notifications regarding events they are subscribed to:

check OP1 { // Users can only have notifications of subscribed events
        always (notifications in subscriptions)
}

or equivalently :

check OP1 { // Users can only have notifications of subscribed events
       always (all u :User, e :Event | 
           u->e in notifications implies u->e in subscriptions)
}

We will implement each software concept in WhyML as a stateful module where:

The state is encapsulated using a WhyML record type
Actions are written as WhyML functions with effects on the state
Each action predicate in the Alloy specification originates a contract for the corresponding WhyML function, making use of the Why3 standard library’s finite sets, set.Fset
Any desired state invariants can be encoded as type invariants of the state type

Note that the use of sets in the action function contracts allows for the Alloy specification to be directly encoded in Why3.

Implementation Using Sets

The most straightforward implementation uses sets (implementation type) to encode binary relations.

Consider for instance the notifications encoding. It will be implemented as a module with a state variable state, a record with two fields subscriptions and notifications :

  type user = int
  type event = int
  
  (* define imperative sets of pairs (user, event) *)
  clone set.SetImp with type elt = (user,event)    

  (* state type *) 
  type stateT = { subscriptions: set ; notifications : set }

  (* state variable *) 
  val state : stateT

Relations are manipulated by adding and removing pairs to one of the sets in the state variable.

When extracting the WhyML implementation to a running OCaml program, imperative sets are implemented as hash tables, so adding and removing pairs will tend to run in constant time. This does not mean that this is an efficient implementation option. In particular, projecting a relation (say, finding all the events subscribed by a user, or all users that subscribe to an event) is not efficient, since it will imply iterating over the entire set of pairs in the relation.

The advantage of this implementation is that it is very close to the specification. Since the finite sets library provides an implicit coercion from the implementation set type to the logic set.Fset type, the contracts of the WhyML action functions may refer to the state variables in a natural way.

For instance the subscribe action in Alloy:

pred subscribe [u : User, e : Event] { // Subscribe to an event
        e not in u.subscriptions
        subscriptions' = subscriptions + u->e
        notifications' = notifications
}

will be implemented as a program function with the following contract:

  let subscribe (u:user) (e:event)
    requires { not mem (u,e) state.subscriptions }
    ensures  { state.subscriptions = add (u,e) (old state.subscriptions) } 
    ensures  { state.notifications = old state.notifications }
  = . . .

where mem and add are logic functions on finite sets (from set.Fset).

For the remaining actions the WhyML specification consists of the following contracts:

  let unsubscribe (u:user) (e:event)
    requires { mem (u,e) state.subscriptions }
    ensures  { state.subscriptions = remove (u,e) (old state.subscriptions) } 
    ensures  { state.notifications = remove (u,e) (old state.notifications) }
  = . . .

  let read (u:user)       
    requires { exists e:event . mem (u,e) state.notifications }
            (* notifications' = notifications - u->Event *)
    ensures  { forall x:user. x <> u -> 
                 (forall e :event. mem (x,e) state.notifications 
                    <-> mem (x,e) (old state.notifications)) }
    ensures  { forall e:event . not mem (u,e) state.notifications }
    ensures  { state.subscriptions = old state.subscriptions }
  = . . .

  let occur (e:event)
            (* notifications' = notifications + subscriptions :> e *)
    ensures  { forall u:user . mem (u,e) state.notifications <->
               mem (u,e) state.subscriptions \/ mem (u,e) (old state.notifications)}
    ensures  { forall x:event . x <> e ->
                 (forall u:user. mem (u,x) state.notifications 
                    <-> mem (u,x) (old state.notifications)) }  
    ensures  { state.subscriptions = old state.subscriptions }

Let us now see in turn how each function can be implemented to be consistent with the specification. For subscribe and unsubscribe this is straightforward:

  let subscribe (u:user) (e:event)
    requires { not mem (u,e) state.subscriptions }
    ensures  { state.subscriptions = add (u,e) (old state.subscriptions) } 
    ensures  { state.notifications = old state.notifications }
  = 
  add (u,e) state.subscriptions

  let unsubscribe (u:user) (e:event)
    requires { mem (u,e) state.subscriptions }
    ensures  { state.subscriptions = remove (u,e) (old state.subscriptions) } 
    ensures  { state.notifications = remove (u,e) (old state.notifications) }
  = 
  remove (u,e) state.subscriptions ;
  remove (u,e) state.notifications

Observe that the programming (state-changing) functions add and remove and the logic functions of the same name are working on different set types, with the programming type implicitly coerced to the logic.

Turning to the more complicated functions, implementing the read action requires removing from state.notifications all pairs containing user u.
In order to iterate over all pairs we make a copy of the set and repeatedly use the choose_and_remove library function to pick and remove an arbitrary element.

  let read (u:user) 
    requires { exists e:event . mem (u,e) state.notifications }
            (* notifications' = notifications - u->Event *)
    ensures  { forall x:user. x <> u -> 
                 (forall e :event. mem (x,e) state.notifications 
                    <-> mem (x,e) (old state.notifications)) }
    ensures  { forall e:event . not mem (u,e) state.notifications }
    ensures  { state.subscriptions = old state.subscriptions }
  =
  let aux = copy state.notifications in
  while not is_empty aux do
    let (x,y) = choose_and_remove aux in
    if x = u then remove (x,y) state.notifications
  done

As usual, reasoning about while loops requires identifying appropriate invariants, as well as a variant to establish termination.

  while not is_empty aux do
    invariant { forall x:user . x <> u ->
                  (forall e :event. mem (x,e) state.notifications 
                       <-> mem (x,e) (old state.notifications)) }
    invariant { forall e:event. mem (u,e) state.notifications -> mem (u,e) aux }
    variant { cardinal aux }
    let (x,y) = choose_and_remove aux in
    if x = u then remove (x,y) state.notifications
  done

Finally we have the occur action function. We iterate over all pairs in state.subscriptions and add the pairs containing event e to state.notifications.

  let occur (e:event) 
            (* notifications' = notifications + subscriptions :> e *)
    ensures  { forall u:user . mem (u,e) state.notifications <->
               mem (u,e) state.subscriptions \/ mem (u,e) (old state.notifications)}
    ensures  { forall x:event . x <> e ->
                 (forall u:user. mem (u,x) state.notifications 
                    <-> mem (u,x) (old state.notifications)) }  
    ensures  { state.subscriptions = old state.subscriptions }
  = 
  let aux = copy state.subscriptions in
  while not (is_empty aux) do
    invariant { forall u:user. (mem (u,e) aux \/ mem (u,e) state.notifications)
                                <-> mem (u,e) state.subscriptions }
    invariant { forall x:event. x <> e ->
                  (forall u:user. mem (u,x) state.notifications 
                      <-> mem (u,x) (old state.notifications)) }
    variant { cardinal aux }
    let (x,y) = choose_and_remove aux in
    if y = e then add (x,y) state.notifications;
  done  

State Invariants

Invariant properties, that can be identified with the help of Alloy, can be proved at the implementation level by including them as type invariants in the state type.

In the Notifications example, an invariant identified in the Alloy spec states that the notifications relation is contained in subscriptions. We can include this in the state type as follows:

  type stateT = { subscriptions: set ; notifications : set }
    invariant { subset notifications subscriptions }
    by { subscriptions = empty() ; notifications = empty() }

The by clause contains an example of an inhabitant of the type that satisfies the invariant (it must be included to guarantee the consistency of the theory). One state that satisfies the invariant is, of course, the one in which both relations are empty, as given above.

Why3 will generate verification conditions to guarantee that all action functions indeed preserve this invariant. Predictably all of them can be proved, since this is a property that already holds at specification level.

The full example is available in TryWhy3 [permalink].

Case Study: the Reservations Software Concept

A second example illustrates a less direct transposition of an Alloy specification into WhyML. In the Reservations concept, resources can be Available, or Reserved by some User, or Used. There is no state variable containing the set of used resources: it is assumed that resources that are not available and not reserved are being used, and the purpose of the cleanup operation is to make used resources available again.

sig Resource {}
sig User {
        var reservations : set Resource
}
var sig Available in Resource {}


pred reserve[u : User, r : Resource] { // Make a reservation  . . . }

pred cancel[u : User, r : Resource] { // Cancel a reservation . . . }

pred use[u : User, r : Resource] { // Use a reserved resource . . . }

pred cleanup {     // Make all used resources available again . . . }

A crucial point here is that in Alloy’s untyped language Resource is a set, not a type, and Available is a subset of Resource. So the set difference operation gives us the set of used resources.

Now in Why3 it is natural to make Resource a type. We could have a state variable corresponding to the finite set of all existing resources, but instead we will have a variable for used resources (the set of existing resources is thus the union of available, reserved and used resources).

The WhyML Reservations module starts with two clonings of set.SetImp, giving us a type of sets of resources (Set.set) and a type for user \(\times\) resource binary relations Rel.set.

The state type will be a record type containing the Available and Reservations state variables as in the Alloy spec, and additionally the set of Used resources.

    type resource = int
    type user = int
        
    clone set.SetImp as Set with type elt = resource
    clone set.SetImp as Rel with type elt = (user,resource)

    type stateT = { available: Set.set ; 
                    used : Set.set ; 
                    reservations : Rel.set }

    val state : stateT

After this initial discussion the action functions are straightforward to write. Note the use of the prefixes Set. or Rel. to identify set functions on each of the set types.

(*
pred reserve[u : User, r : Resource] {
        r in Available
        Available' = Available - r
        reservations' = reservations + u->r
        Used' = Used
}
*)

    let reserve (u:user) (r:resource) 
        requires { mem r state.available }
        ensures  { state.available = remove r (old state.available) }
        ensures  { state.reservations = add (u,r) (old state.reservations) }
        ensures  { state.used = old state.used }
    =
        Set.remove r state.available ;
        Rel.add (u,r) state.reservations



(*
pred cancel[u : User, r : Resource] {
        r in u.state.reservations
        Available' = Available + r
        reservations' = reservations - u->r        
            Used' = Used
} *)

    let cancel (u:user) (r:resource) 
        requires { mem (u,r) state.reservations }
        ensures  { state.available = add r (old state.available) }
        ensures  { state.reservations = remove (u,r) (old state.reservations) }
        ensures  { state.used = old state.used }
    =
        Set.add r state.available;
        Rel.remove (u,r) state.reservations




(*
pred uses[u : User, r : Resource] {
        r in u.reservations
        reservations' = reservations - u->r        
        Used' = Used + r
        Available' = Available
} *)

    let use (u:user) (r:resource) 
        requires { mem (u,r) state.reservations }
        ensures  { state.reservations = remove (u,r) (old state.reservations) }
        ensures  { state.used = add r (old state.used) }
        ensures  { state.available = old state.available }
    =
        Set.add r state.used;
        Rel.remove (u,r) state.reservations

The cleanup action function requires iterating over all pairs in the state.reserved relation

(*
pred cleanup {
        some Used
        Available' = Available + Used
        no Used'        
        reservations' = reservations
} *)

    let cleanup ()
        requires { not is_empty state.used }
        ensures  { state.available = union (old state.available) (old state.used) }
        ensures  { is_empty state.used }
        ensures  { state.reservations = old state.reservations }
    =
        while not (Set.is_empty state.used) do
            invariant { union state.available state.used == 
                        union (old state.available) (old state.used) }
            variant { cardinal state.used }
            let x = Set.choose_and_remove state.used in
            Set.add x state.available
        done

State Invariant

Recall the following invariant of this specification, identified with Alloy:

check OP1 {
        // Reserved resources aren't available
        all r :Resource, u :User | 
          always (r in Available implies r not in u.reservations)
}

We can write it as a type invariant as follows, strengthened to state additionally that reserved resources are not used:

type stateT = { available: Set.set ; used : Set.set ; reservations : Rel.set }
  invariant  { forall u :user, r :resource. 
                 mem (u,r) reservations -> not mem r available /\ not mem r used }

  by { available = Set.empty() ; used = Set.empty() ; reservations = Rel.empty() }

Unfortunately, unlike in Alloy, this invariant cannot be established. The reason for this is that it is not inductive.

An invariant is a property that holds in every configuration of any execution of the system. Alloy checks invariants by bounded model checking, exploring exhaustively execution traces up to a given length. Deductive tools on the other hand establish that a property is an invariant by proving that every state transition preserves it. Such invariants are said to be inductive.
In order to prove an invariant in Why3, it may thus be required to strengthen it with additional properties that make it inductive.

It is easy to see that for instance the cancel action does not preserve the above invariant: in the case that a resource is reserved by more than one user, this action adds it to the Available set and deletes one of the reservations, but it may remain reserved by other users.

The addtional property that is required is in itself important in a reservation system: each resource is never reserved by more than one user. We add the following type invariant:

  invariant  { forall u1 u2 :user, r :resource. 
                 mem (u1,r) reservations /\ mem (u2,r) reservations -> u1=u2 }

The conjunction of both invariants is however still not inductive! The only reason for this now lies in the reserve action, which moves resources from Available to reserved, but does not modify the set of Used resources, and there is no context information justifying that a resource could not be left in Used while being reserved. In fact this is not possible because resources may not be simultaneously in Available and Used. We add this as an invariant:

  invariant  { forall u :user, r :resource. not (mem r available /\ mem r used) }

The conjunction of all three invariants is now inductive and the corresponding VCs are now easily proved automatically with an SMT solver.