Experimental Imperative Reference

This page documents Deduce's imperative-verification surface. The design is described in docs/imperative-verification-plan.md and tracked by issue #854.

Status: Phase 1 (parser/AST only). The grammar entries below are recognized by both parsers and the pretty-printer round-trips them. The imperative verifier itself does not exist yet — the checker rejects every proc, observer, and resource declaration until later phases land.

Most of the surface lives behind the --experimental-imperative flag. The exceptions are noted per-section.

Contents

• Frame Expression
• Mutable Array Type
• Object (Statement)
• Observer (Statement)
• Procedure (Statement)
• Resource (Statement)
• Resource Formulas

Frame Expression

A frame expression denotes a set of heap locations referenced by the reads and modifies clauses of a Procedure or the reads clause of an Observer. The empty set is written {}, footprint(e) names the ghost footprint owned by e, e.f names one mutable object field, and a bare term e names every cell of a mutable structure. A frame list is a comma-separated union.

Mutable Array Type

The mutable-array type [T]! is defined in the main Type grammar. It is parser-only today and requires --experimental-imperative.

Object (Statement)

An object declaration introduces a heap-allocated type with a fixed set of fields. Each field is introduced by var, optionally preceded by ghost to mark a specification-only field. The body braces may be omitted to declare a bodyless object.

Field-level visibility is determined by the enclosing object: an opaque object hides its fields outside the defining module; otherwise fields follow the object's visibility.

Object declarations parse without --experimental-imperative, but mutation, allocation, and field reads/writes still have no runtime or proof semantics — those land with the verifier in later phases.

Observer (Statement)

An observer is a pure specification function over mutable state. It may read the heap through its Frame Expression reads clauses but cannot mutate it. Repeated reads clauses union their frames. The optional body, when present, is an ordinary Deduce term computing the observer's result.

Observer declarations require --experimental-imperative. The checker rejects them until the imperative verifier exists.

Procedure (Statement)

A proc declares an imperative procedure. Parameters may be marked ghost to indicate they exist only for specification. The optional -> type annotates the procedure's return type. Specification clauses may be repeated and are interpreted as conjunction for requires and ensures, and union for reads and modifies. An ensures clause may carry a label so that callers can cite the postcondition by name.

Procedure declarations require --experimental-imperative. The checker rejects every procedure until the imperative verifier exists, so a procedure body is parsed but not yet type-checked or verified. Frame clauses use the Frame Expression grammar.

Procedure Body (Statement Block)

A procedure body is a brace-delimited sequence of imperative statements. Local variables are introduced with var (or ghost var for specification-only values) and an optional type annotation. An assignment target is a local variable, a mutable array cell a[i], or a field p.f. An imperative if uses braces rather than the then/else of the pure if term, so pure conditional terms are unaffected inside a procedure body. A while loop carries repeated invariant, modifies, established by, preserved by, and decreases annotations before its body. The assert, assume, call, and return statements take an ordinary term or formula.

Proof clauses, proof slots, and call labels

Verification points may carry an explicit proof after by: assert P by p, call f(args) by p, and a loop's established by p, preserved by q, and decreases d by r. A proof clause (imp_proof) is either an ordinary Deduce proof expression — which also covers a bare proof-slot label such as loop_init — or a qualified call-postcondition reference such as h.valid_post.

A call may bind a call label with as h, exposing the callee's labelled postconditions as h.<label> facts for later proof clauses. A call used as a var/assignment right-hand side (var x := call f(args) as h) may bind a label the same way.

Long proofs move out of line into a procedure's optional proof ... end block, one label { proof } entry per proof slot named by a by label clause:

This is parser/AST only: proof-slot goal generation, ambiguity checking between theorem names and slot labels, and tying h.valid_post to a call label all land with the verifier in a later phase.

Resource (Statement)

A resource declares a named separation-logic predicate over mutable state. Its parameters reuse the Procedure parameter grammar. The optional body, when present, is a resource formula describing the heap ownership the resource stands for; a bodyless resource is an abstract predicate whose definition is supplied elsewhere.

Resource declarations require --experimental-imperative. The checker rejects them until the imperative verifier exists.

Resource Formulas

Resource formulas extend the ordinary term grammar with three separation-logic connectives, gated behind --experimental-imperative:

• emp is the empty resource — a heap owning no locations.

• p ** q is the separating conjunction: the heap splits into two disjoint parts, one satisfying p and the other q. It is left-associative, looser than |-> but tighter than and/or.

• a |-> b is the points-to assertion: a heap owning exactly the single cell at address a, holding value b. It is non-associative, so a |-> b |-> c must be parenthesized. A field-access address such as p.f is an ordinary atomic term, so it needs no extra syntax on the left of |->.

These connectives parse into ordinary Term nodes; they have no proof rules or runtime meaning yet.