3.5.1. File-scope globals🔗

A program-level var counter: int defines shared mutable state. Laurel lowers direct and transitive global effects to hidden parameters in declaration order; initial values come from the caller or runtime.

Supported: reads and writes in procedure bodies (including instance and transitive calls), current global values in contracts, and multiple globals alongside heap state.

Not yet supported (reported with source diagnostics):

• Global-dependent old(...) expressions.

• Globals in entry procedures, constants, or constrained-type predicates and witnesses.

• Explicit inout/global interactions and global-writing invokeOn procedures.

• Writes in restricted expressions, ambiguous bodiless postconditions, and unsupported multi-output call shapes.

Names containing $ are reserved for compiler-generated variables.

3.5.2. Primitive types🔗

Laurel provides unbounded mathematical int and real types, a bool type, string, and fixed-width bitvectors. Because int is unbounded, arithmetic in specifications behaves like ordinary mathematics: there is no overflow to reason around when you are stating what a procedure computes.

3.5.3. Composites🔗

Laurel models objects with composite types. A composite declares mutable fields and may declare instance procedures (methods). Fields are read and written with the # selector, instances are created with new, and a method is invoked with the same # syntax.

composite Counter {
  var count: int
  procedure reset(self: Counter)
    opaque
    ensures self#count == 0
    modifies self
  {
    self#count := 0
  };
}

procedure useCounter()
  opaque
{
  var c: Counter := new Counter;
  c#reset();
  assert c#count == 0
};

An instance procedure takes its receiver as an explicit self parameter and refers to fields through it. The contract of a method uses the same requires / ensures / modifies clauses as any other procedure; here ensures self#count == 0 is what lets the caller conclude c#count == 0 after c#reset().

Field selection and method calls chain, so you can reach through one object to another: o#inner#x reads field x of the object stored in o's inner field, and o#inner#isOne() calls a method on it.

composite Inner { var x: int }
composite Outer { var inner: Inner }

procedure useOuter()
  opaque
{
  var o: Outer := new Outer;
  var v: int := o#inner#x
};