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.
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)
globals:
We get the expected output, namely the pair (45, 10).
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 maxsum__MaxAndSum.ml containing the OCaml code for functions max_sum and test.
To compile it, we create a file main.ml 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 maxsum__MaxAndSum.ml and main.ml to the OCaml compiler:
> cd dir > ocamlopt zarith.cmxa why3extract.cmxa maxsum__MaxAndSum.ml main.ml
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 maxsum__MaxAndSum.ml main.ml |