Le 17/02/2021 à 13:44, Frank Pfenning a écrit :
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 purposes. Is there a way to do this? I couldn't find any notes on this in the manual or standard libraries. We are using Why3.1.3.3.
Why3 includes a `string` type since version 1.3, and there is the module io.StdIO in the standard library.
I don't think `why3 execute` supports those though (fell free to submit an issue) but extraction to OCaml supports it. For example
```hello.mlw let test () = print_string "Hello Why3 World"; print_newline () ``` can be extracted thanks to ``` why3 extract -D ocaml64 hello.mlw ``` giving the file ```hello.ml let test (_: unit) : unit = Pervasives.print_string "Hello Why3 World"; Pervasives.print_newline () ``` I hope that can be of some help in your use case - Claude _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
