4.9. Composites and objects🔗

Laurel models objects with composite types. A composite declares 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
};

Two things about new regularly surprise newcomers. It allocates identity but runs no constructor, so the fields of a fresh object are unconstrained until assigned — a freshly allocated int field is an arbitrary integer, not zero. And a variable of composite type holds a reference, so assigning it copies the reference and not the object; that is the subject of Aliasing and separation.

A field may be declared with or without the var marker, which records whether it is mutable. Only mutable fields are implemented: every field is currently compiled as mutable, so leaving var off records the intent but does not prevent writes, and nothing yet relies on it. Genuinely immutable fields are planned — they make verification easier, because a value read once stays valid — along with non-reference composites, which will only be allowed immutable fields. Until then, do not treat a missing var as a guarantee.

4.9.1. Inheritance and runtime type tests🔗

A composite may extend one or more parents, which gives nominal subtyping and inherits their fields. x is T tests an object's runtime type and x as T narrows a reference to a subtype:

composite Shape {}
composite Colored {}
composite Circle extends Shape, Colored {}

procedure classify(s: Shape): bool
{
  return s is Circle
};

x as T behaves like a checked narrowing — it asserts x is T and then has static type T, so a cast that cannot be justified is a verification failure rather than a runtime one.

Fields are inherited through the declared parent graph. If the same field name reaches a child along two different paths, accessing it is rejected as ambiguous unless the child declares its own field with that name.

4.9.2. Overriding and dynamic dispatch🔗

When a composite declares a method that an ancestor also declares, it overrides it, and a call through the ancestor's type runs the override that matches the receiver's runtime type — the same semantics Java and C# have. So a parent may declare a method with a contract and no body and let each child supply the implementation:

composite Shape {
  procedure area(self: Shape): int
    opaque
    ensures area >= 0;
}

composite Square extends Shape {
  var side: int
  procedure area(self: Square): int
    opaque
    ensures area >= 0
  {
    return self#side * self#side
  };
}

procedure describe(s: Shape): int
  opaque
{
  return s#area()
};

describe sees only Shape's contract, and the call dispatches to whichever override the receiver's runtime type selects. A method that nothing overrides is dispatched statically, so inheritance-free code pays nothing for this.

What makes it sound is that an override may not weaken the contract callers were promised. Laurel checks behavioural subtyping at the point of declaration: the override may not demand more of its callers than the parent's precondition did, must deliver at least the parent's postcondition, and may not widen the parent's modifies frame. An override that breaks one of these is reported against the override itself, not at some call site.

Four shapes are rejected rather than dispatched, each with a diagnostic:

the methods in a family disagreeing about whether they throw;
an overrider that renames its type parameters instead of reusing the base's names (SBox<T> extends Box<T> is fine, a renamed one is not);
an incompatible output signature — a different number of outputs, or a return type that is neither the base's nor a subtype of it. A covariant return type is accepted;
an external body anywhere in the family, since a dispatch branch needs a real implementation to call.

Note that changing the non-self parameter types does not produce an override at all: that is an overload, and the two methods stay independent.

Dispatch is on the runtime type tag, so this is not Python's MRO. A front end whose dispatch rules differ from single-inheritance-style tag dispatch — Python's method resolution order, or dispatch on something other than the receiver's type — still has to emit that itself, as explicit control flow over type tests.