EvoSpex: An Evolutionary Algorithm for Learning Postconditions

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

scope

EvoSpex infers Java method postconditions from executions. Its abstract states that it “automatically produces a specification of the method’s current behavior, in the form of postcondition assertions.” (Abstract, p. 1). The target is reference-based classes with structural invariants, and the output is a JML/Alloy-like assertion, not a proof. The method is deliberately behavioral: “This mechanism is based on generating executions of the method under analysis to obtain valid pre/post state pairs, mutating these pairs to obtain (allegedly) invalid ones, and then using a genetic algorithm to produce an assertion that is satisfied by the valid pre/post pairs, while leaving out the invalid ones.” (Abstract, p. 1).

technique: bounded state generation

Use a finite scope to make executions and object graphs enumerable. For a target method m, build initial tuples containing an object of the receiver class and objects for each parameter type, using user-defined primitive ranges and a bound k on execution length (Section IV-A, pp. 5–6). Execute m on every generated tuple and collect valid pre/post pairs V. The paper’s state-matching optimization discards a newly generated trace when its resulting object matches a previously collected canonical object, reducing redundant executions (Section IV-A, p. 6). Invalid set I is generated by selecting a valid pair <s,s′>, randomly changing a field of the post-state or return value within scope, and retaining <s,s″> only when it is not in V (Section IV-A, p. 6). The authors explicitly warn that this is unsound: mutated pairs “may actually correspond to a valid execution of m that we had not generated in V.” (Section I, p. 2).

Verus form (Inference): generate bounded concrete inputs in a harness, then use them as counterexample candidates for a Verus contract. A postcondition should become an ensures clause over old and new values; exhaustive tests can suggest a contract but cannot replace a proof. Verus’s old(...) and ghost snapshots can express pre-state values, while recursive reachability needs a ghost predicate and lemmas. The paper’s canonical object matching and Java reflection do not carry over automatically to Rust ownership and lifetimes.

Evidence and limits: the valid set is only exhaustive within the selected scope and builders; I can contain false “invalid” examples. The benchmark also excludes environment-dependent projects (Section V). The paper does not report a proof that inferred assertions are universally true; it states that “the truth of the remaining assertions” cannot be guaranteed because OASIs’ oracle analysis is incomplete (Section V-A, p. 9).

technique: chromosome representation and assertion language

Represent a candidate as a variable-length chromosome c = <g1,…,gn> whose genes are conjuncts, so its postcondition is φc = g1 ∧ … ∧ gn (Section IV-B, p. 6). Initial chromosomes have one gene; genetic operators grow conjunctions progressively. Genes use equality and inequality, Boolean connectives, navigation through fields, quantifiers over reachable sets, reflexive/transitive closure, set cardinality, return values, and parameters. The paper’s examples include this.root.*(left+right) and quantified acyclicity constraints (Section IV-B, pp. 5–7).

Steps to construct the initial population:

1. Evaluate an expression on randomly selected valid tuples and create expr == v; on invalid tuples create expr != v (Section IV-C, p. 7).
2. Add same-type comparisons, quantified formulas over navigation sets, cardinality comparisons, and comparisons involving result/argument expressions (Section IV-C, p. 7).
3. Keep size-one chromosomes so later mutation and crossover can add conjuncts (Section IV-C, p. 7).

Verus form (Inference): map each gene to a candidate ensures conjunct, using pure/spec functions for navigation and set membership. Quantifiers must be bounded by explicit domains and supported triggers; Alloy transitive closure requires a separately proved recursive reachability predicate. A candidate contract is still only a hypothesis until Verus proves it for all executions.

technique: asymmetric fitness and genetic search

For candidate c, compute positive counterexamples P = {v∈V | ¬φc(v)} and negative counterexamples N = {i∈I | φc(i)} (Section IV-D, p. 7). Fitness prioritizes zero positive counterexamples, then penalizes length and syntactic complexity, and rewards method-component assertions relating parameters, return values, or pre/post state. The paper gives a case-based formula and explains: “This case-based definition aims at considering the negative counterexamples only when no positive counterexamples are obtained.” (Section IV-D, p. 8).

Mutation selects each gene with probability 0.3 and can delete, negate, add/subtract numeric expressions, replace or extend navigations, or replace operators (Section IV-E, p. 8). Crossover has rate 0.35 and unions genes from two chromosomes, producing conjunction φc1 ∧ φc2; only candidates consistent with all valid executions are retained for combination (Section IV-E, p. 8). Run selection and these operators for up to 30 generations or a 10-minute timeout per method, repeating runs and selecting the most frequent result (Section V, pp. 8–9).

Verus form (Inference): use the search only outside the verifier to propose contracts, then compile survivors into Rust ensures clauses and run cargo verus. Counterexamples from failed proofs replace EvoSpex’s test-pair fitness signal. Mutation of a contract is useful for exploration, but weakening a contract to make it prove is unsound for the intended requirement.

evidence, measured results, and threat

The RQ1 benchmark randomly selected 16 open-source Java projects from SF110; 200 methods were analyzed. Table II reports 522 EvoSpex assertions with 35 false positives (6.70%) versus 2,219 Daikon assertions with 388 false positives (17.49%), denominators being all produced assertions over those 200 methods (Section V-A, Table II, pp. 9–10). The authors report lower false-positive percentages in 13 of 16 projects. RQ2 compares against manually written Eiffel contracts (11 methods) and synthesized Cozy classes (12 methods): EvoSpex recovered at least one exact property in 8/11 Eiffel cases and 9/12 Cozy cases (Section V-A, pp. 10–11). False negatives remain: both tools produce weaker-than-strongest postconditions and miss some mutations (Section V-A, p. 10).

Trusted and unproved: the Java execution engine, builders, scope bounds, mutation assumption, translation of Eiffel/Cozy subjects, manual filtering, and OASIs oracle all remain outside a formal proof. The authors say their Eiffel translation was “not formally verified” (Section V, p. 9). Inference: threat to a product generating agent-written verified Rust is medium. EvoSpex provides a useful contract-discovery loop and explicit measures, but its finite tests and unsound invalid-pair generation cannot establish Verus proof obligations or specification adequacy. VL should not redo this exact evolutionary postcondition search; it should reuse bounded counterexample generation to suggest contracts, then insist on Verus proofs and track which inferred clauses fail or require manual lemmas.

techniques for the catalog

• bounded valid/invalid pair generation: execute within a finite object and trace scope, then mutate post-states as negative guidance while recording the mutation unsoundness
• chromosome contract synthesis: represent a postcondition as a conjunction of navigational, quantified, and relational genes
• asymmetric evolutionary fitness: prioritize candidates consistent with every valid execution before penalizing complexity and using mutated negatives
• state matching: canonicalize generated objects and discard traces that duplicate an existing state Checked 2026-10-15 against paper molina2021evospex: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: 2026-10-15