[Why3-club] request for comments

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Thu Sep 20 19:56:08 CEST 2012

> - couldn't the "{ }" be dropped entirely for pre/post?

not without a terminating symbol, since

	ensures p x = y

is a possible conflict between (ensures p x) = y i.e. with a body y and 
ensures (p x = y) with a postcondition being an equality

> - Yannick already pointed out the problem when the effects clause is the
> last one in the spec list;

in the design, we considered for a while using curly braces for effects 
as well (for symmetry, as Yannick pointed out) so we might go for it

> - couldn't the " = " move between the spec list and the expression?

as we said at the end of the email, the specification can be placed at 
three different places; file array.mlw was only one example, as close as 
possible to the current syntax

> - are "val" and "let" interchangeable now?

no; our proposal is to keep "val" for declarations, but to use it for 
toplevel declarations as well ("let" being used in "let in" only)

in particular, it eases the switch between declaration and definition, 
as the beginning (up to the spec) is now identical, as we already do 
with "function" and "predicate" when we add a definition to a previously 
uninterpreted symbol


More information about the Why3-club mailing list