In-Place Linked-List Reversal in Why3
This is a Why3 version of the classical example of in-place linked-list reversal
Auteurs: Claude Marché
Catégories: Inductive predicates / List Data Structure / Separation challenges / Ghost code / Pointer Programs
Outils: Why3
see also the index (by topic, by tool, by reference, by year)
In-place linked list reversal
Version designed for the MPRI lecture ``Proof of Programs''
This is an improved version of this one: it does not use any Coq proofs, but lemma functions instead.
module InPlaceRev use map.Map use ref.Ref use int.Int use list.List use list.Quant as Q use list.Append use list.Mem use list.Length use export list.Reverse type loc val function eq_loc (l1 l2:loc) : bool ensures { result <-> l1 = l2 } val constant null : loc predicate disjoint (l1:list loc) (l2:list loc) = forall x:loc. not (mem x l1 /\ mem x l2) predicate no_repet (l:list loc) = match l with | Nil -> true | Cons x r -> not (mem x r) /\ no_repet r end let rec ghost mem_decomp (x: loc) (l: list loc) : (l1: list loc, l2: list loc) requires { mem x l } variant { l } ensures { l = l1 ++ Cons x l2 } = match l with | Nil -> absurd | Cons h t -> if eq_loc h x then (Nil,t) else let (r1,r2) = mem_decomp x t in (Cons h r1,r2) end val acc (field: ref (map loc 'a)) (l:loc) : 'a requires { l <> null } reads { field } ensures { result = get !field l } val upd (field: ref (map loc 'a)) (l:loc) (v:'a):unit requires { l <> null } writes { field } ensures { !field = set (old !field) l v } inductive list_seg loc (map loc loc) (list loc) loc = | list_seg_nil: forall p:loc, next:map loc loc. list_seg p next Nil p | list_seg_cons: forall p q:loc, next:map loc loc, l:list loc. p <> null /\ list_seg (get next p) next l q -> list_seg p next (Cons p l) q let rec lemma list_seg_frame_ext (next1 next2:map loc loc) (p q r v: loc) (pM:list loc) requires { list_seg p next1 pM r } requires { next2 = set next1 q v } requires { not (mem q pM) } variant { pM } ensures { list_seg p next2 pM r } = match pM with | Nil -> () | Cons h t -> assert { p = h }; list_seg_frame_ext next1 next2 (get next1 p) q r v t end let rec lemma list_seg_functional (next:map loc loc) (l1 l2:list loc) (p: loc) requires { list_seg p next l1 null } requires { list_seg p next l2 null } variant { l1 } ensures { l1 = l2 } = match l1,l2 with | Nil, Nil -> () | Cons _ r1, Cons _ r2 -> list_seg_functional next r1 r2 (get next p) | _ -> absurd end let rec lemma list_seg_sublistl (next:map loc loc) (l1 l2:list loc) (p q: loc) requires { list_seg p next (l1 ++ Cons q l2) null } variant { l1 } ensures { list_seg q next (Cons q l2) null } = match l1 with | Nil -> () | Cons _ r -> list_seg_sublistl next r l2 (get next p) q end let rec lemma list_seg_no_repet (next:map loc loc) (p: loc) (pM:list loc) requires { list_seg p next pM null } variant { pM } ensures { no_repet pM } = match pM with | Nil -> () | Cons h t -> if mem h t then (* absurd case *) let (l1,l2) = mem_decomp h t in list_seg_sublistl next (Cons h l1) l2 p h; list_seg_functional next pM (Cons h l2) p; assert { length pM > length (Cons h l2) } else list_seg_no_repet next (get next p) t end let rec lemma list_seg_append (next:map loc loc) (p q r: loc) (pM qM:list loc) requires { list_seg p next pM q } requires { list_seg q next qM r } variant { pM } ensures { list_seg p next (pM ++ qM) r } = match pM with | Nil -> () | Cons _ t -> list_seg_append next (get next p) q r t qM end val next : ref (map loc loc) let app (l1 l2:loc) (ghost l1M l2M:list loc) : loc requires { list_seg l1 !next l1M null } requires { list_seg l2 !next l2M null } requires { disjoint l1M l2M } ensures { list_seg result !next (l1M ++ l2M) null } = if eq_loc l1 null then l2 else let p = ref l1 in let ghost pM = ref l1M in let ghost l1pM = ref (Nil : list loc) in while not (eq_loc (acc next !p) null) do invariant { !p <> null } invariant { list_seg l1 !next !l1pM !p } invariant { list_seg !p !next !pM null } invariant { !l1pM ++ !pM = l1M } invariant { disjoint !l1pM !pM } variant { !pM } match !pM with | Nil -> absurd | Cons h t -> pM := t; assert { disjoint !l1pM !pM }; assert { not (mem h !pM) }; l1pM := !l1pM ++ Cons h Nil; end; p := acc next !p done; upd next !p l2; assert { list_seg l1 !next !l1pM !p }; assert { list_seg !p !next (Cons !p Nil) l2 }; assert { list_seg l2 !next l2M null }; l1 let in_place_reverse (l:loc) (ghost lM:list loc) : loc requires { list_seg l !next lM null } ensures { list_seg result !next (reverse lM) null } = let p = ref l in let ghost pM = ref lM in let r = ref null in let ghost rM = ref (Nil : list loc) in while not (eq_loc !p null) do invariant { list_seg !p !next !pM null } invariant { list_seg !r !next !rM null } invariant { disjoint !pM !rM } invariant { (reverse !pM) ++ !rM = reverse lM } variant { !pM } let n = get !next !p in upd next !p !r; assert { list_seg !r !next !rM null }; r := !p; p := n; match !pM with | Nil -> absurd | Cons h t -> rM := Cons h !rM; pM := t end done; !r end
Using sequences instead of lists
module InPlaceRevSeq use int.Int use map.Map as Map use seq.Seq use seq.Mem use seq.Reverse type loc val function null: loc val function eq_loc (l1 l2:loc) : bool ensures { result <-> l1 = l2 } predicate disjoint (s1: seq 'a) (s2: seq 'a) = (* forall x:'a. not (mem x s1 /\ mem x s2) *) forall i1. 0 <= i1 < length s1 -> forall i2. 0 <= i2 < length s2 -> s1[i1] <> s2[i2] predicate no_repet (s: seq loc) = forall i. 0 <= i < length s -> not (mem s[i] s[i+1..]) lemma non_empty_seq: forall s: seq 'a. length s > 0 -> s == cons s[0] s[1..] let rec ghost mem_decomp (x: loc) (s: seq loc) : (s1: seq loc, s2: seq loc) requires { mem x s } variant { length s } ensures { s == s1 ++ cons x s2 } = if eq_loc s[0] x then (empty, s[1..]) else begin assert { s == cons s[0] s[1..] }; let (s1, s2) = mem_decomp x s[1..] in (cons s[0] s1, s2) end use ref.Ref type memory 'a = ref (Map.map loc 'a) val acc (field: memory 'a) (l:loc) : 'a requires { l <> null } reads { field } ensures { result = Map.get !field l } val upd (field: memory 'a) (l: loc) (v: 'a) : unit requires { l <> null } writes { field } ensures { !field = Map.set (old !field) l v } type next = Map.map loc loc predicate list_seg (next: next) (p: loc) (s: seq loc) (q: loc) = let n = length s in (forall i. 0 <= i < n -> s[i] <> null) /\ ( (p = q /\ n = 0) \/ (1 <= n /\ s[0] = p /\ Map.get next s[n-1] = q /\ forall i. 0 <= i < n-1 -> Map.get next s[i] = s[i+1])) lemma list_seg_frame_ext: forall next1 next2: next, p q r v: loc, pM: seq loc. list_seg next1 p pM r -> next2 = Map.set next1 q v -> not (mem q pM) -> list_seg next2 p pM r let rec lemma list_seg_functional (next: next) (l1 l2: seq loc) (p: loc) requires { list_seg next p l1 null } requires { list_seg next p l2 null } variant { length l1 } ensures { l1 == l2 } = if length l1 > 0 && length l2 > 0 then begin assert { l1[0] = l2[0] = p }; list_seg_functional next l1[1..] l2[1..] (Map.get next p) end let rec lemma list_seg_tail (next: next) (l1: seq loc) (p q: loc) requires { list_seg next p l1 q } requires { length l1 > 0 } variant { length l1 } ensures { list_seg next (Map.get next p) l1[1..] q } = if length l1 > 1 then list_seg_tail next l1[1..] (Map.get next p) q let rec lemma list_seg_append (next: next) (p q r: loc) (pM qM: seq loc) requires { list_seg next p pM q } requires { list_seg next q qM r } variant { length pM } ensures { list_seg next p (pM ++ qM) r } = if length pM > 0 then list_seg_append next (Map.get next p) q r pM[1..] qM lemma seq_tail_append: forall l1 l2: seq 'a. length l1 > 0 -> (l1 ++ l2)[1..] == l1[1..] ++ l2 let rec lemma list_seg_prefix (next: next) (l1 l2: seq loc) (p q: loc) requires { list_seg next p (l1 ++ cons q l2) null } variant { length l1 } ensures { list_seg next p l1 q } = if length l1 > 0 then begin list_seg_tail next (l1 ++ cons q l2) p null; list_seg_prefix next l1[1..] l2 (Map.get next p) q end let rec lemma list_seg_sublistl (next: next) (l1 l2: seq loc) (p q: loc) requires { list_seg next p (l1 ++ cons q l2) null } variant { length l1 } ensures { list_seg next q (cons q l2) null } = assert { list_seg next p l1 q }; if length l1 > 0 then begin list_seg_tail next l1 p q; list_seg_sublistl next l1[1..] l2 (Map.get next p) q end lemma get_tail: forall i: int, s: seq 'a. 0 <= i < length s - 1 -> s[1..][i] = s[i+1] lemma tail_suffix: forall i: int, s: seq 'a. 0 <= i < length s -> s[1..][i..] == s[i+1..] let rec lemma list_seg_no_repet (next: next) (p: loc) (pM: seq loc) requires { list_seg next p pM null } variant { length pM } ensures { no_repet pM } = if length pM > 0 then begin let h = pM[0] in let t = pM[1..] in if mem h t then (* absurd case *) let (l1,l2) = mem_decomp h t in list_seg_sublistl next (cons h l1) l2 p h; list_seg_functional next pM (cons h l2) p; assert { length pM > length (cons h l2) } else begin assert { not (mem pM[0] pM[0+1..]) }; list_seg_no_repet next (Map.get next p) t; assert { forall i. 1 <= i < length pM -> not (mem pM[i] pM[i+1..]) } end end val next : ref next let app (l1 l2: loc) (ghost l1M l2M: seq loc) : loc requires { list_seg !next l1 l1M null } requires { list_seg !next l2 l2M null } requires { disjoint l1M l2M } ensures { list_seg !next result (l1M ++ l2M) null } = if eq_loc l1 null then l2 else let p = ref l1 in let ghost pM = ref l1M in let ghost l1pM = ref (empty : seq loc) in ghost list_seg_no_repet !next l1 l1M; while not (eq_loc (acc next !p) null) do invariant { !p <> null } invariant { list_seg !next l1 !l1pM !p } invariant { list_seg !next !p !pM null } invariant { !l1pM ++ !pM == l1M } invariant { disjoint !l1pM !pM } variant { length !pM } assert { length !pM > 0 }; assert { not (mem !p !l1pM) }; let ghost t = !pM[1..] in ghost l1pM := !l1pM ++ cons !p empty; ghost pM := t; p := acc next !p done; upd next !p l2; assert { list_seg !next l1 !l1pM !p }; assert { list_seg !next !p (cons !p empty) l2 }; assert { list_seg !next l2 l2M null }; l1 let in_place_reverse (l:loc) (ghost lM: seq loc) : loc requires { list_seg !next l lM null } ensures { list_seg !next result (reverse lM) null } = let p = ref l in let ghost pM = ref lM in let r = ref null in let ghost rM = ref (empty: seq loc) in while not (eq_loc !p null) do invariant { list_seg !next !p !pM null } invariant { list_seg !next !r !rM null } invariant { disjoint !pM !rM } invariant { (reverse !pM) ++ !rM == reverse lM } variant { length !pM } let n = acc next !p in upd next !p !r; assert { list_seg !next !r !rM null }; r := !p; p := n; rM := cons !pM[0] !rM; pM := !pM[1..] done; !r end
This time with a fully automated proof.
The key to a fully automated proof is to introduce an array of
cells, called cell
below, and then to resort to arithmetic and
universal quantifiers to define lists (predicates listLR
and
listRL
below).
This proof requires no lemma function and no transformation. A single call to Z3 completes the proof in no time (0.04 s).
module YetAnotherInPlaceRev use int.Int use map.Map type loc val (=) (l1 l2: loc) : bool ensures { result <-> l1 = l2 } val constant null : loc type mem = { mutable next: loc -> loc } val mem: mem let cdr (p: loc) : loc requires { p <> null } ensures { result = mem.next p } = mem.next p let set_cdr (p: loc) (v: loc) : unit requires { p <> null } ensures { mem.next = (old mem.next)[p <- v] } = let m = mem.next in mem.next <- fun x -> if x = p then v else m x predicate valid_cells (s: int -> loc) (n: int) = (forall i. 0 <= i < n -> s i <> null) && (forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> s i <> s j) predicate listLR (m: mem) (s: int -> loc) (l: loc) (lo hi: int) = 0 <= lo <= hi && if lo = hi then l = null else l = s lo && m.next (s (hi-1)) = null && forall k. lo <= k < hi-1 -> m.next (s k) = s (k+1) predicate listRL (m: mem) (s: int -> loc) (l: loc) (lo hi: int) = 0 <= lo <= hi && if lo = hi then l = null else m.next (s lo) = null && l = s (hi-1) && forall k. lo < k < hi -> m.next (s k) = s (k-1) predicate frame (m1 m2: mem) (s: int -> loc) (n: int) = forall p. (forall i. 0 <= i < n -> p <> s i) -> m1.next p = m2.next p let list_reversal (ghost s: int -> loc) (ghost n: int) (l: loc) : (r: loc) requires { valid_cells s n } requires { listLR mem s l 0 n } ensures { listRL mem s r 0 n } ensures { frame mem (old mem) s n } = let ref l = l in let ref p = null in let ghost ref i = 0 in while l <> null do invariant { if n = 0 then l = p = null else i = 0 && p = null && l = s 0 || i = n && p = s (n-1) && l = null || 0 < i < n && p = s (i-1) && l = s i } invariant { listRL mem s p 0 i } invariant { listLR mem s l i n } invariant { frame mem (old mem) s n } variant { n - i } let tmp = l in l <- cdr l; set_cdr tmp p; p <- tmp; i <- i + 1 done; return p let rec ghost predicate is_list (m: mem) (l: loc) (s: int -> loc) (n: int) requires { n >= 0 } variant { n } = if n = 0 then l = null else l = s 0 <> null && is_list m (m.next l) (fun i -> s (i+1)) (n - 1) let rec lemma cells_of_list (l: loc) (s: int -> loc) (n: int) requires { n >= 0 } requires { is_list mem l s n } variant { n } ensures { valid_cells s n } ensures { listLR mem s l 0 n } = if n <> 0 then cells_of_list (cdr l) (fun i -> s (i+1)) (n - 1) let rec lemma list_of_cells (r: loc) (s: int -> loc) (n: int) requires { n >= 0 } requires { valid_cells s n } requires { listRL mem s r 0 n } variant { n } ensures { is_list mem r (fun i -> s (n-1-i)) n } = if n <> 0 then list_of_cells (cdr r) s (n - 1) let list_reversal_final (ghost s) (ghost n: int) (l: loc) : (r: loc) requires { n >= 0 } requires { is_list mem l s n } ensures { is_list mem r (fun i -> s (n-1-i)) n } ensures { frame mem (old mem) s n } = cells_of_list l s n; let r = list_reversal s n l in list_of_cells r s n; r end module Termination
On a null-terminated list, list_reversal
terminates. We have shown it
already e.g. in the previous module.
But list_reversal
actually terminates on *any* list, even when it
contains a loop. Indeed, the code will reach the loop while reversing
the initial segment, will reverse the loop, and then will restore the
initial segment. So we end up with a list where only the loop has been
reversed.
before +---o<--o<--+ v | o-->o-->o-->o-->o-->o-->o
after +-->o-->o---+ | V o-->o-->o-->o<--o<--o<--o
In the module below, we show that list_reversal
always terminates.
This requires ruling out inifitely-long lists i.e. assuming a finite
amount of memory.
use int.Int use int.NumOf use map.Map type loc val (=) (l1 l2: loc) : bool ensures { result <-> l1 = l2 } val constant null : loc type mem = { mutable next: loc -> loc } val mem: mem let cdr (p: loc) : loc requires { p <> null } ensures { result = mem.next p } = mem.next p let set_cdr (p: loc) (v: loc) : unit requires { p <> null } ensures { mem.next = (old mem.next)[p <- v] } = let m = mem.next in mem.next <- fun x -> if x = p then v else m x (* Finite memory hypothesis: the list is entirely contained in a finite set `s` of `n` cells *) predicate valid_cells (s: int -> loc) (n: int) = (forall i. 0 <= i < n -> s i <> null) && (forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> s i <> s j) predicate inside_memory (s: int -> loc) (n: int) (l: loc) = l = null || exists i. 0 <= i < n && l = s[i] predicate finite_memory (m: mem) (s: int -> loc) (n: int) = forall i. 0 <= i < n -> inside_memory s n (m.next s[i]) (* The variant is lexicographic, as follows: - as long as we still discover new cells, we mark them with increasing numbers (with function `idx` below) and the number of unmarked cells decreases; - once we reach a marked cell, this means we are back in the initial segment and then the mark decreases. *) function seen (s: int -> loc) (idx: loc -> int) (lo hi: int) : int = numof (fun i -> idx s[i] > 0) lo hi let ghost set_idx (s: int -> loc) (n: int) (idx: loc -> int) (l: loc) (k: int) requires { valid_cells s n } requires { inside_memory s n l } requires { l <> null } requires { idx l = -1 } requires { k = seen s idx 0 n >= 0 } ensures { seen s idx[l <- k+1] 0 n = 1 + seen s idx 0 n } = assert { seen s idx[l <- k+1] 0 n = 1 + seen s idx 0 n by exists il. 0 <= il < n && l = s[il] so seen s idx 0 n = seen s idx 0 il + seen s idx (il+1) n && seen s idx[l <- k+1] 0 n = seen s idx[l <- k+1] 0 il + 1 + seen s idx[l <- k+1] (il+1) n } let list_reversal (ghost s: int -> loc) (ghost n: int) (l: loc) : (r: loc) requires { n >= 0 } requires { valid_cells s n } requires { finite_memory mem s n } requires { inside_memory s n l } = let ref l = l in let ref r = null in (* marking function: -1 for unmarked / 0 for null / >0 for marked *) let ghost ref idx = fun p -> if p = null then 0 else -1 in let ghost ref k = 0 in (* last mark *) while l <> null do invariant { inside_memory s n l } invariant { inside_memory s n r } invariant { finite_memory mem s n } invariant { k = seen s idx 0 n >= 0 } invariant { forall i. 0 <= i < n -> -1 <= idx s[i] <= k } invariant { forall p. idx p = 0 <-> p = null } invariant { if idx l = -1 then idx r = k && forall i. 0 <= i < n -> 0 < idx s[i] -> idx (mem.next s[i]) = idx s[i] - 1 else forall i. 0 <= i < n -> 0 < idx s[i] <= idx l -> idx (mem.next s[i]) = idx s[i] - 1 } variant { n - k, 1 + idx l } if idx l = -1 then (set_idx s n idx l k; k <- k + 1; idx <- idx[l <- k]); let tmp = l in l <- cdr l; set_cdr tmp r; r <- tmp; done; return r end
download ZIP archive
Why3 Proof Results for Project "linked_list_rev"
Theory "linked_list_rev.InPlaceRev": fully verified
Obligations | Alt-Ergo 2.3.3 | Alt-Ergo 2.5.3 | |
VC for mem_decomp | 0.04 | 0.05 | |
VC for list_seg_frame_ext | 0.04 | 0.05 | |
VC for list_seg_functional | 0.03 | 0.05 | |
VC for list_seg_sublistl | 0.05 | 0.06 | |
VC for list_seg_no_repet | 0.06 | 0.06 | |
VC for list_seg_append | 0.03 | 0.04 | |
VC for app | --- | --- | |
split_vc | |||
postcondition | 0.01 | 0.02 | |
loop invariant init | 0.00 | 0.01 | |
loop invariant init | 0.00 | 0.02 | |
loop invariant init | 0.00 | 0.01 | |
loop invariant init | 0.01 | 0.02 | |
loop invariant init | 0.01 | 0.02 | |
precondition | 0.01 | 0.01 | |
unreachable point | 0.01 | 0.01 | |
assertion | 0.02 | 0.04 | |
assertion | 0.01 | 0.02 | |
precondition | 0.00 | 0.02 | |
loop variant decrease | 0.02 | 0.03 | |
loop invariant preservation | 0.00 | 0.02 | |
loop invariant preservation | 0.06 | 0.07 | |
loop invariant preservation | 0.02 | 0.03 | |
loop invariant preservation | 0.04 | 0.06 | |
loop invariant preservation | 0.06 | 0.07 | |
precondition | 0.00 | 0.01 | |
assertion | 0.02 | 0.03 | |
assertion | 0.02 | 0.03 | |
assertion | 0.08 | 0.08 | |
postcondition | 0.04 | 0.05 | |
VC for in_place_reverse | --- | --- | |
split_vc | |||
loop invariant init | 0.00 | 0.01 | |
loop invariant init | 0.00 | 0.01 | |
loop invariant init | 0.00 | 0.02 | |
loop invariant init | 0.00 | 0.01 | |
precondition | 0.00 | 0.01 | |
assertion | 0.02 | 0.03 | |
unreachable point | 0.01 | 0.01 | |
loop variant decrease | 0.02 | 0.03 | |
loop invariant preservation | 0.02 | 0.04 | |
loop invariant preservation | 0.02 | 0.03 | |
loop invariant preservation | 0.21 | 0.22 | |
loop invariant preservation | 0.01 | 0.02 | |
postcondition | 0.01 | 0.02 |
Theory "linked_list_rev.InPlaceRevSeq": fully verified
Obligations | Alt-Ergo 2.0.0 | Alt-Ergo 2.3.3 | Alt-Ergo 2.5.3 | CVC4 1.8 | Eprover 2.0 | Z3 4.12.1 | Z3 4.12.2 | |||||
non_empty_seq | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
VC for mem_decomp | --- | --- | --- | --- | --- | --- | --- | |||||
split_vc | ||||||||||||
precondition | --- | 0.01 | 0.01 | --- | --- | --- | --- | |||||
assertion | --- | 0.01 | 0.01 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
variant decrease | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
precondition | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
postcondition | --- | 0.08 | 0.12 | --- | --- | --- | --- | |||||
list_seg_frame_ext | --- | 0.03 | 0.03 | --- | --- | --- | --- | |||||
VC for list_seg_functional | --- | --- | --- | --- | --- | --- | --- | |||||
split_vc | ||||||||||||
assertion | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.02 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.00 | --- | --- | --- | --- | |||||
variant decrease | --- | 0.01 | 0.01 | --- | --- | --- | --- | |||||
precondition | --- | 0.05 | 0.07 | --- | --- | --- | --- | |||||
precondition | --- | 0.10 | 0.16 | --- | --- | --- | --- | |||||
postcondition | --- | 6.02 | 2.03 | --- | --- | --- | --- | |||||
VC for list_seg_tail | --- | --- | --- | --- | --- | --- | --- | |||||
split_vc | ||||||||||||
precondition | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
variant decrease | --- | 0.01 | 0.01 | --- | --- | --- | --- | |||||
precondition | --- | 0.03 | 0.04 | --- | --- | --- | --- | |||||
precondition | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
postcondition | --- | 0.08 | 0.11 | --- | --- | --- | --- | |||||
VC for list_seg_append | --- | --- | --- | --- | --- | --- | --- | |||||
split_vc | ||||||||||||
precondition | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
variant decrease | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
precondition | --- | 0.01 | 0.01 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
postcondition | --- | 3.44 | 4.17 | --- | --- | --- | --- | |||||
seq_tail_append | --- | 0.03 | 0.03 | --- | --- | --- | --- | |||||
VC for list_seg_prefix | --- | --- | --- | --- | --- | --- | --- | |||||
split_vc | ||||||||||||
precondition | --- | 0.01 | 0.01 | --- | --- | --- | --- | |||||
precondition | --- | 0.01 | 0.01 | --- | --- | --- | --- | |||||
precondition | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
variant decrease | --- | 0.02 | 0.03 | --- | --- | --- | --- | |||||
precondition | --- | 0.02 | 0.02 | --- | --- | --- | --- | |||||
postcondition | --- | --- | 4.75 | --- | --- | 0.04 | --- | |||||
VC for list_seg_sublistl | --- | --- | --- | --- | --- | --- | --- | |||||
split_vc | ||||||||||||
assertion | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
variant decrease | --- | 0.02 | 0.02 | --- | --- | --- | --- | |||||
precondition | --- | 0.02 | 0.03 | --- | --- | --- | --- | |||||
postcondition | --- | --- | --- | --- | --- | --- | --- | |||||
destruct H | ||||||||||||
postcondition | --- | 0.00 | 0.00 | --- | --- | --- | --- | |||||
postcondition | --- | --- | --- | --- | --- | --- | --- | |||||
assert (l1 = empty) | ||||||||||||
asserted formula | --- | --- | --- | --- | 0.05 | --- | --- | |||||
postcondition | --- | --- | --- | --- | --- | --- | --- | |||||
assert (forall l:seq 'a. empty ++ l = l) | ||||||||||||
asserted formula | --- | --- | --- | --- | --- | --- | --- | |||||
assert (forall l:seq 'a. empty ++ l == l) | ||||||||||||
asserted formula | --- | 0.03 | 0.05 | --- | --- | --- | --- | |||||
asserted formula | --- | 0.02 | 0.03 | --- | --- | --- | --- | |||||
postcondition | --- | 0.01 | 0.01 | --- | --- | --- | --- | |||||
get_tail | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
tail_suffix | --- | 0.02 | 0.03 | --- | --- | --- | --- | |||||
VC for list_seg_no_repet | --- | --- | --- | --- | --- | --- | --- | |||||
split_vc | ||||||||||||
precondition | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.02 | --- | --- | --- | --- | |||||
precondition | --- | 0.56 | 0.27 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.02 | --- | --- | --- | --- | |||||
precondition | --- | 0.01 | 0.03 | --- | --- | --- | --- | |||||
assertion | --- | 0.03 | 0.05 | --- | --- | --- | --- | |||||
assertion | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
variant decrease | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
precondition | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
assertion | --- | --- | --- | 0.33 | --- | --- | --- | |||||
postcondition | --- | 0.05 | 0.07 | --- | --- | --- | --- | |||||
VC for app | --- | --- | --- | --- | --- | --- | --- | |||||
split_vc | ||||||||||||
postcondition | --- | 0.03 | 0.04 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
loop invariant init | --- | 0.00 | 0.02 | --- | --- | --- | --- | |||||
loop invariant init | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
loop invariant init | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
loop invariant init | --- | 0.02 | 0.03 | --- | --- | --- | --- | |||||
loop invariant init | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.02 | --- | --- | --- | --- | |||||
assertion | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
assertion | --- | 0.06 | 0.09 | --- | --- | --- | --- | |||||
precondition | --- | 0.01 | 0.01 | --- | --- | --- | --- | |||||
precondition | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
loop variant decrease | --- | 0.04 | 0.05 | --- | --- | --- | --- | |||||
loop invariant preservation | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
loop invariant preservation | --- | 0.44 | 0.29 | --- | --- | --- | --- | |||||
loop invariant preservation | --- | 0.01 | 0.03 | --- | --- | --- | --- | |||||
loop invariant preservation | --- | 0.05 | 0.05 | --- | --- | --- | --- | |||||
loop invariant preservation | 1.64 | --- | --- | --- | --- | --- | --- | |||||
remove zero,one,(-),(>),(<=),(>=),get1,set1,([]'),([<-]'),(!),([]),singleton,cons,snoc,(++),reverse,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,length_nonnegative,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'def,([.._])'def,mem_append,mem_tail,eq_loc'spec,non_empty_seq,list_seg_frame_ext,list_seg_functional,list_seg_tail,list_seg_append,seq_tail_append,list_seg_prefix,list_seg_sublistl,get_tail,tail_suffix,Requires2,Requires1,Requires,Ensures11,H1,Ensures10,LoopInvariant8,LoopInvariant7,Ensures9,H,Assert,Ensures8,Ensures7,Ensures6,Ensures5,Ensures4,Ensures3,LoopInvariant3,LoopInvariant2,LoopInvariant1 | ||||||||||||
loop invariant preservation | 0.04 | 0.05 | 0.06 | --- | --- | --- | --- | |||||
precondition | --- | 0.01 | 0.01 | --- | --- | --- | --- | |||||
assertion | --- | 0.20 | 1.83 | --- | --- | --- | --- | |||||
assertion | --- | 0.07 | 0.07 | --- | --- | --- | --- | |||||
assertion | --- | 2.06 | 3.01 | --- | --- | --- | --- | |||||
postcondition | --- | --- | --- | --- | --- | --- | 0.19 | |||||
VC for in_place_reverse | --- | --- | --- | --- | --- | --- | --- | |||||
split_vc | ||||||||||||
loop invariant init | --- | 0.00 | 0.02 | --- | --- | --- | --- | |||||
loop invariant init | --- | 0.01 | 0.01 | --- | --- | --- | --- | |||||
loop invariant init | --- | 0.01 | 0.01 | --- | --- | --- | --- | |||||
loop invariant init | --- | 0.02 | 0.04 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
precondition | --- | 0.00 | 0.01 | --- | --- | --- | --- | |||||
assertion | --- | 0.34 | 0.13 | --- | --- | --- | --- | |||||
precondition | --- | 0.01 | 0.02 | --- | --- | --- | --- | |||||
loop variant decrease | --- | 0.03 | 0.04 | --- | --- | --- | --- | |||||
loop invariant preservation | --- | 0.28 | 0.10 | --- | --- | --- | --- | |||||
loop invariant preservation | --- | --- | 1.93 | --- | --- | --- | --- | |||||
loop invariant preservation | --- | --- | --- | 0.55 | --- | --- | --- | |||||
loop invariant preservation | --- | --- | --- | --- | --- | --- | --- | |||||
assert (length pM1 > 0) | ||||||||||||
asserted formula | --- | 0.02 | 0.02 | --- | --- | --- | --- | |||||
loop invariant preservation | --- | --- | --- | --- | --- | --- | --- | |||||
remove LoopInvariant,LoopInvariant1,LoopInvariant2,LoopInvariant4,LoopInvariant5,LoopInvariant6,Ensures2,Ensures3,Ensures4,Ensures5,Ensures6,Ensures7,Ensures8 | ||||||||||||
loop invariant preservation | 1.17 | --- | --- | --- | --- | --- | --- | |||||
remove zero,one,(-),(>),(<=),(>=),get1,set1,([]'),([<-]'),(!),([]),singleton,cons,snoc,(++),mem,disjoint,no_repet,list_seg,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,length_nonnegative,empty'def,set'spec,set'def,([<-])'def,singleton'spec,snoc'spec,([..])'def,([.._])'def,mem_append,mem_tail,eq_loc'spec,non_empty_seq,list_seg_frame_ext,list_seg_functional,list_seg_tail,list_seg_append,seq_tail_append,list_seg_prefix,list_seg_sublistl,get_tail,tail_suffix,list_seg_no_repet,Requires,H,Assert | ||||||||||||
loop invariant preservation | 0.02 | 0.05 | 0.06 | --- | --- | --- | --- | |||||
postcondition | --- | 0.08 | 0.06 | --- | --- | --- | --- |
Theory "linked_list_rev.YetAnotherInPlaceRev": fully verified
Obligations | Alt-Ergo 2.4.0 | Alt-Ergo 2.5.3 | CVC4 1.7 | CVC5 1.0.5 | Z3 4.12.2 | |
VC for cdr | --- | 0.01 | --- | 0.07 | --- | |
VC for set_cdr | --- | 0.01 | --- | 0.09 | --- | |
VC for list_reversal | --- | 2.91 | --- | --- | 0.04 | |
VC for is_list | --- | 0.01 | --- | 0.07 | --- | |
VC for cells_of_list | --- | --- | --- | --- | --- | |
split_vc | ||||||
precondition | --- | 0.02 | --- | 0.04 | --- | |
variant decrease | --- | 0.01 | --- | 0.02 | --- | |
precondition | --- | 0.01 | --- | 0.03 | --- | |
precondition | --- | --- | --- | 0.56 | --- | |
postcondition | 0.79 | 0.67 | --- | --- | --- | |
postcondition | 0.06 | 0.06 | --- | --- | --- | |
VC for list_of_cells | --- | --- | --- | --- | 1.18 | |
split_vc | ||||||
precondition | --- | 0.01 | --- | 0.04 | --- | |
variant decrease | --- | 0.01 | --- | 0.04 | --- | |
precondition | --- | 0.00 | --- | 0.03 | --- | |
precondition | --- | 0.03 | --- | 0.08 | --- | |
precondition | --- | 0.02 | --- | 0.10 | --- | |
postcondition | --- | --- | --- | 0.24 | --- | |
VC for list_reversal_final | --- | --- | 0.26 | --- | --- |
Theory "linked_list_rev.Termination": fully verified
Obligations | Alt-Ergo 2.4.0 | Alt-Ergo 2.5.3 | CVC5 1.0.5 | Z3 4.12.2 | ||||
VC for cdr | --- | 0.01 | 0.03 | --- | ||||
VC for set_cdr | --- | 0.01 | 0.03 | --- | ||||
VC for set_idx | --- | --- | --- | --- | ||||
split_vc | ||||||||
assertion | --- | --- | --- | --- | ||||
split_vc | ||||||||
assertion | --- | 0.02 | 0.04 | --- | ||||
VC for set_idx | --- | 0.20 | 0.13 | --- | ||||
VC for set_idx | --- | 0.28 | 0.55 | --- | ||||
VC for set_idx | --- | --- | --- | 1.02 | ||||
postcondition | --- | 0.02 | 0.04 | --- | ||||
VC for list_reversal | --- | --- | --- | --- | ||||
split_vc | ||||||||
loop invariant init | --- | 0.00 | 0.04 | --- | ||||
loop invariant init | --- | 0.01 | 0.04 | --- | ||||
loop invariant init | --- | 0.00 | 0.03 | --- | ||||
loop invariant init | --- | 1.40 | 0.05 | --- | ||||
loop invariant init | --- | 0.02 | 0.05 | --- | ||||
loop invariant init | --- | 0.01 | 0.04 | --- | ||||
loop invariant init | --- | 0.04 | 0.04 | --- | ||||
precondition | --- | 0.01 | 0.03 | --- | ||||
precondition | --- | 0.01 | 0.03 | --- | ||||
precondition | --- | 0.01 | 0.03 | 0.01 | ||||
precondition | --- | 0.02 | 0.04 | --- | ||||
precondition | --- | 0.01 | 0.03 | --- | ||||
precondition | --- | 0.02 | 0.03 | --- | ||||
precondition | --- | 0.02 | 0.04 | --- | ||||
loop variant decrease | --- | 0.03 | 0.06 | --- | ||||
loop invariant preservation | --- | 0.03 | 0.08 | --- | ||||
loop invariant preservation | --- | 0.02 | 0.04 | --- | ||||
loop invariant preservation | --- | 0.04 | 0.24 | --- | ||||
loop invariant preservation | --- | 0.02 | 0.04 | --- | ||||
loop invariant preservation | --- | 0.04 | 0.05 | --- | ||||
loop invariant preservation | --- | 0.03 | 0.04 | --- | ||||
loop invariant preservation | --- | --- | --- | --- | ||||
case (idx l = -1) | ||||||||
true case (loop invariant preservation) | --- | 0.03 | 0.07 | --- | ||||
false case (loop invariant preservation) | --- | 0.04 | 0.07 | --- | ||||
case (idx l = 0) | ||||||||
true case (loop invariant preservation) | --- | 0.02 | 0.04 | --- | ||||
false case (loop invariant preservation) | --- | 0.11 | 0.09 | --- | ||||
precondition | --- | 0.00 | 0.04 | --- | ||||
precondition | --- | 0.01 | 0.04 | --- | ||||
loop variant decrease | --- | --- | --- | --- | ||||
right | ||||||||
right case | --- | --- | --- | --- | ||||
split_vc | ||||||||
right case | --- | 0.02 | 0.05 | --- | ||||
right case | --- | 0.02 | 0.05 | --- | ||||
loop invariant preservation | --- | 0.03 | 0.08 | --- | ||||
loop invariant preservation | --- | 0.01 | 0.03 | --- | ||||
loop invariant preservation | --- | 0.03 | 0.43 | --- | ||||
loop invariant preservation | --- | 0.01 | 0.04 | --- | ||||
loop invariant preservation | --- | 0.02 | 0.05 | --- | ||||
loop invariant preservation | 0.01 | 0.02 | --- | --- | ||||
loop invariant preservation | --- | --- | --- | --- | ||||
case (idx l = 0) | ||||||||
true case (loop invariant preservation) | --- | --- | --- | --- | ||||
rewrite h | ||||||||
true case (loop invariant preservation) | --- | --- | --- | --- | ||||
compute_in_goal | ||||||||
true case (loop invariant preservation) | --- | 0.02 | 0.04 | --- | ||||
false case (loop invariant preservation) | --- | 0.02 | 0.04 | --- |