Expressions

Every expression has a type that can be uniquely determined from the expression itself, provided the expression is well-formed and well-typed.

Expression ::=
  | Literal
  | Id
  | OperatorExpr
  | FunctionCall
  | LabeledExpr
  | LetExpr
  | QuantifierExpr
  | "(" Expression ")"

Literal expressions

Literal ::=
  | false | true
  | 0 | 1 | 2 | ...
  | "|" LiteralIdentifier ":" Type "|"

The literals false and true have the built-in type bool.

Natural numbers have the built-in type int. They are unbounded integers. Negative integers can be formed using the unary-minus operator.

B3 has very few built-in types. For user-defined types, one way to define specific values is to define a nullary function for each such value, optionally tagging the functions to indicate that they give distinct values. For example,

type Airport
tagger AirportTag for Airport

function SEA(): Airport tag AirportTag
function CFG(): Airport tag AirportTag
function NBO(): Airport tag AirportTag
// ...

or

type real
tagger realTag for real

function Zero(): real tag realTag
function Seventeen(): real tag realTag
function OneHalf(): real tag realTag
function r_12_508(): real tag realTag
function Pi(): real tag realTag
// ...

However, when the number of values is large—indeed, perhaps infinite—then this approach is at best clumsy. To address this issue and yet remain mostly agnostic about the details of non-built-in types, B3 supports custom literals.

A custom literal is an identifier-like token with a given type. Syntactically, the identifier-like token is just a string of input characters; B3 does not further parse or interpret this string by itself. But when the same identifier-like token is used in multiple places for the same type, B3 interprets them as having the same value. For example, the following is always provable:

check |ARN: Airport| == |ARN: Airport|

B3 does not say whether or not two custom literals with different identifier-like tokens are equal. That is, in general, neither of the following checks is provable:

check |three: real| == |3.0: real| // not provable
check |three: real| != |3.0: real| // not provable

Syntactically, a custom literal always includes its type. Custom literals of different types are allowed to use overlapping sets of identifier-like tokens.

Custom literals can be given more specific interpretations using a foreign function interface, described elsewhere.

Identifier expressions

Id ::=
  [ old ] Identifier

The given identifier must denote a variable in scope. Such a variable may be

an in-, inout-, or out-parameter
a mutable or immutable local variable
a bound variable

The type of the expression is the type of the variable.

In postconditions and procedure bodies, the use of an inout-parameter y as an expression refers to the post-state value (in postconditions) or current value (in bodies) of y. In these contexts, it is also possible to refer to the pre-state value of y, that is, the value of y on entry to the procedure. This is written old y.

Operator expressions

OperatorExpr ::=
  | if Expression Expression else Expression
  | Expression BinaryOp Expression
  | UnaryOp Expression
BinaryOp ::=
  | "<==>"
  | "==>" | "<=="
  | "&&" | "||"
  | "==" | "!=" | "<" | "<=" | ">=" | ">"
  | "+" | "-"
  | "*" | div | mod
UnaryOp ::=
  | "!" | "-"

The ternary operator expression if b e0 else e1 evaluates to e0 if b evaluates to true and evaluates to e1 if b evaluates to false. The type of b must be bool, and the types of expressions e0 and e1 must be the same.

Binary and unary expressions are parsed according to precedence and associativity rules. The unary operators have the highest binding power. The following table lists the binding powers of binary operators, from lowest to highest:

operators	associativity
`<==>`	associative
`==>` `<==`	`==>` associates to the right, `<==` associates to the left, the two different operators do not associate with each other
`&&` `\|\|`	associative, the two different operators do not associate with each other
`==` `!=` `<` `<=` `>=` `>`	not associative
`+` `-`	left associative
`*` `div` `mod`	left associative

Here are descriptions of these operators and their type signatures:

operators	type	description
`<==>`	`bool` \(\times\) `bool` \(\to\) `\bool`	boolean equivalence, aka boolean equality, aka “if and only if”
`==>`	`bool` \(\times\) `bool` \(\to\) `\bool`	logical implication
`<==`	`bool` \(\times\) `bool` \(\to\) `\bool`	reverse implication (that is, `A ==> B` is the same as `B <== A`)
`&&`	`bool` \(\times\) `bool` \(\to\) `\bool`	logical conjunction, aka “and”
`\|\|`	`bool` \(\times\) `bool` \(\to\) `\bool`	logical disjunction, aka “or”
`==`	\(\alpha \times \alpha \to\) `\bool`	equality
`!=`	\(\alpha \times \alpha \to\) `\bool`	disequality, aka “not equal”
`<` `<=` `>=` `>`	`int` \(\times\) `int` \(\to\) `bool`	less, at most, at least, greater
`+`	`int` \(\times\) `int` \(\to\) `int`	addition
`-`	`int` \(\times\) `int` \(\to\) `int`	subtraction
`*`	`int` \(\times\) `int` \(\to\) `int`	multiplication
`div`	`int` \(\times\) `int` \(\to\) `int`	Euclidean division
`mod`	`int` \(\times\) `int` \(\to\) `int`	Euclidean modulo

Notes:

In the table above, \(\alpha\) can be any type, but it has to be the same for both operands.
The comparison operators are not chaining.[1]
Like all functions and expressions in B3, div and mod are total, and in particular they give an integer result even when the divisor (the second argument) is 0. When the divisor is 0, div and mod each gives a result that is a function of its first argument, but B3 intentionally omits any further specification of the value.[2]
Operators div and mod use Euclidean division and modulo. This is also what Dafny, Boogie, and SMT-LIB use, but is different from the truncated division and modulo that, for example, Java and C use. See wikipedia for more information about Euclidean division and modulo.

Function calls

FunctionCall ::=
  Identifier "(" Expression*, ")"

A function call F(e) obtains the value of function F on the argument e.

The identifier must denote a function or tagger in the program. The types of the actual arguments must be the same as for the corresponding formal parameters for the function.

Labeled expressions

LabeledExpr ::=
  Identifier ":" Expression

The expression lbl: e associates the label name lbl with expression e. The label can be used by tools in reporting analysis results.

Syntactically, the Expression parses as far as possible. For example, lbl: a + b means lbl: (a + b). To instead parse it as (lbl: a) + b, use explicit parentheses.

Let expressions

LetExpr ::=
  val Identifier ":=" Expression Expression

The expression val x := rhs e, which can be pronounced “let x be rhs in e, binds the new immutable variable x to the value of rhs and then evaluates e. The expression e is the body of the let expression. The scope of x is that body.

Three notes about the syntax are relevant. The bound variable is introduced without an explicit type; its type is computed from the right-hand side expression. There is no punctuation between the right-hand side expression and the body expression. The body expression parses as far as possible; for example, val x := rhs a + b means val x := rhs (a + b).

Quantifier expressions

QuantifierExpr ::=
  ( forall | exists ) ( Identifier ":" Type )+,
  Pattern*
  Expression
Pattern ::=
  pattern Expression+,

The expression forall x: X pattern p e denotes the universal quantifier \(\forall\, x \colon X \cdot\; e\) and exists x: X pattern p e denotes the existential quantifier \(\exists\, x \colon X \cdot\; e\). Expression e is the body of the quantifier.

The bound variables introduced by the quantifier must be distinct, but they are allowed to shadow other variables already in scope.

A matching pattern for a quantifier is a directive that says how the quantifier is used in proofs. A pattern consists of a list of expressions. The bound variables introduced by the quantifier are in scope in these expressions; in fact, the list of expressions must mention each of the bound variables at least once. The pattern expression is not allowed to include quantifiers.

Two notes about the syntax are relevant. There is no punctuation before the body expression. The body expression parses as far as possible.