[Why3-club] Interpreter for why3 code?

Alan Schmitt alan.schmitt at polytechnique.org
Thu Mar 13 11:57:17 CET 2014


Jean-Christophe Filliatre <Jean-Christophe.Filliatre at lri.fr> writes:

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

Great, thanks a lot!

Alan



More information about the Why3-club mailing list