[Why3-club] Interpreter for why3 code?
Jean-Christophe.Filliatre at lri.fr
Thu Mar 13 11:23:40 CET 2014
> 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).
More information about the Why3-club