[Why3-club] Interpreter for why3 code?
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)
> 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!
More information about the Why3-club