diff options
Diffstat (limited to 'formal/README.md')
| -rw-r--r-- | formal/README.md | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/formal/README.md b/formal/README.md index f667bdf..1bbb7e0 100644 --- a/formal/README.md +++ b/formal/README.md @@ -1,22 +1,24 @@ -# Gobra deductive proof +# Gobra deductive proofs -`insertion.go` is a **machine-checked** proof that an insertion sort is correct, -verified by [Gobra](https://github.com/viperproject/gobra) — ETH Zurich's -deductive verifier for Go, which translates annotated Go to the Viper -intermediate language and discharges the proof obligations with the Z3 SMT +`insertion.go` and `selection.go` are **machine-checked** proofs that these +sorts are correct, verified by [Gobra](https://github.com/viperproject/gobra) — +ETH Zurich's deductive verifier for Go, which translates annotated Go to the +Viper intermediate language and discharges the proof obligations with the Z3 SMT solver. -Unlike the TLA+ model (which checks a hand-written abstraction) and the property -tests (which sample inputs), this verifies the **actual Go source** for **all** -inputs. Gobra proves two things about `Insertion`: +Unlike the TLA+ models (which check a hand-written abstraction) and the property +tests (which sample inputs), these verify the **actual Go source** for **all** +inputs. Gobra proves two things about each sort: 1. **Memory safety** — every index access is in bounds. The permission invariants `forall k :: 0 <= k < len(a) ==> acc(&a[k])` carry write access to every element through both loops; Go itself cannot prove the absence of index-out-of-range panics, Gobra can. 2. **Ordering** — on return `a` is sorted ascending - (`forall p < q :: a[p] <= a[q]`), established via the two insertion-sort loop - invariants in the annotations. + (`forall p < q :: a[p] <= a[q]`), established via the loop invariants in the + annotations. Selection sort needs the stronger "every prefix element ≤ every + suffix element" invariant; insertion sort uses a "sorted except at the + in-flight index" invariant. The **permutation** half of full correctness (output is a rearrangement of the input) is intentionally left to the property tests and the paper proof in @@ -45,7 +47,8 @@ or directly: ```sh podman run --rm -v "$PWD/formal:/gobra/formal:z" \ - ghcr.io/viperproject/gobra:latest -i /gobra/formal/insertion.go + ghcr.io/viperproject/gobra:latest \ + -i /gobra/formal/insertion.go /gobra/formal/selection.go ``` Expected output ends with: |