# Statements

Statements and expressions in B3 are self-terminating, so there are no semi-colons.

```
Stmt ::=
  | VarDecl
  | Assign
  | Reinit
  | BlockStmt
  | Call
  // assertions
  | Check
  | Assume
  | Reach
  | Assert
  | AForall
  // control flow
  | Choose
  | If
  | IfCase
  | Loop
  | LabeledStmt
  | Exit
  | Return
  // error reporting
  | Probe
```

## Variable declarations

```
VarDecl ::=
  ( var | val ) Identifier [ ":" Type ] [ "autoinv" Expression ] [ ":=" Expression ]
```

A declaration using `var` introduces a mutable local variable, whereas `val`
introduces an immutable local variable. A mutable variable that is never updated
is semantically equivalent to an immutable variable. However, the body of a `forall`
statements is not allowed to declare mutable variables.

The variable declaration is allowed to omit one of `: Type` or `:= Expression`,
but not both. If the type is omitted, it is determined from the given expression.
If the expression is omitted, the variable is initialized with an arbitrary value
of its type.

The variable remains in scope until the end of the enclosing block.

A variable is allowed to shadow previously declared variables with the same name.

## Assignment statements

```
Assign ::=
  Identifier ":=" Expression
```

The identifier must be a mutable variable.

## Re-init statements

```
Reinit ::=
  reinit Identifier*,
```

This statement sets each of the named variables to an arbitrary value, subject to the auto-invariants of the variables.

## Block statements

```
BlockStmt ::=
  "{" Stmt* "}"
```

## Call statement

```
Call ::=
  Identifier "(" CallArgument ")"
CallArgument ::=
  | Expression
  | ( "inout" | "out" ) Identifier
```

A call statement invokes a procedure. The argument mode (in, inout, or out) of each parameter
is explicitly repeated at the call site (where the absence of `inout` and `out` indicates an
in-argument).

The types of the actual arguments must be the same as for the corresponding formal parameters.

The variables given as inout- and out-arguments must be distinct mutable variables.

## Check statements

```
Check ::=
  check Expression
```

The statement `check e` describes the intention that every program trace that leads to
this statement finds `e` to evaluate `true`.

It is an error if control flow can reach a `check` statement whose expression can evaluate to `false`.

## Assume statements

```
Assume ::=
  assume Expression
```

The statement `assume e` declares that a program trace that leads to this statement is of interest
only if, in that trace, `e` to evaluate `true`. In other words, the assume statement says that
"what follows this statement is of interest only if `e` evaluates to `true`".

## Reach statements

```
Reach ::=
  reach Expression
```

The statement `reach e` describes the intention that there exists a program trace that leads to
this statement and finds `e` to evaluate `true`.

## Assert statements

```
Assert ::=
  assert Expression
```

A statement `assert E` is equivalent to the statement sequence `check E assume E`.

## Forall statements

```
AForall ::=
  forall Identifier ":" Type
  BlockStmt
```

TODO: description

## Choose statements

```
Choose ::=
  choose BlockStmt ( or BlockStmt )*
```

TODO: description

## If statements

```
If ::=
  if Expression BlockStmt [ else IfContinuation ]
IfContinuation ::=
  | BlockStmt
  | If
  | IfCase
```

TODO: description

## If-case statements

```
IfCase ::=
  if Case+
Case ::=
  case Expression BlockStmt
```

TODO: description

## Loops

```
Loop ::=
  loop Invariant* BlockStmt
Invariant ::=
  invariant AExpression
```

TODO: description

## Labeled statements

```
LabeledStmt ::=
  Identifier ":" ( BlockStmt | Loop )
```

TODO: description

## Exit statements

```
Exit ::=
  exit [ Identifier ]
```

An exit statement terminates a statement abruptly, transferring control out
of the enclosing statement labeled with the given label. If the label is omitted,
the statement transfers control out of the enclosing loop (which need not be labeled).

## Return statements

```
Return ::=
  return
```

A return statement terminates a procedure body abruptly, transferring control out
of the enclosing procedure body. It is as if the procedure body were labeled and
the return statement performs an `exit` to that label.

## Probe statements

```
Probe ::=
  probe Expression
```

TODO: description