We are using WhyML/Why3 in a course on Bug Catching at CMU,
and one of the students asked if it was possible to insert print
statements into their code. Presumably, they'd want the interpreter
(why3 execute) to show them the value of variables at certain points
in the program for debugging purpose
Dear Frank,
I am not sure this can be done at the WhyML-level, even with `why3
execute`.
One possibility is to extract your WhyML program into OCaml via `why3
extract` (http://why3.lri.fr/doc/exec.html#compiling-whyml-to-ocaml). You
can then manipulate the extracted code, in order to introduce so
Thanks, Mário! If there is a print statement as indicated in the 2018
paper, I couldn't find
a way to access it. The other path seems doable. Not that I am generally
advocating
print statement as a debugging tool, but desperate situations sometimes
call for
desperate measures.
- Frank
On Wed
Le 17/02/2021 à 18:48, Frank Pfenning a écrit :
> Thanks, Mário! If there is a print statement as indicated in the 2018
> paper, I couldn't find a way to access it.
It is only available for reflection-based proofs. (No good reason, it
just never got ported to the other execution engines.) So, if y
> (No good reason, it just never got ported to the other execution
engines.)
Maybe this thread should be considered as a bug report asking for it to be
available in all execution engines?
(Being able to easily print stuff sounds like a reasonable need to test
programs.)
On Wed, Feb 17, 2021 at 9:
