Equality test. Uses reference equality for impure composite types, structural equality for pure ones.

Inequality test.

Logical conjunction (eager).

Logical disjunction (eager).

Logical negation.

Logical implication (short-circuit).

Short-circuit logical conjunction. Only evaluates the second argument if the first is true.

Short-circuit logical disjunction. Only evaluates the second argument if the first is false.

Arithmetic negation. Works on Int and Float64.

Addition. Works on Int and Float64.

Subtraction. Works on Int and Float64.

Multiplication. Works on Int and Float64.

Euclidean division. Works on Int and Float64.

Euclidean modulus. Works on Int and Float64.

Truncation division.

Truncation modulus.

Less than. Works on Int and Real.

Less than or equal. Works on Int and Real.

Greater than. Works on Int and Real.

Greater than or equal. Works on Int and Real.

String concatenation.

Conditional with a then-branch and optional else-branch.

A sequence of statements with an optional label for Exit.

A while loop with a condition, invariants, optional termination measure, and body. Only allowed in impure contexts.

postTest selects when the condition is tested relative to the body:

• false (default) — a pre-test loop (while): the condition is checked before the body, so the body may run zero times.

• true — a post-test loop (do … while): the body runs once before the condition is first checked, so it always runs at least once.

Invariants are checked at the loop head (before each body) in both cases. A post-test loop is lowered to the pre-test form by the EliminateDoWhile pass.

Exit a labelled block. Models break and continue statements.

Return from the enclosing procedure with an optional value.

An integer literal.

A boolean literal.

A string literal.

A decimal literal.

A bitvector literal with value and width.

A variable reference or declaration. When var is Variable.Local, this is a reference that evaluates to the variable's value. When var is Variable.Declare, this is a declaration without an initializer (used as a standalone statement in a block).

Assignment to one or more targets. Multiple targets are only supported with identifier targets and a call as the RHS.

Java-style increment/decrement operator. The target must be a Local or Field Variable. As an expression, prefix form yields the new value (after the update) and postfix form yields the old value (before the update). As a statement the yielded value is discarded. Eliminated by the EliminateIncrDecrAndCompoundAssign pass before lifting imperative expressions.

C-style compound assignment (x += e, x -= e, x *= e, x /= e, x %= e), plus x ^= e for string concatenation (Laurel uses ^ for concat, OCaml-style, not bitwise XOR). Lowers to target := target op rhs and yields the new value. The target must be a Local or Field Variable. Invariant: op is one of Add/Sub/Mul/Div/Mod/StrConcat — the only operators the concrete-to-abstract translator ever constructs here. Downstream sites may treat any other Operation as a StrataBug. Eliminated by the EliminateIncrDecrAndCompoundAssign pass before lifting imperative expressions.

Update a field on a pure (value) type, producing a new value.

Call a static procedure by name with the given arguments. Primitive operators are calls too: x + y is a StaticCall to the built-in wrapper $add. See Operation.procName.

Create new object (new). typeArgs carries explicit instantiation arguments for a generic composite, e.g. new Box<int> → ref = Box, typeArgs = [int]. Empty for a non-generic new C (the common case and the pre-existing surface syntax), so the monomorphizer can read the concrete instantiation directly off the allocation site rather than recovering it from surrounding context.

Reference to the current object (this/self).

Reference equality test between two expressions.

Type cast: treat the target as the given type.

Type test: check whether the target is an instance of the given type.

Call an instance method on a target object.

Quantification (universal or existential) over a typed parameter with an optional trigger.

Check whether a variable has been assigned.

Refer to the pre-state value of an expression in a postcondition.

Check whether a reference is freshly allocated. May only target impure composite types.

Assert a condition, generating a proof obligation. The optional summary is a human-readable description of the property being checked.

Assume a condition, restricting the state space.

Throw a value on the exceptional channel. The operand is unconstrained at the throw site; the thrown types are reconciled at each enclosing catch (typed at their least common ancestor) and against the procedure's declared throwsType. See the Exceptions section of the Laurel User Guide.

Structured exception handler: a body, an ordered list of catch clauses (tried first-match-wins), and an optional finally arm that runs on every exit path. See the Exceptions section of the Laurel User Guide.

Attach a proof hint to a value. The semantics are those of value, but proof helps discharge assertions in value.

Extract the contract (reads, modifies, precondition, or postcondition) of a function.

Marker for abstract contracts. Makes the containing type abstract.

Refers to all objects in the heap. Used in reads or modifies clauses.

A hole represents an unknown expression. This can be used to represent programs that are still under development, for example the program 3 + The defining property of a hole is that interaction with it and other code should not produce any errors. Besides representing partial user programs, holes can also be used to handle under development parts of compilers that target Laurel.

• deterministic: if true, the hole represents a deterministic unknown (translated as an uninterpreted function); if false, a nondeterministic unknown (translated as a havoced variable). Nondeterministic holes are not allowed in functions.

• type: this property is used internally by Laurel and can be left to its default value. Internal usage: inferred by the hole type inference pass; none means not yet inferred.