• Andrei Paskevich's avatar
    WhyML: change the syntax of "abstract" · 4fd8b24d
    Andrei Paskevich authored
    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).
    4fd8b24d
why3.vim 8.79 KB