Inverting an Injection, in Why3
Inverting an injective array, in Why3
Auteurs: Jean-Christophe Filliâtre
Catégories: Array Data Structure / Permutation
Outils: Why3
Références: The 1st Verified Software Competition / The VerifyThis Benchmarks
see also the index (by topic, by tool, by reference, by year)
(* VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html Problem 2: inverting an injection Author: Jean-Christophe Filliatre (CNRS) Tool: Why3 (see http://why3.lri.fr/) *) module InvertingAnInjection use int.Int use array.Array use map.MapInjection as M predicate injective (a: array int) (n: int) = M.injective a.elts n predicate surjective (a: array int) (n: int) = M.surjective a.elts n predicate range (a: array int) (n: int) = M.range a.elts n let inverting (a: array int) (b: array int) (n: int) : unit requires { n = length a = length b /\ injective a n /\ range a n } ensures { injective b n } = for i = 0 to n - 1 do invariant { forall j. 0 <= j < i -> b[a[j]] = j } b[a[i]] <- i done (* variant where array b is returned /\ with additional post *) let inverting2 (a: array int) (n: int) : array int requires { n = length a /\ injective a n /\ range a n } ensures { length result = n /\ injective result n /\ forall i. 0 <= i < n -> result[a[i]] = i } = let b = make n 0 in for i = 0 to n - 1 do invariant { forall j. 0 <= j < i -> b[a[j]] = j } b[a[i]] <- i done; b end module Test use array.Array use InvertingAnInjection let test () = let a = make 10 0 in a[0] <- 9; a[1] <- 3; a[2] <- 8; a[3] <- 2; a[4] <- 7; a[5] <- 4; a[6] <- 0; a[7] <- 1; a[8] <- 5; a[9] <- 6; assert { a[0] = 9 && a[1] = 3 && a[2] = 8 && a[3] = 2 && a[4] = 7 && a[5] = 4 && a[6] = 0 && a[7] = 1 && a[8] = 5 && a[9] = 6 }; let b = inverting2 a 10 in assert { b[0] = 6 && b[1] = 7 && b[2] = 3 && b[3] = 1 && b[4] = 5 && b[5] = 8 && b[6] = 9 && b[7] = 4 && b[8] = 2 && b[9] = 0 } end
download ZIP archive
Why3 Proof Results for Project "vstte10_inverting"
Theory "vstte10_inverting.InvertingAnInjection": fully verified
Obligations | Alt-Ergo 2.3.3 | CVC4 1.5 | CVC5 1.0.5 | Coq 8.19.2 | Z3 4.11.2 | ||
VC for inverting | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
loop invariant init | --- | --- | --- | --- | 0.01 | ||
index in array bounds | --- | --- | --- | --- | 0.01 | ||
index in array bounds | --- | --- | --- | --- | 0.01 | ||
loop invariant preservation | --- | --- | 0.00 | --- | --- | ||
postcondition | --- | --- | --- | 0.27 | --- | ||
postcondition | --- | --- | --- | --- | 0.01 | ||
VC for inverting2 | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
array creation size | --- | --- | --- | --- | 0.01 | ||
loop invariant init | --- | --- | --- | --- | 0.01 | ||
index in array bounds | --- | --- | --- | --- | 0.01 | ||
index in array bounds | --- | --- | --- | --- | 0.01 | ||
loop invariant preservation | --- | --- | --- | --- | 0.01 | ||
postcondition | --- | --- | --- | --- | --- | ||
split_goal_right | |||||||
VC for inverting2 | --- | --- | --- | --- | 0.01 | ||
VC for inverting2 | --- | --- | --- | 0.24 | --- | ||
VC for inverting2 | 0.01 | 0.01 | 0.01 | --- | 0.01 | ||
out of loop bounds | --- | --- | --- | --- | 0.01 |
Theory "vstte10_inverting.Test": fully verified
Obligations | Z3 4.11.2 | |
VC for test | --- | |
split_goal_right | ||
array creation size | 0.01 | |
index in array bounds | 0.01 | |
index in array bounds | 0.01 | |
index in array bounds | 0.01 | |
index in array bounds | 0.01 | |
index in array bounds | 0.01 | |
index in array bounds | 0.01 | |
index in array bounds | 0.01 | |
index in array bounds | 0.01 | |
index in array bounds | 0.01 | |
index in array bounds | 0.01 | |
assertion | 0.02 | |
precondition | 4.71 | |
assertion | 0.02 |