# 9. Executing WhyML Programs

This chapter shows how WhyML code can be executed, either by being interpreted or compiled to some existing programming language.

## 9.1. Interpreting WhyML Code

Consider the program of Section 3.2 that computes the maximum and the sum of an array of integers. Let us assume it is contained in a file `maxsum.mlw`.

To test function `max_sum`, we can introduce a WhyML test function in module `MaxAndSum`

    let test () =
      let n = 10 in
      let a = make n 0 in
      a[0] <- 9; a[1] <- 5; a[2] <- 0; a[3] <- 2;  a[4] <- 7;
      a[5] <- 3; a[6] <- 2; a[7] <- 1; a[8] <- 10; a[9] <- 6;
      max_sum a n

and then we use the `execute` command to interpret this function, as follows:

    $ why3 execute maxsum.mlw --use=MaxAndSum 'test ()'
    result: (int, int) = (45, 10)
    globals:

We get the expected output, namely the pair `(45, 10)`.

Notice that the WhyML interpreter optionally supports Runtime Assertion Checking (RAC). This is detailed in Section 5.8.

## 9.2. Compiling WhyML to OCaml

An alternative to interpretation is to compile WhyML to OCaml. We do so using the `extract` command, as follows:

    why3 extract -D ocaml64 maxsum.mlw -o max_sum.ml

The `extract` command requires the name of a driver, which indicates how theories/modules from the Why3 standard library are translated to OCaml. Here we assume a 64-bit architecture and thus we pass `ocaml64`. We also specify an output file using option `-o`, namely `max_sum.ml`. After this command, the file `max_sum.ml` contains an OCaml code for function `max_sum`. To compile it, we create a file `main.ml` containing a call to `max_sum`, e.g.,

    let a = Array.map Z.of_int [| 9; 5; 0; 2; 7; 3; 2; 1; 10; 6 |]
    let s, m = Max_sum.max_sum a (Z.of_int 10)
    let () = Format.printf "sum=%s, max=%s@." (Z.to_string s) (Z.to_string m)

It is convenient to use ocamlbuild to compile and link both files `max_sum.ml` and `main.ml`:

    ocamlbuild -pkg zarith main.native

Since Why3’s type `int` is translated to OCaml arbitrary precision integers using the `ZArith` library, we have to pass option `-pkg zarith` to ocamlbuild. In order to get extracted code that uses OCaml’s native integers instead, one has to use Why3’s types for 63-bit integers from libraries `mach.int.Int63` and `mach.array.Array63`.

### 9.2.1. Examples

We illustrate different ways of using the `extract` command through some examples.

Consider the program of Section 3.6. If we are only interested in extracting function `enqueue`, we can proceed as follows:

    why3 extract -D ocaml64 -L . aqueue.AmortizedQueue.enqueue -o aqueue.ml

Here we assume that file `aqueue.mlw` contains this program, and that we invoke the `extract` command from the directory where this file is stored. File `aqueue.ml` now contains the following OCaml code:

    let enqueue (x: 'a) (q: 'a queue) : 'a queue =
      create (q.front) (q.lenf) (x :: (q.rear))
        (Z.add (q.lenr) (Z.of_string "1"))

Choosing a function symbol as the entry point of extraction allows us to focus only on specific parts of the program. However, the generated code cannot be type-checked by the OCaml compiler, as it depends on function `create` and on type `'a queue`, whose definitions are not given. In order to obtain a complete OCaml implementation, we can perform a recursive extraction:

    why3 extract --recursive -D ocaml64 -L . aqueue.AmortizedQueue.enqueue -o aqueue.ml

This updates the contents of file `aqueue.ml` as follows:

    type 'a queue = {
      front: 'a list;
      lenf: Z.t;
      rear: 'a list;
      lenr: Z.t;
      }

    let create (f: 'a list) (lf: Z.t) (r: 'a list) (lr: Z.t) : 'a queue =
      if Z.geq lf lr
      then
        { front = f; lenf = lf; rear = r; lenr = lr }
      else
        let f1 = List.append f (List.rev r) in
        { front = f1; lenf = Z.add lf lr; rear = []; lenr = (Z.of_string "0") }

    let enqueue (x: 'a) (q: 'a queue) : 'a queue =
      create (q.front) (q.lenf) (x :: (q.rear))
        (Z.add (q.lenr) (Z.of_string "1"))

This new version of the code is now accepted by the OCaml compiler (provided the `ZArith` library is available, as above).

### 9.2.2. Extraction of functors

WhyML and OCaml are both dialects of the ML-family, sharing many syntactic and semantics traits. Yet their module systems differ significantly. A WhyML program is a list of modules, a module is a list of top-level declarations, and declarations can be organized within scopes, the WhyML unit for namespaces management. In particular, there is no support for sub-modules in Why3, nor a dedicated syntactic construction for functors. The latter are represented, instead, as modules containing only abstract symbols [FP20]. One must follow exactly this programming pattern when it comes to extract an OCaml functor from a Why3 proof. Let us consider the following (excerpt) of a WhyML module implementing binary search trees:

    module BST
      scope Make
        scope Ord
          type t
          val compare : t -> t -> int
        end

        type elt = Ord.t

        type t = E | N t elt t

        use int.Int

        let rec insert (x: elt) (t: t)
        = match t with
          | E -> N E x E
          | N l y r ->
              if Ord.compare x y > 0 then N l y (insert x r)
              else N (insert x l) y r
          end
      end
    end

For the sake of simplicity, we omit here behavioral specification. Assuming the above example is contained in a file named `bst.mlw`, one can readily extract it into OCaml, as follows:

    why3 extract -D ocaml64 bst.mlw --modular -o .

This produces the following functorial implementation:

    module Make (Ord: sig type t
      val compare : t -> t -> Z.t end) =
    struct
      type elt = Ord.t

      type t =
      | E
      | N of t * Ord.t * t

      let rec insert (x: Ord.t) (t: t) : t =
        match t with
        | E -> N (E, x, E)
        | N (l, y, r) ->
            if Z.gt (Ord.compare x y) Z.zero
            then N (l, y, insert x r)
            else N (insert x l, y, r)
    end

The extracted code features the functor `Make` parameterized with a module containing the abstract type `t` and function `compare`. This is similar to the OCaml standard library when it comes to data structures parameterized by an order relation, e.g., the `Set` and `Map` modules.

From the result of the extraction, one understands that scope `Make` is turned into a functor, while the nested scope `Ord` is extracted as the functor argument. In summary, for a WhyML implementation of the form

    module M
      scope A
        scope X ... end
        scope Y ... end
        scope Z ... end
      end
      ...
    end

contained in file `f.mlw`, the Why3 extraction engine produces the following OCaml code:

    module A (X: ...) (Y: ...) (Z: ...) = struct
      ...
    end

and prints it into file `f__M.ml`. In order for functor extraction to succeed, scopes `X`, `Y`, and `Z` can only contain non-defined programming symbols, i.e., abstract type declarations, function signatures, and exception declarations. If ever a scope mixes non-defined and defined symbols, or if there is no surrounding scope such as `Make`, the extraction will complain about the presence of non-defined symbols that cannot be extracted.

It is worth noting that extraction of functors only works for modular extraction (i.e. with command-line option `--modular`).

### 9.2.3. Custom extraction drivers

Several OCaml drivers can be specified on the command line, using option `-D` several times. In particular, one can provide a custom driver to map some symbols of a Why3 development to existing OCaml code. Suppose for instance we have a file `file.mlw` containing a proof parameterized with some type `elt` and some binary function `f`:

    module M
      type elt
      val f (x y: elt) : elt
      let double (x: elt) : elt = f x x
      ...

When it comes to extract this module to OCaml, we may want to instantiate type `elt` with OCaml’s type `int` and function `f` with OCaml’s addition. For this purpose, we provide the following in a file `mydriver.drv`:

    module file.M
      syntax type elt "int"
      syntax val  f   "%1 + %2"
    end

OCaml fragments to be substituted for Why3 symbols are given as arbitrary strings, where `%1`, `%2`, etc., will be replaced with actual arguments. Here is the extraction command line and its output:

    $ why3 extract -D ocaml64 -D mydriver.drv -L . file.M
    let double (x: int) : int = x + x
    ...

When using such custom drivers, it is not possible to pass Why3 file names on the command line; one has to specify module names to be extracted, as done above.

## 9.3. Compiling to Other Languages

The `extract` command can produce code for languages other than just OCaml. This is a matter of choosing a suitable driver.

### 9.3.1. Compiling to C

Consider the following example. It defines a function that returns the position of the maximum element in an array `a` of size `n`.

    use int.Int
    use map.Map as Map
    use mach.c.C
    use mach.int.Int32
    use mach.int.Int64

    function ([]) (a: ptr 'a) (i: int): 'a = Map.get a.data.Array.elts (a.offset + i)

    let locate_max (a: ptr int64) (n: int32): int32
      requires { 0 < n }
      requires { valid a n }
      ensures  { 0 <= result < n }
      ensures  { forall i. 0 <= i < n -> a[i] <= a[result] }
    = let ref idx = 0 in
      for j = 1 to n - 1 do
        invariant { 0 <= idx < n }
        invariant { forall i. 0 <= i < j -> a[i] <= a[idx] }
        if get_ofs a idx < get_ofs a j then idx <- j
      done;
      idx

There are a few differences with a standard WhyML program. The main one is that the array is described by a value of type `ptr int64`, which models a C pointer of type `int64_t *`.

Among other things, the type `ptr 'a` has two fields: `data` and `offset`. The `data` field is of type `array 'a`; its value represents the content of the memory block (as allocated by `malloc`) the pointer points into. The `offset` field indicates the actual position of the pointer into that block, as it might not point at the start of the block.

The WhyML expression `get_ofs a j` in the example corresponds to the C expression `a[j]`. The assignment `a[j] = v` could be expressed as `set_ofs a j v`. To access just `*a` (i.e., `a[0]`), one could use `get a` and `set a v`.

For the access `a[j]` to have a well-defined behavior, the memory block needs to have been allocated and not yet freed, and it needs to be large enough to accommodate the offset `j`. This is expressed using the precondition `valid a n`, which means that the block extends at least until `a.offset + n`.

The code can be extracted to C using the following command:

    why3 extract -D c locate_max.mlw

This gives the following C code.

    #include <stdint.h>

    int32_t locate_max(int64_t * a, int32_t n) {
      int32_t idx;
      int32_t j, o;
      idx = 0;
      o = n - 1;
      if (1 <= o) {
        for (j = 1; ; ++j) {
          if (a[idx] < a[j]) {
            idx = j;
          }
          if (j == o) break;
        }
      }
      return idx;
    }

Not any WhyML code can be extracted to C. Here is a list of supported features and a few rules that your code must follow for extraction to succeed.

- Basic datatypes

  > - Integer types declared in `mach.int` library are supported for sizes 16, 32 and 64 bits. They are translated into C types of appropriate size and sign, say `int32_t`, `uint64_t`, etc.

  > - The mathematical integer type `int` is not supported.

  > - The Boolean type is translated to C type `int`. The bitwise operators from `bool.Bool` are supported.

  > - Character and strings are partially supported via the functions declared in `mach.c.String` library

  > - Floating-point types are not yet supported

- Compound datatypes

  > - Record types are supported. When they have no mutable fields, they are translated into C structs, and as such are passed by value and returned by value. For example the WhyML code

  >       use mach.int.Int32
  >       type r = { x : int32; y : int32 }
  >       let swap (a : r) : r = { x = a.y ; y = a.x }

  >   is extracted as

  >       #include <stdint.h>

  >       struct r {
  >         int32_t x;
  >         int32_t y;
  >       };

  >       struct r swap(struct r a) {
  >         struct r r;
  >         r.x = a.y;
  >         r.y = a.x;
  >         return r;
  >       }

  >   On the other hand, records with mutable fields are interpreted as pointers to structs, and are thus passed by reference. For example the WhyML code

  >       use mach.int.Int32
  >       type r = { mutable x : int32; mutable y : int32 }
  >       let swap (a : r) : unit =
  >          let tmp = a.y in a.y <- a.x; a.x <- tmp

  >   is extracted as

  >       struct r {
  >         int32_t x;
  >         int32_t y;
  >       };

  >       void swap(struct r * a) {
  >         int32_t tmp;
  >         tmp = a->y;
  >         a->y = a->x;
  >         a->x = tmp;
  >       }

  > - WhyML arrays are not supported

  > - Pointer types are supported via the type `ptr` declared in library `mach.c.C`. See above for an example of use.

  > - Algebraic datatypes are not supported (even enumerations)

- Pointer aliasing constraints

  > The type `ptr` from `mach.c.C` must be seen as a WhyML mutable type, and as such is subject to the WhyML restrictions regarding aliasing. In particular, two pointers passed as argument to a function are implicitly not aliased.

- Control flow structures

  > - Sequences, conditionals, `while` loops and `for` loops are supported

  > - Pattern matching is not supported

  > - Exception raising and catching is not supported

  > - `break`, `continue` and `return` are supported

### 9.3.2. Compilation of WhyML modules into Java classes

The `java` extraction driver is used to compile WhyML files into Java classes. The driver does not support flat extraction; thus, option `--modular` is mandatory. Each (non empty) module M is translated into a class with the same name. The imported modules are not translated unless the option `--recursive` is used. Since the extraction of a module requires data related to its dependencies, the option `--recursive` should be used systematically.

The code generated by the Java driver can be tuned using attributes. All attributes used by the Java driver are prefixed with `@java:`. Attributes not encountered in following examples are given in section WhyML Attributes.

In addition to the driver, new modules have been added to the Why3 Standard Library (see Extension of Why3 Standard Library).

#### 9.3.2.1. A running example

In order to illustrate the Java extraction, we implement a directory of some company. The directory contains employees and each of them stores the name of the person and its service in the company, its phone number and the number of its office.

We first create the module for the data structure that will store employees; the WhyML code is given below. The module defines a type `t` that is a record with 4 fields, `name`, `room`, `phone` and `service`. For the first three fields, we use types (`integer` and `string`) that mimics those of the Java language; they are defined in modules that come along with the driver (see Extension of Why3 Standard Library).

The type of the field `service` is defined by an algebraic type. The driver permits to declare inner `Enum` classes using algebraic types of the WhyML language. Only algebraic constructors with no arguments are allowed i.e the type is just an enumeration of identifiers. `Enum` classes are the only form allowed by the driver.

We define a function `create_member` whose purpose is to create a record of type `t`. This function is kinda redundant with the WhyML syntax that permits to build such record directly using the usual constructor (`{ ... }`). The reader should have noticed the attribute `java:constructor` attached to the function. It is used to mark functions that should yield Java constructors. The driver allows only such marked functions to build records.

    module Employee
      use mach.java.lang.Integer
      use mach.java.lang.String

      type service_id = HUMAN_RES | TECHNICAL | BUSINESS

      type t = {
        name: string;
        room: integer;
        phone : string;
        service : service_id;
      }

      let create_employee [@java:constructor] (name : string) (room : integer) (phone : string)
                                              (service : service_id) = {
        name = name; room = room; phone = phone; service = service;
      }
    end

We assume that the entire WhyML code described in this section is stored in a file `./directory.mlw`. We generate the file `Employee.java` using the following command (according to the option -o the file is created in the current directory).

    $ why3 extract -L . -D java -o . --recursive --modular directory.Employee

`extract` produces the Java code described below. After the header of the class `Employee` comes the definition of the `ServiceId` that correspond to the algebraic type `service_id`. Note that identifiers are translated using camel case.

    /* This file has been extracted from module Employee. */
    public class Employee {

      public enum ServiceId
      {
         HUMAN_RES,
         TECHNICAL,
         BUSINESS
      }

To be consistent with WhyML semantics the fields of the type `Employee.t` have been translated as `final` instance variables. When a field of a record is `mutable` then so is the corresponding instance variable.

      public final String name;
      public final int room;
      public final String phone;
      public final ServiceId service;

As a rule of thumb, the first type definition encountered by the driver is assumed to be the type of the generated class. Usually this type is a record, the fields of which are translated as instance variables. Abstract types can also be used when the expected class does not store any data (e.g. an exception) or when one wants to generate an interface (see attribute `java:class_kind:`). Since the driver looks for the first type definition, it can be difficult to use module cloning because new types may be added by this mechanism. The definition of a type for the class is not mandatory when one wants to gather a collection of static methods.

In order to make generated classes usable with Java containers (especially those implemented in Extension of Why3 Standard Library) the driver produces systematically the methods `equals` and `hashCode`. The implementation of these methods for `Employee` objects is given below. These methods are specified `final` to prevent their redefinition. Note that these methods are not available from the WhyML code.

      public final boolean equals(Object obj) {

        if (this == obj) {
          return true;
        }
        if (obj == null) {
          return false;
        }
        if (!(this.getClass() == obj.getClass())) {
          return false;
        }

        Employee other = (Employee) obj;
        if (!(this.name == null ? other.name == null : this.name.equals(other.name))) {
          return false;
        }
        if (!(this.room == other.room)) {
          return false;
        }
        if (!(this.phone == null ? other.phone == null : this.phone.equals(
                                                         other.phone))) {
          return false;
        }
        if (!(this.service == other.service)) {
          return false;
        }
        return true;

      }
      public final int hashCode() {
        int hashValue = 1;
        hashValue = 31 * hashValue + (this.name == null ? 0 : this.name.hashCode());
        hashValue = 31 * hashValue + this.room;
        hashValue = 31 * hashValue + (this.phone == null ? 0 : this.phone.hashCode());
        hashValue = 31 * hashValue + this.service.hashCode();
        return hashValue;
      }

Finally the driver translates `create_employee` into a constructor of `Employee` objects. During this translation, the identifier of functions annotated with the attribute `java:constructor` is lost. This allows to declare several constructors with different signatures.

      public Employee(String name, int room, String phone, ServiceId service) {

        this.name = name;
        this.room = room;
        this.phone = phone;
        this.service = service;
      }
    }

We now focus on the module implementing the directory. We use a `Map` container to associate to a name (a `string`) an Employee. The container, specified in the module mach.java.util.Map, partially mimics the container from the JDK.

A directory is simply a record with only one field `employees` (see section `extraction:preserve_single_field` for a detailed description of this attribute). We use the attribute `java:visibility:private` to avoid direct access to `employees`.

We also define a method `add_employee` that permits to insert a new entry into the directory. The contract of the method requires that no entry already exists the same employee’s name and ensures a new entry with given data has been added.

    module Directory
      use int.Int
      use mach.java.lang.String
      use mach.java.lang.Integer
      use mach.java.util.Map
      use Employee

      type t [@extraction:preserve_single_field]= {
        employees [@java:visibility:private] : Map.map string Employee.t
      }

      let create_directory [@java:constructor] () : t = {
        employees = Map.empty()
      }

      let add_employee (self : t) (name : string) (phone : string) (room : integer)
                                  (service : service_id) : unit
        requires { not Map.containsKey self.employees name }
        ensures { Map.containsKey self.employees name }
        ensures { let m = Map.get self.employees name in
                   m.name = name && m.phone = phone && m.room = room  && m.service = service }
      =
        Map.put self.employees name (Employee.create_employee name room phone service)
    end

The Java code extracted from this specification is the following (the code of methods `equals` and `hashCode` has been suppressed).

    /* This file has been extracted from module Directory. */
    import java.util.Map;
    import java.util.HashMap;
    public class Directory {

      private final Map<String,Employee> employees;
      public Directory() {

        this.employees = new HashMap<> ();
      }

      public void addEmployee(String name, String phone, int room,
                              Employee.ServiceId service) {

        this.employees.put (name, new Employee(name, room, phone, service));
      }
    }

The reader should have noticed that the contract of `add_employee`. This not surprising since `extract` removes all ghost code. In the context of a WhyML program we are guaranteed that `add_employee` is called with parameters that satisfy the precondition of the function (i.e. `name` is not an entry of the directory). However, if this method is invoked from a client code that has not been generated with `extract`, we should add explicitly the verification of the precondition.

Let fix this issue by modifying `add_employee` in such a way it raises an exception if the precondition is not fulfilled. First, we create the class for the exception `EmployeeAlreadyExistsException`:

    module EmployeeAlreadyExistsException [@java:exception:RuntimeException]
      use mach.java.lang.String

      type t [@extraction:preserve_single_field] = { msg : string }

      exception E t

      let constructor[@java:constructor](name : string) : t = {
        msg = (String.format_1 "Employee '%s' already exists" name)
      }

      let getMessage(self : t) : string = self.msg
    end

The creation of an exception for Java extraction is based on two points:

1. Firstly, it requires to annotate the module with the attribute `java:exception:` exn-class. The suffix of this attribute indicates the class from which the generated exception inherits. This suffix is not interpreted and is printed out as-is by the driver. In our example, we just want the exception to inherit from the standard `RuntimeException` from the JDK.

2. Secondly, the module must define a WhyML exception, `E` in our example. As for standard classes, it is possible to declare instance variables in exceptions. In our example, `EmployeeAlreadyExistsException` stores an information message.

    /* This file has been extracted from module EmployeeAlreadyExistsException. */
    public class EmployeeAlreadyExistsException extends RuntimeException {

      public final String msg;

      public EmployeeAlreadyExistsException(String name) {

        this.msg = String.format("Employee '%s' already exists", name);
      }

      public String getMessage() {

        return this.msg;
      }
    }

The implementation of the method `add_employee` can now be updated. First, the contract is changed: the precondition has been removed and replaced by an exceptional postcondition that relates the occurrence of an exception `EmployeeAlreadyExistsException` with an invalid value of the parameter `name`. Then, before the creation of an new entry, we check if `name` already exists in the directory, in which case an exception is raised.

      use EmployeeAlreadyExistsException

      let add_employee (self : t) (name : string) (phone : string) (room : integer)
                                  (service : service_id) : unit
        ensures { Map.containsKey self.employees name }
        ensures { let m = Map.get self.employees name in
                   m.name = name && m.phone = phone && m.room = room  && m.service = service }
        raises { EmployeeAlreadyExistsException.E _ -> Map.containsKey (old self.employees) name }
      =
        if Map.containsKey self.employees name then
          raise (EmployeeAlreadyExistsException.E (constructor name));
        Map.put self.employees name (Employee.create_employee name room phone service)

The Java code extracted from this new implementation is given below. Two things have been added to the original method. First, the declaration of the exception in the signature of the function and second, the translation of the test related to the parameter `name`.

      public void addEmployee(String name, String phone, int room,
                              Employee.ServiceId service) throws EmployeeAlreadyExistsException {

        if (this.employees.containsKey (name)) {
          throw new EmployeeAlreadyExistsException(name);
        }
        this.employees.put (name, new Employee(name, room, phone, service));
      }

#### 9.3.2.2. Extension of Why3 Standard Library

Several modules have been implemented to ease the extraction of Java classes. They are gathered accroding to JDKL’s packages.

Library mach.java.lang defines types for bounded integers used in Java (`Short`, `Integer` and `Long`) and also strings (`String`) but the latter are limited to formatting methods. Another important module is mach.java.lang.Array that must be used in place of Java bounded size arrays. There are also some standard exceptions that are used by others modules.

Library mach.java.util gathers some containers (like `Map` used in this section). In the specification of these containers we tried to stick to Java semantics. In particular, according to the specification of java.util.Collection.size():

    int size()
      Returns the number of elements in this collection. If this collection
      contains more than Integer.MAX_VALUE elements, returns Integer.MAX_VALUE.

    Returns:
      the number of elements in this collection