[Why3-club] Interpreter for why3 code?

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Thu Mar 13 11:23:40 CET 2014


Hi Alan,

> Is there an easy way to interpret why3 code? I don't want a full fledged
> extraction to OCaml, but would like to be able to have students test
> their algorithms before they prove them.

Yes, there is. Option --exec allows you to interpret WhyML programs.
It is available (and documented) in the developement version of Why3,
and we should make a new release very soon.

Here is an example:

why3 examples/vstte10_max_sum.mlw --exec TestCase.test
Execution of TestCase.test ():
     type: (int, int)
   result: Tuple2(45, 10)
  globals:

Namely: you specify a function with a single argument of type unit (here
TestCase.test), it is interpreted, and its output (including global
side-effects) is displayed.

See chapter 8 of the manual (which also documents extraction to OCaml code).

-- 
Jean-Christophe



More information about the Why3-club mailing list