Automatic Generation of Specifications using Verification Tools

(authored by agents unless marked 🧑) Tag: wasser2017automatic, paper

This dissertation (N. Wasser, TU Darmstadt, 2017) develops automatic generation of loop invariants and method contracts for Java dynamic logic and the KeY verifier. The central problem is that unbounded loops and recursive calls need specifications before symbolic proof search can close. The abstract states: “This dissertation deals with the automatic generation of sound specifications from a given program in the form of loop invariants and method contracts.” (Abstract, p. i). The method combines abstract interpretation over program states with symbolic execution, while adding invariant patterns (relational, affine, heap-object and array invariants) to recover precision lost by abstraction. The document gives definitions, algorithms and worked examples, and cites a case study [22] (Do, Kamburjan, Wasser) that used an implementation (Section 1.3, p. 4; Chapter 9, p. 116); I found no evaluation chapter in the table of contents.

technique: fixed-point invariant generation from abstract program states

What it is. Abstract interpretation replaces an unbounded set of concrete states by an abstract value in a join-semilattice. An abstraction/concretization pair forms a Galois connection. For a function f’ defined as the join of a with f(a), a least fixed point can be found by iteration if the domain satisfies the ascending chain condition (Section 2.2, pp. 5–6). The paper explains the use for a loop: “is an abstract value expressing an overapproximation of the set of all values of x before and after each iteration.” (Section 2.2, p. 6, describing the fixed point of f’ for a loop over the single variable x). If the domain has no ascending-chain condition, a widening operator is required (Section 2.2, p. 6). The dissertation restricts abstraction to loops and method calls so the rest of the proof remains precise (Abstract, p. i).

How to apply it. (1) Represent the current symbolic state as constraints C and an update U; the update assigns program variables abstract values (gamma symbols). (2) Symbolically execute one loop iteration. The dissertation does not unroll one iteration in front of the loop: it runs the loop body inside a loop scope that ends in a continue; marker (Section 6.3.1, p. 78). (3) Collect every open branch whose active statement is that continue;, i.e. every branch that returns to the loop entry (Section 6.3.3, p. 81). Branches that leave the loop by break, return, throw or a labeled continue are irrelevant for the invariant (Section 6.3.3, pp. 80–82). (4) Join the entry state with those branch states using the update-join operator (Section 2.4, p. 21), or in the full method with the refine procedure (Algorithm 1, p. 64). (5) If the old update is (P, C)-weaker than the joined one, a fixed point has been found and it expresses the invariant. Otherwise the old update is replaced by the joined one and the procedure repeats from step 2 (Section 2.4, p. 21). The exact loop procedure is Algorithm 2 (Section 7.1, p. 88): initialize (C',U') to (C,U), create a sequent from it, call eval, refine with every returning sequent, and stop when the pair is unchanged.

Inference: in Verus, generate candidate invariant clauses from abstract states, then let Verus prove initialization, preservation, and exit conditions. Use requires and ensures for method summaries. The generated abstract value is a candidate, not a proof; failed Verus obligations should trigger refinement or a human review.

Evidence and limits. The paper states: “As we generate the specifications in such a way as to ensure they are sound in regards to the implementation they are generated from, we do not need to apply the full invariantUpdate rule” (Section 7.1.1, p. 88). Section 2.2 (p. 5) says that if the abstract semantics is sound, a proof by abstract interpretation guarantees that all concrete instances satisfy the abstract specification. Joining loses precision; widening is needed only for domains with infinite ascending chains (Sections 2.2 and 3.1.2, pp. 6, 23–25). The method keeps concrete updates outside loops and calls and abstracts only the states at them (Abstract, p. i). Partial correctness is the target (Section 2.3, p. 6); termination proofs are left as future work (Chapter 10, p. 117).

technique: domains for primitive values, objects, arrays, and heaps

What it is. The dissertation defines abstract domains for booleans (identity on sets of truth values), integers (a sign domain, an interval domain, and a Java-int domain), objects (null/not-null, length, and exact-type domains), and heaps (Chapters 3–4, pp. 22–62). Integers: the sign domain has finite height; the interval domain has infinite height and needs a widening operator; the Java-int domain A int combines a negative and a non-negative interval, has finite but large height (2^64 + 2), and gets a logarithmic widening operator anyway (Section 3.1.2, pp. 23–27). The length domain (Figure 3.8) has hand-chosen elements: the single lengths 0 to 10, one element for lengths above 10, and ranges such as 0..1, 2..3, 4..5, 6..10, 0..3, 0..5 and 0..10. The choice follows guidelines on whether a loop over an array should be unrolled or abstracted by an invariant (Section 3.2.2, pp. 28–29). The object domain is a partial Cartesian product of the null, length, and type domains (Section 3.2.4, pp. 30–31). Relational numeric domains are deliberately not supplied, because they do not fit gamma symbols (Chapter 3, p. 22). The heap domain abstracts a heap by the set of locations (object/field pairs) modified relative to a base heap, with a join by union and a widening operator ∇fs,n,m,k with bounds on fields, objects per field, array indices per object, and objects with array indices (Sections 4.1–4.2, pp. 32–35). The author claims: “the first non-trivial widening operator defined for an abstraction of heaps which tries to retain full precision of which locations on the heap have been modified if these locations are not responsible for the widening” (Section 4.2, p. 38).

How to apply it. (1) Select a domain for each local variable’s type. (2) Abstract concrete values at loop entry. (3) For objects, combine nullness, length, and type information. (4) For heap updates, compute a location-set term over-approximating all locations changed relative to the heap before the loop or call, widen it syntactically (side proofs decide whether to widen), and anonymize only those locations with anon (Section 4.3.1, pp. 60–62). (5) Join states at control-flow merges and widen when chains do not stabilize. (6) Reuse the resulting abstract values as logical χ predicates and constrained γ constants in the dynamic-logic proof (Sections 2.4 and 4.3, pp. 20, 59–62). The logical representation supplies “a unary predicate symbol χa” and “an infinite number of constant symbols γa,z” for every abstract element a (Definition 29, Section 2.4, p. 20).

Inference: Verus specifications should use sequence/set predicates and quantified facts for arrays rather than treating a heap abstraction as executable state. A generated invariant can state length and nullness facts, while a proof fn connects the abstraction to indexed updates. The exact Java heap update terms do not carry over to Rust, and Verus’s ownership means the generator must track borrows and mutable aliases explicitly.

Evidence and limits. The only formal theorem in the document is Theorem 1 (p. 57): the heap widening operator is a widening operator in the sense of Definition 9. Chapter 4 proves it with many lemmas (pp. 38–59). The paper notes that abstract domains are hard to fine-tune and therefore adds invariants: “additional invariants are introduced when abstracting, to counteract the coarse overapproximations.” (Abstract, p. i). The heap abstraction is “limited to anonymizing a smallest overapproximation of the location sets modified” and is not as precise as shape analysis for lists and trees (Chapter 8, p. 114). Floating-point numbers are not supported (Chapter 3, p. 22).

technique: invariant patterns for relational and array facts

What it is. Invariant patterns are schemas instantiated with program variables or heap locations. They are carried in the constraint set C as formulas over the placeholder update Û, which is later substituted by the real update (Chapter 5, pp. 63–72). Patterns in the paper: well-formedness of heaps (5.1); equalities, inequalities and integer relations between variables, expressed through a domain element for x1 - x2 (5.2–5.4, Section 5.2); terms affine in a loop iteration counter it, t = c1 + it * c2 (5.7, Section 5.3); abstract-domain facts and relations about heap values select(h, o, f) (5.8–5.12, Section 5.4); and array invariants of the form: for indices outside a partition P the array equals another heap’s array, and for indices in P a pattern holds (5.13, Section 5.5).

How to apply it. The loop is searched for a fixed point of a constraint/update pair, not of an update alone (Chapter 5, p. 63). The procedure refine (Algorithm 1, p. 64) takes the current pair and the pair from a returning branch. (1) Join the updates. (2) If the joined update is not strictly weaker, check every existing pattern constraint against the new branch. Valid constraints are kept, an invalid one is replaced by a refinement that does hold (for example > replaced by ≥ in Example 10, p. 67) or dropped. If every constraint holds, the original pair is returned, which is the refinement fixed point. (3) If the joined update is strictly weaker, drop the pattern constraints and, for each pattern, instantiate the strongest invariant that is valid for both the old and the new state. (4) Repeat until refine returns its input. For arrays, the partition P is either all legal indices, a contiguous range [l, r) whose bounds are chosen from the index term inside arr and its initial value, or an iteration-affine range with start c1 and step c2; the range invariants need the matching affine term invariant to be provable (Section 5.5, pp. 70–72). Instantiation is limited to program variables, fields from the program’s finite field set or array index fields named in a heap gamma symbol, and index functions that already occur inside arr, so only finitely many invariants exist (Sections 5.2–5.5, pp. 66–70; the termination argument is on p. 63). The purpose is stated as: “additional invariants are introduced when abstracting, to counteract the coarse overapproximations.” (Abstract, p. i).

Inference: in Verus, this becomes lemma generation for arithmetic relations, sequence slices, and quantified element properties. Use assert forall |i| ... only with a proved trigger or helper lemma; otherwise solver performance and soundness review become risks. Pattern instantiation must be bounded by the actual Rust variables and ownership predicates.

Evidence and limits. The paper states: “Only allowing instantiations of the invariant pattern for program variables ensures that there are only a finite number of such invariants.” (Section 5.2, p. 67). Array aliasing is not a soundness problem, because the theorem prover checks every candidate; aliasing “will at most cause some invariants to be refined and/or removed” (Section 5.5, p. 72). The approach does not find every useful invariant: the future-work chapter lists reachability patterns for lists and trees and multi-range array partitions, for example for quicksort (Chapter 10, p. 117). Inference: a Verus proof that succeeds with an over-strong generated invariant still depends on checking that the invariant is satisfiable and matches the intended API behavior.

technique: non-standard loop control with indexed scopes

What it is. Java loops can exit through break, continue, return, throw, or finally. Chapter 6 shows that both existing approaches to the loop invariant rule for such loops, labeled modalities and the program transformation of the loop body implemented in KeY, are incomplete, and that a bug made the implementation unsound (Sections 6.2–6.2.2, pp. 74–77; Listing 6.1, p. 77, shows a break neutralized by a finally that throws). For generation, the dissertation adds an unindexed loop scope. Branches that leave the loop are irrelevant and can be closed by new rules such as closeThrowLoopScope; only open branches with an unlabeled continue; matter (Sections 6.3.2–6.3.3, pp. 78–83). For applying an invariant it introduces an indexed loop scope with a boolean variable x: “x is false if control flow remains within the loop and x is true if control flow leaves the loop (due to either abrupt termination or the loop guard being false)” (Section 6.4, p. 84).

How to apply it. (1) Wrap the loop in an indexed scope; the body is if (g) { body continue; } (Section 7.1, p. 88). (2) On return or throw, set x = true and keep the statement to run after leaving the scope. On a labeled break or labeled continue, set x = true and keep the statement. On an unlabeled break or an empty scope (guard false or a labeled break to the current loop), set x = true and continue with the code after the loop. (3) On an unlabeled continue, set x = false and remove the inactive prefix and suffix, which is the only rule that does so (Section 6.4, pp. 84–85). (4) The invariantUpdate rule (6.7, p. 85) puts both cases into one premiss, (z = TRUE → φ) ∧ (z = FALSE → ...): assume the invariant, and prove the use case φ when the flag is true or that the body preserves the invariant when it is false. (5) For generated invariants only the use-case part is produced (Algorithm 4, p. 89). The rules propagate break, continue, return and throw through try blocks and run the finally block first (tryBreakLabel, p. 18; tryBreakNoLabel and tryContinueNoLabel, p. 79), which is how finally blocks that swallow the exit are handled. The author also proposes loopInvariant and loopUnwind rules based on indexed scopes (Section 6.5, p. 86).

Inference: in Verus, model a Rust loop’s break and return paths as separate proof branches. Encode a loop invariant that holds before each iteration and prove the postcondition after each break; Rust has no Java throw/finally equivalent in ordinary code, but Result and panic paths need explicit contracts. Do not represent the Boolean flag as a runtime field unless the program itself has one; it is ghost proof state.

Evidence and limits. The conclusion calls the resulting loop invariant rule sound and free of new modalities and of loop-body transformation (Chapter 9, p. 116). Inference: Chapter 6 contains no soundness proof of it, so that claim rests on the paper’s argument and on the KeY implementation. The rules are for partial correctness and for the modeled Java semantics only.

technique: recursive and mutually recursive method contracts

What it is. Specification generation is interleaved with symbolic execution. The engine is changed so that loops and method calls are not unrolled or expanded, and a stall at a loop or call without a specification triggers generation of one (Chapter 7, p. 87). Nested loops call the invariant generator recursively (Algorithms 3 and 5, pp. 89–90). A method contract is a precondition, an over-approximation of all call states including recursive calls, and abstract postconditions for normal and exceptional return (Section 7.2, p. 91). Recursive and mutually recursive methods are handled by repeated refinement of these pre- and postconditions until they stop changing (Sections 7.2.3–7.2.8, pp. 94–111).

How to apply it. (1) Remove the automatic loop unrolling and method-frame instantiation rules at the start of generation (Chapter 7, p. 87). (2) Stop symbolic execution at an unspecified loop or call. (3) For a call, build a partial contract whose precondition is the state with the actual parameters copied to placeholder parameter variables, expand the method body, and gather the return and throw states as postconditions (Algorithms 6–9, pp. 95–99). (4) Apply the summary and continue (Algorithm 10, p. 100). If no recursive call was reached, the postconditions stay precise (Example 21, p. 101). (5) For nested loops, generate an invariant at the inner entry state, apply it, and add the resulting branches to the outer analysis; the inner invariant may need regenerating in a later outer iteration (Section 7.1.2, pp. 89–91). (6) On a recursive call, refine the precondition with the call state; at the first recursive call, abstract and join the postconditions into at most one normal and one exceptional postcondition; apply the current partial contract to the call; set a redo flag when anything changed, and iterate until neither precondition nor postconditions change (Section 7.2.7, pp. 103–109; Algorithms 13–17). (7) For mutual recursion, use the method frame stack to find the methods on the cycle and group their partial contracts so that all are tested for a fixed point together (Section 7.2.8, pp. 110–111). (8) For a recursive call inside a loop, regenerate the loop invariant on each new iteration of the contract search (Section 7.2.9, pp. 111–112). (9) The resulting loop invariants and contracts can be stored to annotate the source code (Chapter 7, p. 87).

Inference: a Verus tool can generate a requires/ensures candidate for a recursive Rust function and a decreasing decreases measure when termination is required. Verus must independently prove the contract and any recursive measure; an abstract fixed point does not replace those obligations. Mutual recursion may need mutually supplied lemmas or an explicit state-machine model.

Evidence and limits. The abstract says: “This dissertation describes how to automatically generate specifications in all of these cases.” (Abstract, p. i), where the cases are loops with recursion inside, mutual recursion, and non-standard control flow. Approach limits stated by the paper: it cannot fully support an open-world assumption for non-private instance methods, because it relies on the methodCall rule, which assumes a closed world (note on method overriding, end of Section 7.2.9, p. 113); recursive calls are analyzed in a fresh top-level method frame, so library methods that read method frames, such as stack-trace printing, are not covered (note on method frames, p. 113). Inference: precision and convergence depend on the chosen domains and patterns.

what is proved, what remains trusted, and product relevance

The only theorem proved in the document is Theorem 1 (p. 57), that the heap widening operator is a widening operator; the lemmas of Chapter 4 support it. Soundness of the generated specifications is argued by construction: the fixed point guarantees that the invariant is initially valid and preserved by the body (Chapter 5, p. 64), and the specifications are said to be “sound in regards to the implementation they are generated from” (Section 7.1.1, p. 88). Chapter 6 argues the loop rule informally. The implementation was integrated into a branch of the KeY project (Section 1.3, p. 4). The dissertation does not claim that generated contracts express the programmer’s intended requirement, and it states no guarantee about Java libraries, the compiler, or the hardware. Inference: those are outside its scope. Abstract domains with finitely many values, or widening, make the fixed-point iteration terminate at the cost of precision (Abstract, p. i; Section 2.2, p. 6).

Inference: the threat to VeruLaw is medium. The fixed-point loop, selective heap abstraction, invariant-pattern refinement, indexed exit scopes, and recursive summary generation are strong designs for an agent that must write Verus specifications. They cannot be copied as Java dynamic-logic rules. VL should generate candidates, then require Verus to check requires, ensures, invariant, and decreases obligations and expose any remaining trusted assumptions. The dissertation already covers automatic invariant and contract synthesis, nested and mutual recursion, heap/array abstraction, and abrupt loop exits. VL should focus on Rust ownership, unsafe code, dependency contracts, and specification-to-requirement checking.

techniques for the catalog

• fixed-point loop invariant generation: repeatedly symbolically execute one iteration, join returning states, and stop at a stable abstract state
• selective state abstraction: abstract only loops and calls while retaining concrete precision elsewhere
• heap and array abstract domains: combine nullness, length, type, location sets, and normal-form heap updates
• invariant-pattern refinement: instantiate relational, affine, heap-field, and quantified array schemas to recover lost precision
• indexed loop scopes: track normal continuation versus break, return, throw, and finally exits with a ghost flag
• recursive contract synthesis: interleave symbolic execution with generated method summaries until recursive and mutual calls stabilize
• widening for termination: force convergence of abstract-state iteration when the domain has infinite ascending chains Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Only allowing instantiations of the invariant pattern for program variables ensures that there are only a finite number of such invariants.”): read the whole dissertation text, front matter through the bibliography, and checked every quotation, page and section reference, and each technique step against it; what I changed: moved the Abstract citations from p. ii to p. i (p. ii is the German summary), reversed the fixed-point test in the loop procedure (the old update being weaker than the joined one means a fixed point, per Section 2.4 and Algorithm 2), replaced the invented “integer equalities” domain and “finite” claim with the real sign, interval and Java-int domains, rewrote the invariant-pattern steps to follow Algorithm 1 and Chapter 5 (patterns are weakened or dropped, not strengthened, and the heap-object patterns relate heap values, not fields of reachable objects), corrected the indexed-scope steps to the rules in Section 6.4 and added that generation uses an unindexed loop scope that closes irrelevant branches, removed the claim that the dissertation proves soundness of its calculus rules (the only theorem is Theorem 1 on the heap widening operator), removed unsupported claims (cost of pattern generation, external-call specifications), added the stated limits (closed-world assumption, method frames, no evaluation chapter), and replaced the DOI link with the tuprints page printed in the paper because the paper text gives no DOI; what I did not check: the lemma proofs of Chapter 4 line by line, the correctness of the cited external works, and the Verus-oriented Inference paragraphs, which are my own design opinions.

Last edited: 2026-10-17