[Why3-club] request for comments

Yannick Moy 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 mailing list