2.7. Surface grammar🔗

The transcription below normalises the layout directives in LaurelGrammar.st. { X } means zero or more, [ X ] optional, and X , ... a comma-separated list. A file is a sequence of declarations with no separator between them; each declaration's own terminator (; for a procedure, the closing brace or the next leading keyword otherwise) delimits it.

program             = { declaration } ;

declaration         = procedure-declaration
                    | coroutine-declaration
                    | composite-declaration
                    | datatype-declaration
                    | constrained-type-declaration
                    | type-alias-declaration
                    | opaque-type-declaration
                    | global-variable-declaration ;

(* Types *)

type                = "int" | "bool" | "real" | "float64" | "string"
                    | "bv" natural
                    | "TotalMap" type type
                    | "Core" identifier
                    | identifier
                    | identifier "<" type , ... ">"
                    | "(" type ")" ;

type-parameters     = "<" identifier , ... ">" ;

(* Type, alias, and global declarations *)

datatype-declaration
                    = "datatype" identifier [ type-parameters ]
                      "{" [ constructor , ... ] "}" ;
constructor         = identifier | identifier "(" [ argument , ... ] ")" ;
argument            = identifier ":" type ;

constrained-type-declaration
                    = "constrained" identifier "=" identifier ":" type
                      "where" expression "witness" expression ;

type-alias-declaration
                    = "type" identifier [ type-parameters ] "=" type ;

opaque-type-declaration
                    = "opaque" identifier [ type-parameters ] ;

global-variable-declaration
                    = "var" identifier ":" type [ ":=" expression ] ;

(* Composites *)

composite-declaration
                    = "composite" identifier [ type-parameters ]
                      [ "extends" type , ... ]
                      "{" { field-declaration } { procedure-declaration } "}" ;
field-declaration   = [ "var" ] identifier ":" type ;

(* Procedures: the clause order below is significant *)

procedure-declaration
                    = "procedure" identifier [ type-parameters ]
                      "(" [ parameter , ... ] ")"
                      [ ":" type ]
                      [ "returns" "(" [ parameter , ... ] ")" ]
                      [ "throws" "(" identifier ":" type ")" ]
                      { requires-clause }
                      [ "invokeOn" expression ]
                      [ "entry" ]
                      [ opaque-specification ]
                      [ body | "external" ]
                      ";" ;

parameter           = identifier ":" type ;
body                = expression ;

requires-clause     = [ "free" | "checked" ] "requires" expression
                      [ "summary" string-literal ] ;

opaque-specification
                    = "opaque"
                      { ensures-clause }
                      { modifies-clause }
                      { throws-on-clause }
                      { "reads" identifier , ... }
                      { "writes" identifier , ... } ;

ensures-clause      = [ "free" | "checked" ] "ensures" expression
                      [ "summary" string-literal ] ;
modifies-clause     = "modifies" "*" | "modifies" expression , ... ;

throws-on-clause    = "throwsOn" expression "{" { throws-on-spec } "}" ;
throws-on-spec      = "ensures" expression [ "summary" string-literal ]
                    | "modifies" expression , ... ;

(* Coroutines *)

coroutine-declaration
                    = "coroutine" identifier "(" [ parameter , ... ] ")"
                      [ "yields" "(" [ parameter , ... ] ")" ]
                      [ "resumes" "(" [ parameter , ... ] ")" ]
                      { requires-clause } { ensures-clause }
                      { relies-clause } { guarantees-clause }
                      { modifies-clause }
                      [ body | "external" ]
                      ";" ;
relies-clause       = "relies" expression [ "summary" string-literal ] ;
guarantees-clause   = "guarantees" expression [ "summary" string-literal ] ;

(* Unified statements and expressions *)

expression          = literal
                    | identifier
                    | "(" expression ")"
                    | variable-declaration
                    | expression "(" [ expression , ... ] ")"
                    | "new" identifier [ "<" type , ... ">" ]
                    | expression "#" identifier
                    | assignment
                    | compound-assignment
                    | multi-assignment
                    | increment-expression
                    | unary-expression
                    | binary-expression
                    | quantifier
                    | "old" "(" expression ")"
                    | "oldGuarantee" "(" expression ")"
                    | "oldRelies" "(" expression ")"
                    | if-expression
                    | "assert" expression [ "summary" string-literal ]
                    | "assume" expression
                    | "throw" expression
                    | "return" [ expression ]
                    | "yield"
                    | block
                    | block identifier
                    | "exit" identifier
                    | try-expression
                    | while-loop
                    | for-loop
                    | do-while-loop
                    | expression "is" type
                    | expression "as" type ;

literal             = "true" | "false" | natural | decimal | string-literal
                    | natural "bv" natural
                    | "<?>" | "<??>" ;

variable-declaration
                    = "var" identifier [ ":" type ] [ ":=" expression ] ;

assignment          = expression ":=" expression ;
compound-assignment = expression compound-operator expression ;
compound-operator   = "+=" | "-=" | "*=" | "/=" | "%=" | "^=" ;

multi-assignment    = "assign" assignment-target , ... ":=" expression ;
assignment-target   = "var" identifier [ ":" type ]
                    | identifier
                    | field-path "#" identifier ;
field-path          = identifier | field-path "#" identifier ;

increment-expression
                    = "++" expression | "--" expression
                    | expression "++" | expression "--" ;

unary-expression    = "!" expression | "-" expression ;

binary-expression   = expression binary-operator expression ;
binary-operator     = "+" | "-" | "*" | "/" | "%" | "/t" | "%t"
                    | "==" | "!=" | "<" | "<=" | ">" | ">="
                    | "&" | "|" | "&&" | "||" | "==>"
                    | "^" ;

quantifier          = ( "forall" | "exists" ) "(" identifier ":" type ")"
                      [ "{" expression "}" ] "=>" expression ;

if-expression       = "if" expression "then" expression
                      [ "else" expression ] ;

block               = "{" [ expression { ";" expression } ] "}" ;

try-expression      = "try" expression { catch-clause } [ finally-clause ] ;
catch-clause        = "catch" identifier [ "when" expression ] expression ;
finally-clause      = "finally" expression ;

while-loop          = "while" "(" expression ")" { invariant-clause }
                      expression ;
for-loop            = "for" "(" expression ";" expression ";" expression ")"
                      { invariant-clause } expression ;
do-while-loop       = "do" expression "while" "(" expression ")"
                      { invariant-clause } ;
invariant-clause    = "invariant" expression ;

A few points the productions alone do not make obvious:

• A single anonymous output (: T) and named outputs (returns (...)) are separate optional slots, but they are alternative user forms. Do not write both.

• Fields must precede procedures inside a composite.

• A procedure body is one expression. Most imperative procedures use a block, which is also an expression.

• A return carries no semicolon of its own; semicolons only separate it from neighbouring expressions in a block.

• A datatype constructor with no arguments may be written Nil or Nil().

• A multi-assignment field target is a plain identifier/field chain, not an arbitrary expression.

• A local variable's : type annotation is grammatically optional, but an unannotated var with no initializer cannot be given a type and is diagnosed. Write the annotation, or use var x := e and let the initializer supply it.

• yield, yields, resumes, relies, guarantees, oldGuarantee, and oldRelies are coroutine-only; see Coroutines.