Why3: Abstract Specifications and Ghost Code
Recall the Trash Software Concept in Alloy, and the corresponding state variables and actions:
sig Item {}
var sig Accessible in Item {}
var sig Trashed in Item {}
pred create[i : Item] {
i not in Accessible + Trashed
Accessible' = Accessible + i
Trashed' = Trashed }
pred delete[i : Item] {
i in Accessible
Accessible' = Accessible - i
Trashed' = Trashed + i }
pred restore[i : Item] {
i in Trashed
Accessible' = Accessible + i
Trashed' = Trashed - i }
pred empty {
some Trashed
no Trashed'
Accessible' = Accessible }
Recall also that in the last lecture we already implemented this concept as a WhyML module, using lists to represent the two sets Accessible and Trashed:
module Trash_Record
type item
type stateT = { mutable accessible : list item ;
mutable trashed : list item }
invariant { forall x :item. not (mem x accessible /\ mem x trashed) }
by { accessible = Nil ; trashed = Nil }
val state : stateT
let create (i : item)
requires { not mem i state.accessible /\ not mem i state.trashed }
= state.accessible <- Cons i state.accessible
let delete (i : item)
requires { mem i state.accessible }
= state.accessible <- deleteAll i state.accessible ;
state.trashed <- Cons i state.trashed
let restore (i : item)
requires { mem i state.trashed }
= state.trashed <- deleteAll i state.trashed ;
state.accessible <- Cons i state.accessible
let empty ()
requires { not is_nil state.trashed }
= state.trashed <- Nil ;
end
Abstract Specifications in WhyML
We will now see how to convert a sets/relations-based Alloy specification to WhyML, to allow concrete implementations (such as the one given above for Trash) to be proven correct. This will result in a complete development workflow:
- from abstract Alloy spec (validated in Alloy, from scenarios to operational principles/temporal properties),
- to WhyML abstract spec and verified WhyML code,
- and then to extracted OCaml implementation.
We will write the Alloy specification in WhyML using the notion of ghost code.
Ghost code operates on ghost state, and is a very useful device in program specification. It allows for programs to be equipped with ‘shadow’ instructions working on ghost variables. These variables can appear in function contracts, which allows for properties relating regular code and ghost code to be written.
A WhyML version of the Alloy specification:
sig Item {}
var sig Accessible in Item {}
var sig Trashed in Item {}
can be written as follows:
use set.Fset
type stateT = { ghost mutable accessible : fset item ;
ghost mutable trashed : fset item }
val state : stateT
A state variable is declared in the module of the stateT record type, which has ghost fields only. Note that ghost data has logic types such as **fset** item. Just as in the Alloy spec, the trash concept has two sets of items as state variables.
Recall that the following invariant has been established for the Alloy spec:
always no Accessible & Trashed
This can be included in the WhyML specification as a type invariant:
type stateT = { ghost mutable accessible : fset item ;
ghost mutable trashed : fset item }
invariant { disjoint accessible trashed }
by { accessible = empty ; trashed = empty }
As to the actions in the Alloy specification, they will be defined as functions manipulating the ghost state. We inspect the specification and identify a precondition in which action predicate. The remaining clauses describe the state change. For instance:
pred create[i : Item] {
i not in Accessible + Trashed
Accessible' = Accessible + i
Trashed' = Trashed }
The new state will be produced by writing instructions manipulating the ghost fields (note that add is an Fset function).
let ghost create (i : item)
requires { not mem i (union state.accessible state.trashed) }
= state.accessible <- add i state.accessible
Note that the mem predicate is here Fset.mem.
The function is marked as **ghost** since it contains exclusively ghost code.
We can of course equip it with a postcondition
let ghost create (i : item)
requires { not mem i (union state.accessible state.trashed) }
ensures { state.accessible = add i (old state.accessible) /\
state.trashed = old state.trashed }
= state.accessible <- add i state.accessible
The ghost instruction state.accessible <- **add** i state.accessible and the postcondition are equivalent logic descriptions of how this action changes the state. However, only the former allows for the state invariant to be established.
let ghost delete (i : item)
requires { mem i state.accessible }
= state.accessible <- remove i state.accessible ;
state.trashed <- add i state.trashed
let ghost restore (i : item)
requires { mem i state.trashed }
= state.trashed <- remove i state.trashed ;
state.accessible <- add i state.accessible
let ghost empty ()
requires { not (is_empty state.trashed) }
= state.trashed <- empty
From this specification Why3 will generate 4 valid verification conditions labeled “type invariant”, which together ensure that the provided state invariant is valid (no item is simultaneously accessible and in the trash).
Implementing Abstract Specifications
We will now implement the specified concept by adding regular state variables (record fields) and code to the type and function definitions in the previous module.
A crucial element of this method is the presence of a refinement invariant that establishes a correspondence between the specification state (ghost fields) and the implementation state (regular fields).
In the current example we simply put together in a single module the previous two (specification and implementation). The state record type contains two ghost fields (sets of items) and two regular fields (lists of items). The refinement invariant simply states that the sets contain the same elements as the lists.
type stateT = { mutable accessible_ : list item ;
mutable trashed_ : list item ;
ghost mutable accessible : fset item ;
ghost mutable trashed : fset item }
(* Specification-level invariant *)
invariant { disjoint accessible trashed }
(* Refinement correspondence *)
invariant { accessible = elements accessible_ /\
trashed = elements trashed_ }
by { accessible_ = Nil ;
trashed_ = Nil ;
accessible = empty ;
trashed = empty }
val state : stateT
Noe that there is no need for the following implementation-level invariant, which follows from the spec-level invariant and the refinement correspondence:
invariant { forall x :item. not (mem x accessible /\ mem x trashed) }
Observe also that it may be a good idea to keep separate modules for
- Specification, containing only ghost code and proofs of specification-level invariants
- Implementation, containing both the ghost and regular code.
In this case there is no need to include specification-level invariants in the implementation module.
Similarly, in the presence of specification contracts the corresponding implementation-level preconditions can be omitted. For instance
let ghost create (i : item)
requires { not mem i (union state.accessible state.trashed) }
requires { not mem i state.accessible_ /\ not mem i state.trashed_ }
...
The complete definition would be:
let create (i : item)
requires { not mem i (union state.accessible state.trashed) }
= state.accessible_ <- Cons i state.accessible_ ;
state.accessible <- add i state.accessible
Note that the simultaneous execution of regular and ghost code ensures the preservation of the refinement correspondence invariant, which in turn guarantees that the implementation adheres to the specification.
As a second example (deleteAll is a function that removes all occurrences of an element from a list):
let delete (i : item)
requires { mem i state.accessible }
= state.accessible_ <- deleteAll i state.accessible_ ;
state.trashed_ <- Cons i state.trashed_ ;
state.accessible <- remove i state.accessible ;
state.trashed <- add i state.trashed
Exercise
Sets can of course be represented by lists not containing repeated elements, in which case the list delete function can be optimized (no need to to look for further occurrences when the the desired element is found).
Modify the previous implementation by adding the following invariant to the state record type:
invariant { forall i :item. num_occ i accessible_ <= 1 /\
forall i :item. num_occ i trashed_ <= 1 }
Then write the optimized function deleteOne and substitute it for deleteAll.
What happens if you use deleteOne without adding the above type invariant ?
A Second Example: the Reservations Concept
It is not always appropriate to interpret an Alloy domain predicate as a FOL type. This example illustrates how a finite set can be used instead.
Recall the Reservations concept, where users book resources:
sig Resource {}
sig User {
var reservations : set Resource
}
var sig Available in Resource {}
We will translate this as follows:
type resource
type user
type pair = (user,resource)
type stateT = { ghost resources : fset resource ;
mutable ghost available : fset resource ;
mutable ghost reservations : fset pair }
The available and reservations state record fields are the expected sets, but we also include a field resources corresponding to the Resource predicate in the Alloy spec. Note that this field is immutable, since the set of resources is fixed in the Alloy specification.
Note that resources in the Alloy spec now correspond to inhabitants of the WhML type resource that are elements of the set resources. This requires the presence typing invariants stating that available and reserved resources are all elements of resources :
invariant { forall r :resource. mem r available -> mem r resources }
invariant { forall r :resource.
(exists u :user. mem (u,r) reservations) -> mem r resources }
Recall the following two state invariants identified in the Alloy specification:
all r :Resource, u :User | always (r in Available implies r not in u.reservations)
always (all r : Resource | lone reservations.r)
We include them as type invariants as follows:
invariant { forall u :user, r :resource.
mem (u,r) reservations -> not mem r available }
invariant { forall u1 u2 :user, r :resource.
mem (u1,r) reservations /\ mem (u2,r) reservations -> u1=u2 }
by { resources = empty ; available = empty ; reservations = empty }
val state : stateT
The all-sets-empty record is provided as an example of a state for which all the provided invariants hold.
Recall the first three action predicates of this specification:
pred reserve[u : User, r : Resource] {
r in Available
Available' = Available - r reservations' = reservations + u->r
}
pred cancel[u : User, r : Resource] {
r in u.reservations
Available' = Available + r reservations' = reservations - u->r
}
pred use[u : User, r : Resource] {
r in u.reservations
Available' = Available reservations' = reservations - u->r
}
Their WhyML versions offer no surprises:
let ghost 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) }
=
state.available <- remove r state.available ;
state.reservations <- add (u,r) state.reservations
let ghost cancel (u:user) (r:resource)
requires { mem (u,r) state.reservations }
ensures { ... }
= state.available <- add r state.available ;
state.reservations <- remove (u,r) state.reservations
let ghost uses (u:user) (r:resource)
requires { mem (u,r) state.reservations }
ensures { ... }
= state.reservations <- remove (u,r) state.reservations
Cleanup is a more challenging action.
pred cleanup {
some Resource - Available - User.reservations
Available' = Resource - User.reservations
reservations' = reservations
}
We will use the **filter** library function to obtain the set of resources that are not reserved by any user.
function filterRsr (s:fset resource) (sp:fset pair) : fset resource =
filter s (fun r -> forall u :user. not mem (u,r) sp)
let ghost cleanup ()
requires { exists r :resource. mem r state.resources /\
not mem r state.available /\
forall u :user. not mem (u,r) state.reservations }
ensures { forall r :resource. mem r state.available <->
mem r state.resources /\
forall u :user. not mem (u,r) state.reservations }
ensures { state.reservations = old state.reservations }
=
state.available <- filterRsr state.resources state.reservations
Refinement
In order to implement this specification it will be useful to keep a list of resources that are currently in use, so that they can be found without looking at the entire list of resources.
We can add this state variable at the specification level, thus refining the previous specification.
type stateT = { ghost resources : fset resource ;
mutable ghost available : fset resource ;
mutable ghost used : fset resource ;
mutable ghost reservations : fset pair }
(* ... *)
(* Refinement correspondence *)
invariant { forall r :resource. mem r used <->
mem r resources /\
not (exists u :user. mem (u,r) reservations) /\
not mem r available }
by { resources = empty ; available = empty ; used = empty ; reservations = empty }
Note the presence of a new type invariant stating that the set of used resources consists of all resources that are neither reserved nor available.
The definitions of the reserve and cancel functions remain unchanged, but uses now updates resources in use:
let ghost uses (u:user) (r:resource)
requires { mem (u,r) state.reservations }
=
state.reservations <- remove (u,r) state.reservations ;
state.used <- add r state.used
Finally, cleanup makes available resources in use without filtering the entire set of resources, and empties the set of used resources:
let ghost cleanup ()
requires { exists r :resource. mem r state.resources /\
not mem r state.available /\
forall u :user.not mem (u,r) state.reservations }
=
state.available <- union state.available state.used ;
state.used <- empty
Exercise
Now it’s time to implement this concept.
Since the reservations relation has a unicity constraint (resources are reserved by at most one user), one natural possibility is to implement it as a map from resources to (single) users. The used and available sets can be implemented as lists. Take the following as a starting point.
Note that for an implementation with uninterpreted types for users and resources, you will need to declare an equality predicate to be instantiated later when the types are defined. See below.
val (=) (x y : resource) : bool
ensures { result <-> x = y }
(* map from resources to users *)
clone fmap.MapApp with type key = resource
type mapRU = MapApp.t user
type stateT = { ghost resources : fset resource ;
mutable available_ : list resource ;
mutable used_ : list resource ;
mutable reservations_ : mapRU ;
mutable ghost available : fset resource ;
mutable ghost used : fset resource ;
mutable ghost reservations : fset pair }
val state : stateT
...