Consider again the Trash software concept in WhyML, from the previous lecture:

  type item 
  type stateT = { ghost mutable accessible : fset item ;
                  ghost mutable trashed : fset item }
     invariant  { disjoint accessible trashed }
     by { accessible = empty ; trashed = empty }

  val state : stateT

  let ghost create (i : item) 
    requires { not mem i (union state.accessible state.trashed) }
  = state.accessible <- add i state.accessible

  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

We will now rewrite it as a functional concept: instead of modifying a shared state record, the action functions will be pure, returning and receiving a stateT record. Consequently,

the record fields, corresponding to the specification state variables, will not be mutable.

Additionally,

the functions will be declared, with no ghost definitions ;

the record fields, corresponding to the specification state variables, will be regular, not ghost .

module Trash_model_fun use set.Fset type item type stateT = abstract { accessible : fset item ; trashed : fset item }
invariant { disjoint accessible trashed } by { accessible = empty ; trashed = empty }

val function create (i:item) (state:stateT) : stateT
  requires { not mem i (union state.accessible state.trashed) }
  ensures  { result.accessible = add i state.accessible  }
  ensures  { result.trashed = state.trashed }

val function delete (i:item) (state:stateT) : stateT
  requires { mem i state.accessible }
  ensures  { result.accessible = remove i state.accessible }
  ensures  { result.trashed = add i state.trashed }

val function restore (i:item) (state:stateT) : stateT
  requires { mem i state.trashed }
  ensures  { result.accessible = add i state.accessible }
  ensures  { result.trashed = remove i state.trashed }

val function empty (state:stateT) : stateT
  requires { not (is_empty state.trashed) }
  ensures  { result.accessible = state.accessible }
  ensures  { is_empty result.trashed }

end

Note the presence of the keyword abstract in the type definition. The idea is that we will now implement this concept in a different module, and use a Why3 mechanism to establish that it actually implements the abstract specification module.

Note that the module includes:

the declaration of a (program) equality predicate eqi on type item, with a postcondition linking it to the logic equality predicate.

a constructor function mkTrash that returns an initial (both sets empty) trash.

module Trash_List_noReps_fun use … type item val eqi (x y :item) : bool ensures { result <-> x=y }

type stateT = { accessible_ : list item ;
                trashed_ : list item ;
                ghost accessible : fset item ;
                ghost trashed : fset item }
    
  (* Refinement correspondence *)
  invariant  { accessible = elements accessible_ /\
               trashed    = elements trashed_ }

  (* Abstract (spec-level) invariant *)
  invariant  { disjoint accessible trashed }

  (* Implementation invariant *)
  invariant  { forall i :item. num_occ i accessible_ <= 1 /\
               forall i :item. num_occ i trashed_ <= 1 }
                     
  by { accessible_ = Nil ; trashed_ = Nil ; 
       accessible = empty ; trashed = empty }
  
(* Constructor function, not part of the software concept *)
let mkTrash () : stateT
= { accessible_ = Nil ;
    trashed_ = Nil ; 
    accessible = empty ;
    trashed = empty }

Observe that the fields of the abstract state record type become ghost fields in the implementation state type. This record type:

must include a refinement invariant, establishing a correspondence between implementation and specification fields;
may if necessary include an implementation invariant;
may include the abstract invariant (involving the ghost fields only).

In the present example, the disjoint sets property (abstract invariant) is required in order to prove that the implementation invariant is preserved by the delete function — so we include it in the implementation state type.

The function definitions will now include both the program and ghost code:

  let function create (i : item) (state : stateT) : stateT
    requires { not mem i (union state.accessible state.trashed) }
  = { accessible_ = Cons i state.accessible_ ;
      trashed_ = state.trashed_ ; 
      accessible = add i state.accessible ;
      trashed = state.trashed }

  let function delete (i : item) (state : stateT) : stateT
    requires { mem i state.accessible }
  = ...

  let function restore (i : item) (state : stateT) : stateT
    requires { mem i state.trashed }
  = ...

  (* 'empty' cannot be used here, we add '_' *)
  let function empty_ (state : stateT) : stateT
    requires { not (is_empty state.trashed) }
  = ... 

Finally, the module ends by cloning the abstract specification module. This copies that module into the present one, instantiating the desired elements, declared in the specification, with the above type and function definitions:

  clone Trash_model_fun with 
    type item, type stateT,
    val create, val delete, val restore, val empty=empty_

end

The clone operation makes Why3 generate a number of verification conditions that will in particular ensure the following:

the abstract type invariant holds for all values of the implementation type
the contracts and function definitions in the implementation module are in accordance with the contracts provided in the specification module

The first condition is trivial in the current example because we have included that invariant in the implementation record type).

Note that, since the action functions are pure, the second condition does not require the presence of postconditions — the specification contracts can be proved directly from the logical encoding of the functions.

Let us move one more step towards an actual implementation. We create another module in which we clone the above implementation module and instantiate the item type and its equality predicate. For the sake of simplicity we will just use integers:

module ExampleTrash
  use int.Int
  clone Trash_List_noReps_fun
    with type item = int, val eqi = (=)

end

We can now write a main function and verify it, or run it using the WhyML interpreter:

  let main () =
    let intrash = mkTrash () in
    let intrash = create 10 intrash in
    let intrash = create 20 intrash in
    let intrash = create 30 intrash in
    let intrash = delete 20 intrash in
    let intrash = delete 30 intrash in
    let intrash = restore 20 intrash in
    assert { mem 30 intrash.trashed /\
             not mem 20 intrash.trashed /\
               not mem 10 intrash.trashed }

But let us focus on extracting an OCaml implementation from the WhyML implementation module. We invoke why3 on the command line with the extract command, and use de -D flag to provide the extraction driver ocaml64.

% why3 extract -D ocaml64 trashfun.ExampleTrash -o trashfun.ml -L .

trashfun.ExampleTrash denotes the ExampleTrash module in the trashfun.mlw file. The resulting OCaml code is stored in file trashfun.ml :

type stateT = {
  accessible_: (Z.t) list;
  trashed_: (Z.t) list;
  }

let mkTrash (_: unit) : stateT = { accessible_ = [] ; trashed_ = []  }

let create (i: Z.t) (state: stateT) : stateT =
  { accessible_ = i :: state.accessible_; trashed_ = state.trashed_ }

let rec deleteOne (x: Z.t) (l: (Z.t) list) : (Z.t) list =
  match l with
  | [] -> [] 
  | h :: t -> if Z.equal h x then t else h :: deleteOne x t

let delete (i: Z.t) (state: stateT) : stateT =
  { accessible_ = deleteOne i state.accessible_; trashed_ =
    i :: state.trashed_ }

let restore (i: Z.t) (state: stateT) : stateT =
  { accessible_ = i :: state.accessible_; trashed_ =
    deleteOne i state.trashed_ }

let empty_ (state: stateT) : stateT =
  { accessible_ = state.accessible_; trashed_ = []  }

Rather than use the WhyML main function that we wrote (see above), we can now ask any LLM chat to generate an OCaml module to exemplify the use of our little Trash library:

AI, write a main function to demonstrate the use of the OCaml code in … ( the file trashfun.ml )

We store this code in the file trashfunMain.ml. Note that it starts with the command open Trashfun that includes the code generated by Why3. We can now compile and run the main function:

% ocamlbuild -pkg zarith trashfunMain.native

Note that:

The switch -pkg zarith instructs the compiler to use the zarith arbitrary precision integers library, used by Why3 to encode the int type.
The trashfun.ml file will be found by ocamlbuild , with no need to mention it in the above command line.

The executable can now be run:

% ./trashfunMain.native 
Initial state: accessible = , trashed = 
After creating items: accessible = 3, 2, 1, trashed = 
After deleting 2: accessible = 3, 1, trashed = 2
After restoring 2: accessible = 2, 3, 1, trashed = 
After deleting 1: accessible = 2, 3, trashed = 1
After emptying trash: accessible = 2, 3, trashed = 

Files:

[trashfun.mlw](https://haslab.github.io/MFES/Why3/Extraction/trashfun.mlw)
[trashfun.ml](https://haslab.github.io/MFES/Why3/Extraction/trashfun.ml)
[trashfunMain.ml](https://haslab.github.io/MFES/Why3/Extraction/trashfunMain.ml)

An Imperative, Array-based Implementation

There is a major obstacle in obtaining an array-based implementation of Trash:

the software concept assumes there are no bounds on the size of the sets of accessible and trashed elements, which is not the case with (statically-allocated) arrays, which have a fixed length.

So we will modify our concept to include boolean indications of whether each set is full or not, to be used in preconditions of the action functions.

Note that, since this will not be a functional implementation, we again need our state record fields to be mutable.

module Trash_model_impBound
  use set.Fset
  type item 
  type stateT = abstract { mutable accessible : fset item ;
                           mutable fullA : bool ;
                           mutable trashed : fset item ;
                           mutable fullT : bool }
     invariant { disjoint accessible trashed }
     invariant { is_empty accessible -> not fullA }
     invariant { is_empty trashed -> not fullT }
     by { accessible = empty ; fullA = false ; trashed = empty ; fullT = false }

The state type includes invariants stating that empty sets are not full , which implies that their capacity is not 0.

Again the functions will work on a state type parameter rather than on shared state variables. Instead of returning a new state record they will mutate the fields of the parameter record (mutable fields make the parameter record somewhat similar to parameters passed by reference in C). Functions that do this are obliged to include in their contracts a writes clause, which lists the elements (parameter record fields) that are possibly written in calls to them. The postconditions make use of the **old** operator to refer to the values of parameters in the pre-state.

  val create (i : item) (state : stateT) : ()
    writes   { state.accessible, state.fullA }
    requires { not state.fullA }
    requires { not mem i (union state.accessible state.trashed) }
    ensures  { state.accessible = add i (old state.accessible)  }
    ensures  { state.trashed = old state.trashed }

  val delete (i : item) (state : stateT) : ()
    writes   { state.accessible, state.trashed,
               state.fullA, state.fullT }
    requires { not state.fullT }
    requires { mem i state.accessible }
    ensures  { state.accessible = remove i (old state.accessible) }
    ensures  { state.trashed = add i (old state.trashed) }

  val restore (i : item) (state : stateT) : ()
    writes   { state.accessible, state.trashed,
               state.fullA, state.fullT }
    requires { not state.fullA }
    requires { mem i state.trashed }
    ensures  { state.accessible = add i (old state.accessible) }
    ensures  { state.trashed = remove i (old state.trashed) }

  val empty (state : stateT) : ()
    writes   { state.trashed, state.fullT }
    requires { not (is_empty state.trashed) }
    ensures  { state.accessible = old state.accessible }
    ensures  { is_empty state.trashed }

end

In the implementation module,

we keep the item type undefined
in addition to an equality predicate eqi, we also declare an initialization function that returns the value with which the arrays will be initialized.
as well as the ghost fields originating in the specification, the state record now includes two arrays accessible_ and trashed, and the numbers sizea and sizet of elements currently stored in each of them.

The refinement invariant concerns the sets of elements stored in each array/set, but also their full status. The additional implementation invariants below are straightforward:

module Trash_Array
  (...) 
  type item
  val eqi (x y :item) : bool
    ensures { result <-> x=y }
  val function init () : item

  type stateT = { accessible_: array item;
                  mutable sizea: int;
                  trashed_: array item;
                  mutable sizet: int ;
                  ghost mutable accessible : fset item ;
                  ghost mutable fullA : bool ;
                  ghost mutable trashed : fset item ;
                  ghost mutable fullT : bool }
     
    (* Refinement correspondence *)
    invariant { accessible = elements accessible_ sizea /\
                trashed    = elements trashed_ sizet }
    invariant { (fullA <-> sizea = accessible_.length) /\  
                (fullT <-> sizet = trashed_.length) }
    (* Abstract (spec-level) invariants *)
    invariant { disjoint accessible trashed }
    invariant { is_empty accessible -> not fullA }
    invariant { is_empty trashed -> not fullT }
    (* Implementation invariants *)
    invariant { 0 < accessible_.length /\ 0 < trashed_.length }
    invariant { 0 <= sizea <= accessible_.length /\ 0 <= sizet <= trashed_.length }

    by { accessible_ = make 1 (init()) ; sizea = 0; 
         trashed_ = make 1 (init()) ; sizet = 0;          
         accessible = Fset.empty ; fullA = false ;
         trashed = Fset.empty ; fullT = false }

The action function definitions repeat the same contracts that are present in the abstract specification module. The ghost code must update the fullA and fullT variables in addition to the accessible and trashed sets.

Two two simpler functions are shown below:

  let create (i : item) (state : stateT)
    writes   { state.accessible, state.fullA,
               state.accessible_, state.sizea }
    requires { not state.fullA }
    requires { not mem i (union state.accessible state.trashed) }
    ensures  { state.accessible = add i (old state.accessible)  }
    ensures  { state.trashed = old state.trashed }
  =
    state.accessible_[state.sizea] <- i;
    state.sizea <- state.sizea + 1 ;
    state.accessible <- add i state.accessible ;
    if state.sizea = state.accessible_.length then state.fullA <- true 




 let empty (state : stateT)
    writes   { state.trashed, state.fullT,
               state.sizet }
    requires { not (is_empty state.trashed) }
    ensures  { state.accessible = old state.accessible }
    ensures  { is_empty state.trashed }
  =
    state.sizet <- 0 ; 
    state.trashed <- Fset.empty ;
    state.fullT <- false

Functions delete and restore require shifting a segment of one of the arrays in order to delete an element. They make use of WhyML references (imperative variables); loop invariants are required for their proofs of correctness. See the code in the links given below.

Once the functions have been defined, the implementation module clones the specification module, to establish the result that indeed it implements (or refines) the latter specification:

 clone Trash_model_impBound with
        type item,
        type stateT,
        val create,
        val delete,
        val restore,
        val empty

Before extracting OCaml code we still need to create a concrete implementation module that instantiates the item type, together with its equality predicate and initialization function:

module ExampleTrash
  use int.Int
  let function init () : int = 0

  clone Trash_Array with 
    type item = int, val eqi = (=) , val init 

end 

All the verification conditions generated from contracts and clone operations in these three modules are proved. We can now move to the extraction.

We assume the previous modules are in file trasharray.mlw , and an LLM chat has create an exemplification main function in file trasharrayMain.ml (which imports TrashArray).

% why3 extract -D ocaml64 trasharray.ExampleTrash -o trasharray.ml -L .

% ocamlbuild -pkg zarith trasharrayMain.native

% ./trasharrayMain.native 
Initial state:
Accessible: []
Trashed: []

After creating items 1, 2, and 3:
Accessible: [1, 2, 3]
Trashed: []

After deleting item 2:
Accessible: [1, 3]
Trashed: [2]

After restoring item 2:
Accessible: [1, 3, 2]
Trashed: []

After creating items 4 and 5:
Accessible: [1, 3, 2, 4, 5]
Trashed: []

After deleting items 1, 3, and 5:
Accessible: [2, 4]
Trashed: [1, 3, 5]

After emptying the trash:
Accessible: [2, 4]
Trashed: []

Files:

[trasharray.mlw](https://haslab.github.io/MFES/Why3/Extraction/trasharray.mlw)
[trasharray.ml](https://haslab.github.io/MFES/Why3/Extraction/trasharray.ml)
[trasharrayMain.ml](https://haslab.github.io/MFES/Why3/Extraction/trasharrayMain.ml)

Métodos Formais em Engenharia de Software

Mestrado em Engenharia Informática

Why3: Refinement and Code Extraction

An Imperative, Array-based Implementation