Previous Up Next

Chapter 8  Executing WhyML Programs

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

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

8.1  Interpreting WhyML Code

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 MaxAndSum.test
Execution of MaxAndSum.test ():
     type: (int, int)
   result: (45, 10)

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

8.2  Compiling WhyML to OCaml

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

> mkdir dir
> why3 extract -D ocaml64 maxsum.mlw -o dir

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. On a 32-bit architecture, we would use ocaml32 instead. Extraction also requires a target directory to be specified using option -o. Here we pass a freshly created directory dir.

Directory dir is now populated with a bunch of OCaml files, among which we find a file containing the OCaml code for functions max_sum and test.

To compile it, we create a file containing a call to test, that is, for example,

let (s,m) = test () in Format.printf "sum=%s, max=%s@." (Why3__BigInt.to_string s) (Why3__BigInt.to_string m)

and we pass both files and to the OCaml compiler:

> cd dir
> ocamlopt zarith.cmxa why3extract.cmxa

OCaml code extracted from Why3 must be linked with the library why3extract.cmxa that is shipped with Why3. It is typically stored in subdirectory why3 of the OCaml standard library. Depending on the way Why3 was installed, it depends either on library nums.cmxa or zarith.cmxa for big integers. Above we assumed the latter. It is likely that additional options -I must be passed to the OCaml compiler for libraries zarith.cmxa and why3extract.cmxa to be found. For instance, it could be

> ocamlopt -I `ocamlfind query zarith` zarith.cmxa \
           -I `why3 --print-libdir`/why3 why3extract.cmxa \

To make the compilation process easier, one can write a Makefile which can include informations about Why3 configuration as follows.

WHY3SHARE=$(shell why3 --print-datadir) include $(WHY3SHARE)/Makefile.config maxsum: ocamlopt $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa \ -o maxsum

Previous Up Next