Semicolons

Semicolons ; are used to separate statements in a block, conditions in a pre-condition, post-condition, invariant or check clause and to separate index variable entries in for loops. Semicolons are not required in most cases, but are sometimes necessary to avoid ambiguity.

Situations Requiring a Semicolon

Calls without arguments

A call to a feature that does not require any arguments consists of the feature name and nothing else, as in

  a

This is a problem if the parser could interpret the call as something else, e.g., a field declaration:

  a b

which can be interpreted as a call to a followed by a call to b or as the declaration of a field a of type b

Calls followed by parenthesis

Also problematic is destructuring a tuple

  a
  (x,y) = some_tuple

which can be parsed as a call to a with arguments x,y.

Similar is an expression in parentheses whose result is ignored:

  a
  (expr)

Solutions

Requiring a Semicolon

The easiest solution is to just require the semicolon as in

  a; b;
  a;
  (x,y) = some_tuple;
  a;
  (expr);

to make sure a is parsed as a call in all three cases.

Changing Syntax for Conflicting Cases

We could keep the call syntax, and change the syntax of anything that could result in a conflict, e.g.,

  var a b

for a declaration

  _ = (expr)

for an ignored expression result. Tuple destructuring can be detected by increasing the parser's lookahead. Then

  a b
  a
  (x,y) = some_tuple
  a
  _ = (expr)

would parse all three occurrences of a as calls while

  var a b
  a
  (x,y)
  a
  (expr)

would parse the three as as a declared field, a call with two arguments and a call with a single argument, respectively.

LF as statement delimiters

Well formatted code for a call that extends over several lines would indent the code from the second line onwards compared to the first line. We could hence interpret the lack of such indentation as the developer's wish to start a new statement. Then, the code becomes

  a; b
  a
  (x,y) = some_tuple
  a
  (expr)

to ensure that a is a call in all cases.

A call with a linebreak must use indentation:

  call_with2_arguments
    (argument1, argument2)

  call_with1_argument
    (argument)

While a field declaration has to be within one single line

  field type

or has to use deeper indentation in the following lines

  field_with_a_very_long_name
    type_with_a_long_name_used_for_field_with_very_long_name