[Why3-club] request for comments

Johannes Kanig kanig at adacore.com
Thu Sep 20 18:46:04 CEST 2012

Hello Andrei,

On 09/20/2012 05:07 PM, Andrei Paskevich wrote:
> We would like to make a change to the syntax of specifications in WhyML.
> Before doing so, we would appreciate comments from our users,
> especially those who produce Why3 syntax automatically (e.g. Adacore)
> as well as those who already have a corpus of WhyML programs.

Actually, at AdaCore we are in both categories. But I suspect that for
both it's OK: changing the pretty printer seems simple enough, and
changing the Why3 declarations in our handwritten Why3 code (this is
mainly Claire's container library) should be pretty straightforward as
well (but may take an hour or so of manual work).

Just a few random comments:
- on the example (e.g. "fill"), I find it difficult to find the
beginning of the program function, or to decide if there even is one;
- couldn't the "{ }" be dropped entirely for pre/post?
- Yannick already pointed out the problem when the effects clause is the
last one in the spec list;
- couldn't the " = " move between the spec list and the expression?
- are "val" and "let" interchangeable now? I would prefer stricter
rules: "val" only for declarations, "let" for definitions.


Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list