Program functions can be declared as partial with "let/val partial".
Similarly to "diverges", partial code cannot be ghost, however it does not need to be
explicitly specified as partial.
Fixes#184.
Without an argument, break and continue refer to the innermost loop.
A label put over an expression sequence starting with a loop, can be
used as an optional argument for break and continue:
label L in
[ghost] ["tag"] [M.begin]
while true do
...
break L
...
done;
[...]
[end] [: unit]
In the square brackets are listed the constructions allowed between
the label declaration and the loop expression.
To install the Why3-related Vim files, just create a symbolic link:
ln -s "$(why3 --print-datadir)/vim" ~/.vim/bundle/why3
Thanks to Johanness Kanig for the suggestion.
The only recent change in master currently ignored in
this merge is renaming mach.Array.Array63.array to array63.
If we decide to give array types in mach.Array specific names,
we should do it for every size, and not only for 63 bits.
The old syntax: abstract expr [spec]...
The semicolon binds more loosely than "abstract" and
the specification clauses are optional, so that
"abstract e1; e2" is the same as "(abstract e1); e2"
and "abstract e1; e2; ensures {...}" is a syntax error.
The new syntax: abstract [spec]... expr end
This allows to put sequences of expressions under "abstract"
without ambiguity and moves the specification clauses to the
beginning. In other words, "abstract" becomes a "begin" with
a specification attached. The spec-at-the-top is consistent
with the syntax of functions and the whole seems to be more
natural for the intented use of "abstract" (a logical cut).
- "diverges" states that the computation may not terminate (which
does not mean that is always diverges: just as any other effect
annotation, this clause states a possibility of a side effect).
- "reads {}" states that the computation does not access any variable
except those that are listed elsewhere in the specification (or the
proper function arguments, if "reads" is in a function spec).
- "writes {}" states that the computation does not modify any mutable
value.
- If a function definition or an abstract computation may diverge,
but there is no "diverges" clause in the specification, a warning
is produced. If a function definition or an abstract computation
always terminates, but there is a "diverges" clause in the spec,
an error is produced.
- If there is a "reads" or a "writes" clause in a function definition
or an abstract computation, then every modified value must be listed
in "writes" and every accessed external variable not mentioned in
the spec must be listed in "reads". (Notice that this is a stricter
requirement than before, when the presence of a "writes" clause
did not require to specify "reads".) However, one does not have to
write "reads {}" or "writes {}" if the corresponding lists are empty.
