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)
.
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;
}