Expressions

Expressions produce either an integer or boolean value, and can be used as part of the statement or method pre- and post-conditions.

Expressions are heavily influenced by how rust handles expressions, albeit a bit simiplified.

Grammar

// currently no distinction in the grammar
BOOL_EXPR           :=  EXPR
ARITH_EXPR          :=  EXPR

EXPR                :=  TERM_EXPR [OP EXPR]?

TERM_EXPR           := NUM_LITERAL_EXPR
                     | BOOL_LITERAL_EXPR
                     | FN_CALL_EXPR
                     | SLICE_EXPR
                     | ELEMENT_EXPR
                     | IDENT_EXPR

NUM_LITERAL_EXPR    := NUMBER
BOOL_LITERAL_EXPR   := BOOLEAN
FN_CALL_EXPR        := IDENT LPAREN [EXPR [COMMA EXPR]* ]? RPAREN
SLICE_EXPR          := IDENT RBRAK RANGE_EXPR LBRAK
RANGE_EXPR          := ARITH_EXPR DOTDOT ARITH_EXPR
ELEMENT_EXPR        := IDENT RBRAK ARITH_EXPR LBRAK
IDENT_EXPR          := IDENT

Operator Precedence

The operator precedence roughly follows the Rust model.

PrecedenceOperatorsAssociativityExample
StrongField expressionleft to righta.b.c
Fn Calls / Arraya() a[]
Unary ! & ~!a ~a &a
Multiply / Divleft to righta * b a / b a % b
Plus Minusleft to righta + b a - b
Shiftsleft to righta << b a >> b
Bitwise Andleft to righta & b
Bitwise Xorleft to righta ^ b
Bitwise Orleft to righta \| b
ComparisonsRequire parenthesisa == b a != b a < b a > b a <= b a >= b
Logical Andleft to righta && b
Logical Orleft to right`a
Impliesleft to righta ==> b
WeakRange ExpressionRequire parenthesisa..b

Quantifier Expressions

A quantifier expression produces a boolean value based on whether the mathematical quantifier expression (forall or exists) holds.

Grammar

QUANTIFIER_EXPR := FORALL_EXPR | EXISTS_EXPR

FORALL_EXPR := KW_FORALL ARGLIST PATHSEP BOOL_EXPR
EXISTS_EXPR := KW_EXISTS ARGLIST PATHSEP BOOL_EXPR

Example

forall x : int :: a + x > 0