[Why3-club] request for comments

Andrei Paskevich andrei at tertium.org
Thu Sep 20 20:16:32 CEST 2012


On 20 September 2012 18:46, Johannes Kanig <kanig at adacore.com> wrote:
> 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;

The equality sign at the end of the first line guarantees that there
is a body. We can also keep using "val" for declarations and "let" for
definitions, if that helps clarity.

As for finding the beginning of the program body after a series of
specification clauses, do you see how to make it better? One
possibility is to put the equality sign after the spec, as follows:

val rec length (l : list int) : int
  ensures { result = length l }
  variant { l }
= match l with ...

This is already accepted by the proposed syntax, and has the added
benefit that you can convert a definition into a declaration simply by
putting a pair of (* *) around the body (provided that we use "val
[rec]" for both definitions and declarations). We can even be stricter
and _require_ the spec to be put between the result type and the
equality. It is all the more justified, since the spec does not really
belong to the body (unlike "assert" or "check"). My only grudge with
this is that I (personally) find the style a bit ugly.

Another possibility is to keep with the proposal and rely on
indentation and coloring for visual cues:

val rec length (l : list int) : int =
    ensures { result = length l }
    variant { l }
  match l with ...

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

No, that would create unresolvable conflicts:

let double x = ensures result = x + x x + x

let double x ensures result = x + x = x + x

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

I think, we can require braces in the effect clauses. Alternatively,
if the spec is only allowed before the equality, the problem
disappears.

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

It can. Notice the "spec" at the end of the rule for "signature".

> - are "val" and "let" interchangeable now? I would prefer stricter
> rules: "val" only for declarations, "let" for definitions.

The idea was to use "val" both for definitions and declarations, and
to forbid "let" at the top level altogether (the "let fill" you saw in
the example was us being clumsy). But that change is orthogonal to the
rest of the proposal and can be discarded.

Andrei



More information about the Why3-club mailing list