[Why3-club] request for comments
moy at adacore.com
Thu Sep 20 17:55:27 CEST 2012
Hello Andrei and Jean-Christophe,
This change looks good to me. Maybe add braces around reads and writes
arguments for more symmetry, and to avoid having a comma change a lot
the parsing, like between
val f () : int = reads x y z
val f () : int = reads x, y z
I think your proposed change will make it easier to read the generated
Why3 code, by having function declarations where the return type comes
before the precondition, and pre/postconditions together.
I'll let Johannes comment further.
Yannick Moy, Senior Software Engineer, AdaCore
More information about the Why3-club