Dijkstra 方法与验证代码生成#

本页内容3 个部分

1. Challenge#

Current verified code generation pipeline:

                Specification ◄──────── failed
                        │                  ▲
                        ▼                  │
               Informal Reasoning 1         │
                        │                  │
                        ▼                  │
                   Formal Code             │
                        │                  │
                        ▼                  │
               Informal Reasoning 2        │
                        │                  │
                        ▼                  │
                  Formal Proof             │
                        │                  │
                        ▼                  │
                     Verify ───────────────┘
                        │
                      Done

Problems:

Duplicate informal reasoning: Step 1 (spec → code) and Step 3 (spec + code → proof) each require independent informal reasoning about the same spec, but neither reuses the other's insights.
Code-proof inconsistency: Code and proof are generated separately, so they easily drift apart, causing redundant iterations until they align.

2. Our Proposal: Dijkstra Method#

Derive code and proof jointly from the spec via weakest-precondition / refinement calculus, aiming to reduce duplicated reasoning and code–proof mismatch. This is a proposed workflow: failed side conditions can still require revising the program, invariants, or specification:

               Specification
                     │
                     ▼
             Informal Reasoning
                     │
                     ▼
        Formal Code + Formal Proof
              (co-derived)
                     │
                     ▼
                  Verify
                     │
                   Done

For total correctness, loop invariants must be accompanied by termination arguments. All refinement steps and side conditions must be checked against the intended language semantics; verification only establishes the encoded specification. See Dijkstra, EWD418.

3. Planned Evaluation#

Candidate benchmarks (no results are claimed here): Verina + AlgoVeri + Our personal benchmark

3.1 Benchmark Harness: Two Types of Test Cases#

	Positive Cases (valid I/O)	Specified Rejection Cases
Purpose	Verify implementation works on typical happy-path scenarios; prevent regression	Verify error or rejection behavior explicitly required by the contract
Can detect	Wrong computation, missing steps, incorrect ordering	Missing boundary handling, lax validation, incorrect error-branch behavior
Cannot guarantee	Full boundary coverage; spec-level correctness over entire domain	All quantified conditions in the spec are fully constrained

Inputs outside a function’s precondition have no promised behavior unless a checked wrapper or a separate contract specifies it. A test must not require rejection merely because the core precondition is false. Boundary cases inside the precondition still belong in the valid-input suite.

Both types serve as empirical sanity checks — they efficiently filter out obviously broken candidates before sending them to formal verification.