A procedure in Laurel. Procedures are the main unit of specification and verification. Unlike separate functions and methods, Laurel uses a single general concept that covers both.
Constructor
Strata.Laurel.Procedure.mk
Fields
name : Strata.Laurel.Identifier
The procedure's name.
typeArgs : List Strata.Laurel.Identifier
Type parameters, e.g. T in procedure f<T>(...). Empty for monomorphic
procedures (the default keeps every existing construction site compiling).
Brought into scope by resolution so T in a signature resolves to .TVar.
inputs : List Strata.Laurel.Parameter
Input parameters with their types.
outputs : List Strata.Laurel.Parameter
Output parameters with their types. Multiple outputs are supported.
preconditions : List Strata.Laurel.Condition
The preconditions that callers must satisfy.
decreases : Option (Strata.Laurel.AstNode Strata.Laurel.StmtExpr)
Optional termination measure for recursive procedures.
body : Strata.Laurel.Body
The procedure body: transparent, opaque, or abstract.
invokeOn : Option (Strata.Laurel.AstNode Strata.Laurel.StmtExpr)
Optional trigger for auto-invocation. When present, the translator also emits an axiom whose body is the ensures clause universally quantified over the procedure's inputs, with this expression as the SMT trigger.
isInterpretEntry : Bool
When true, the producer marked this procedure as an entry point for
concrete interpretation (laurelInterpret). It has no effect on
verification.
Distinct from Core.EntryPoint (the verifier's .main | .roots | .all
target selector) — this marker drives the concrete interpreter only.
axioms : List (Strata.Laurel.AstNode Strata.Laurel.StmtExpr)
Axioms to emit alongside this procedure. Populated by the contract pass from
invokeOn and ensures clauses.
throwsType : Option (Strata.Laurel.AstNode Strata.Laurel.HighType)
Optional declared exception type: the single type this procedure may
throw, drawn from the front end's own hierarchy (no built-in upper bound).
Catch-or-declare is enforced against it, by validateExceptionEscapes
during resolution (only a subtype of this type may escape; a procedure with
no throwsType may let nothing escape). Not lowered until
EliminateExceptions, which turns it into the Err argument of the
procedure's Result<Val, Err>.
throwsBinding : Option Strata.Laurel.Identifier
The name the throws (e: T) clause binds to the thrown value. Scoped over the
throwsOn blocks' postconditions — not over their guards, which are pre-state
conditions evaluated on entry.
Paired with throwsType: the grammar has a single throws op, which carries
both, so a parsed procedure has either both fields or neither. Code that only
needs to know whether a procedure throws should therefore test throwsType.
throwsOn : List Strata.Laurel.ThrowsOnBlock
Exceptional behavior cases (throwsOn C { ensures … modifies … }), one per
case. See ThrowsOnBlock. Empty means the procedure states nothing about
its throwing paths beyond the declared throwsType.