## VerifyThis 2019: Cartesian trees

solution to VerifyThis 2019 challenge 2

**Authors:** Quentin Garchery

**Topics:** Data Structures / Trees

**Tools:** Why3

**References:** VerifyThis @ ETAPS 2019

**See also:** Cartesian Trees (from VerifyThis 2019) in SPARK

see also the index (by topic, by tool, by reference, by year)

# VerifyThis @ ETAPS 2019 competition Challenge 2: Cartesian Trees

Author: Quentin Garchery (LRI, Université Paris Sud)

use int.Int use list.ListRich use array.Array use exn.Exn

## PART A : All nearest smaller value

clone list.Sorted as Decr with type t = int, predicate le = (>=)

Implement the stack with a list

let function destruct l requires { not is_nil l } = match l with | Cons h t -> h, t end let function peek l requires { not is_nil l } ensures { mem result l } = let h, _ = destruct l in h let function tail l requires { not is_nil l } = let _, t = destruct l in t lemma destruct_peek_tail : forall l : list 'a. not is_nil l -> l = Cons (peek l) (tail l)

Compute the sequence of left neighbors

let smaller_left (s : array int) : array int (* Task 1 : left neighbor has smaller index *) ensures { forall y. 0 <= y < s.length -> result[y] < y } (* Task 2 : left neighbor has smaller value *) ensures { forall y. 0 <= y < s.length -> 0 <= result[y] -> s[result[y]] < s[y] } (* Task 3 : no smaller value between an element and its left neighbor *) ensures { forall x z. 0 <= x < s.length -> result[x] < z < x -> s[z] >= s[x] } ensures { result.length = s.length } = let n = s.length in let left = make n (-1) in let ref my_stack = Nil in for x = 0 to s.length - 1 do (* To show that the access are correct *) invariant { forall z. mem z my_stack -> 0 <= z < x } (* Good formation of the stack *) invariant { is_nil my_stack -> x = 0 } invariant { not is_nil my_stack -> peek my_stack = x-1 } invariant { Decr.sorted my_stack } (* Task 1 *) invariant { forall y. 0 <= y < x -> left[y] < y } (* Task 2 *) invariant { forall y. 0 <= y < x -> 0 <= left[y] -> s[left[y]] < s[y] } (* Show that we only need to look in the stack to find the nearest smaller value *) invariant { forall z. 0 <= z < x -> exists y. z <= y < x /\ mem y my_stack /\ s[y] <= s[z] } (* Task 3 *) invariant { forall y z. 0 <= y < x -> left[y] < z < y -> s[z] >= s[y] } label BeforeLoop in while not is_nil my_stack && s[peek my_stack] >= s[x] do (* Good formation of the stack *) invariant { forall z. mem z my_stack -> 0 <= z < x } invariant { Decr.sorted my_stack } (* Remember that what was removed from the stack was too big *) invariant { forall z. mem z (my_stack at BeforeLoop) -> s[z] >= s[x] \/ mem z my_stack } (* Make sure that stack elements at the right of the current top of the stack were previously removed *) invariant { forall z. not is_nil my_stack -> mem z my_stack -> z <= peek my_stack } (* Task 3 *) invariant { forall z. not is_nil my_stack -> peek my_stack < z < x -> s[z] >= s[x] } invariant { forall z. is_nil my_stack -> 0 <= z < x -> s[z] >= s[x] } variant { Length.length my_stack } my_stack <- tail my_stack done; assert { not is_nil my_stack -> s[peek my_stack] < s[x] }; if is_nil my_stack then left[x] <- -1 else left[x] <- peek my_stack; assert { 0 <= left[x] -> s[left[x]] < s[x] }; my_stack <- Cons x my_stack done; left

Same thing but for closest smaller right value : when there is no such value, return an integer greater than the length

val smaller_right (s : array int) : array int (* Task 1 : right neighbor has greater index *) ensures { forall y. 0 <= y < s.length -> result[y] > y } (* Task 2 : right neighbor has smaller value *) ensures { forall y. 0 <= y < s.length -> result[y] < s.length -> s[result[y]] < s[y] } (* Task 3 : no smaller value between an element and its right neighbor *) ensures { forall x z. 0 <= x < s.length -> x < z < result[x] -> s[z] >= s[x] } ensures { result.length = s.length }

## PART B : Construction of a Cartesian Tree

use option.Option type dir = { left : option int; right : option int } type dirs = array dir predicate parent (t : dirs) (p s : int) = t[p].left = Some s \/ t[p].right = Some s inductive descendant dirs int int = | Self : forall t p s. p = s -> descendant t p s | Son_left : forall t p s1 s2. descendant t p s1 -> t[s1].left = Some s2 -> descendant t p s2 | Son_right : forall t p s1 s2. descendant t p s1 -> t[s1].right = Some s2 -> descendant t p s2 predicate is_smallest (a : array int) (i : int) = 0 <= i < a.length /\ forall j. 0 <= j < a.length -> a[i] <= a[j]

Construct an array storing the eventual sons of a node

let construct_dirs (a : array int) : dirs requires { forall i j. 0 <= i < j < a.length -> a[i] <> a[j] } ensures { result.length = a.length } (* Task 2 ++, heap property : left and right sons have greater value than the parent left son is on the left in the array, right son is on the right between indices of parent and son there is no smaller value *) ensures { forall j v. 0 <= j < a.length -> (result[j].left = Some v -> a[v] > a[j] /\ 0 <= v < j /\ forall x. v < x < j -> a[x] > a[j]) /\ (result[j].right = Some v -> a[v] > a[j] /\ j < v < a.length /\ forall x. j < x < v -> a[x] > a[j]) } ensures { forall p s. 0 <= p < a.length -> descendant result p s -> 0 <= s < a.length /\ a[s] >= a[p] } (* Task3, in-order traversal : every "left-descendant" is located on the left in the array every "right-descendant" is located on the right in the array *) ensures { forall p1 p2 s. 0 <= p1 < a.length -> descendant result p2 s -> (result[p1].left = Some p2 -> s < p1) /\ (result[p1].right = Some p2 -> s > p1) } (* Task 1, well-formedness *) (* Every non-minimal element has a parent *) ensures { forall i k. 0 <= i < a.length -> 0 <= k < a.length -> a[k] < a[i] -> exists sm. 0 <= sm < a.length /\ parent result sm i } ensures { forall i. 0 <= i < a.length -> (is_smallest a i \/ (exists sm. 0 <= sm < a.length /\ parent result sm i)) } (* Every element has at most one parent *) ensures { forall p1 p2 s. 0 <= p1 < a.length -> 0 <= p2 < a.length -> 0 <= s < a.length -> parent result p1 s -> parent result p2 s -> p1 = p2 } (* No cycles *) ensures { forall p1 p2 s. 0 <= p1 < a.length -> 0 <= p2 < a.length -> 0 <= s < a.length -> parent result p1 p2 -> descendant result p2 s -> p1 <> s } = let n = a.length in let s_left = smaller_left a in let s_right = smaller_right a in let dirs = Array.make n {left = None; right = None} in for i = 0 to n-1 do (* Task 2 ++ *) invariant { forall j v. 0 <= j < a.length -> (dirs[j].left = Some v -> a[v] > a[j] /\ 0 <= v < j /\ forall x. v < x < j -> a[x] >= a[j]) /\ (dirs[j].right = Some v -> a[v] > a[j] /\ j < v < a.length /\ forall x. j < x < v -> a[x] >= a[j]) } (* Show that once a parent is set-up in <dirs>, it does not change *) invariant { forall j. 0 <= j < i -> if s_left[j] >= 0 && s_right[j] >= n then dirs[s_left[j]].right = Some j else if s_left[j] < 0 && s_right[j] < n then dirs[s_right[j]].left = Some j else if s_left[j] >= 0 && s_right[j] < n then if a[s_left[j]] > a[s_right[j]] then dirs[s_left[j]].right = Some j else dirs[s_right[j]].left = Some j else true } invariant { forall j p. 0 <= j < a.length -> 0 <= p < a.length -> (dirs[p].right = Some j -> p = s_left[j] /\ (s_right[j] < n -> a[s_left[j]] > a[s_right[j]]) ) /\ (dirs[p].left = Some j -> p = s_right[j] /\ (s_left[j] >= 0 -> a[s_left[j]] <= a[s_right[j]])) } let li = s_left[i] in let ri = s_right[i] in if li >= 0 then if ri < n then if a[li] > a[ri] then dirs[li] <- { dirs[li] with right = Some i } else dirs[ri] <- { dirs[ri] with left = Some i } else dirs[li] <- { dirs[li] with right = Some i } else if ri < n then dirs[ri] <- { dirs[ri] with left = Some i } done; dirs

The function <par> finds the parent of a node and is used to define <all_descendant_root>. This last lemma function is useful to show that every node is reachable from the root

let par (a : array int) (dirs : array dir) (j : int) requires { exists sm. 0 <= sm < a.length /\ parent dirs sm j } requires { a.length = dirs.length } requires { forall j v. 0 <= j < a.length -> (dirs[j].left = Some v -> a[v] > a[j] /\ 0 <= v < j /\ forall x. v < x < j -> a[x] > a[j]) /\ (dirs[j].right = Some v -> a[v] > a[j] /\ j < v < a.length /\ forall x. j < x < v -> a[x] > a[j]) } ensures { 0 <= result < a.length } ensures { parent dirs result j } = assert { not a.length = 0 }; let ref res = 0 in for i = 0 to a.length - 1 do invariant { 0 <= res < a.length } invariant { parent dirs res j \/ exists sm. i <= sm < a.length /\ parent dirs sm j } match dirs[i].left with | Some jl -> if jl = j then res <- i | None -> () end; match dirs[i].right with | Some jr -> if jr = j then res <- i | None -> () end done; res let rec lemma all_descendant_root a dirs root j variant { a[j] - a[root] } requires { a.length = dirs.length } requires { forall j v. 0 <= j < a.length -> (dirs[j].left = Some v -> a[v] > a[j] /\ 0 <= v < j /\ forall x. v < x < j -> a[x] > a[j]) /\ (dirs[j].right = Some v -> a[v] > a[j] /\ j < v < a.length /\ forall x. j < x < v -> a[x] > a[j]) } requires { forall i j. 0 <= i < j < a.length -> a[i] <> a[j] } requires { 0 <= j < a.length /\ 0 <= root < a.length } requires { is_smallest a root } requires { forall i. 0 <= i < a.length -> (is_smallest a i \/ (exists sm. 0 <= sm < a.length /\ parent dirs sm i)) } ensures { descendant dirs root j } = if a[j] <> a[root] then all_descendant_root a dirs root (par a dirs j)

Finds the root of the direction tree : it's the smallest element in the array

let find_smaller a = ensures { match result with | Some mv -> is_smallest a mv | None -> a.length = 0 end } let ref m = None in for i = 0 to a.length - 1 do invariant { match m with | Some mv -> 0 <= mv < a.length /\ forall j. 0 <= j < i -> a[mv] <= a[j] | None -> i = 0 end } match m with | Some mv -> if a[mv] > a[i] then m <- Some i | _ -> m <- Some i end done; m

The other way to define descendant. Useful here because it follows the definition of <traversal>

lemma other_descendant : forall t p1 p2 s. parent t p1 p2 -> descendant t p2 s -> descendant t p1 s lemma inv_other_descendant : forall t p1 s. descendant t p1 s -> p1 = s \/ exists p2. parent t p1 p2 /\ descendant t p2 s clone list.Sorted as StrictIncr with type t = int, predicate le = (<)

In-order traversal, we store the indices we traversed

let rec traversal (a : array int) dirs top (ghost s : int) (ghost e) variant { e - s } requires { dirs.length = a.length } requires { 0 <= s <= e <= a.length } requires { forall p1 p2 s. 0 <= p1 < a.length -> descendant dirs p2 s -> (dirs[p1].left = Some p2 -> s < p1) /\ (dirs[p1].right = Some p2 -> s > p1) } requires { forall i j. 0 <= i < j < a.length -> a[i] <> a[j] } requires { match top with | Some top -> forall son. descendant dirs top son <-> s <= son < e | None -> s = e end } ensures { forall x. mem x result <-> s <= x < e } ensures { StrictIncr.sorted result } = match top with | None -> Nil | Some top -> assert { s <= top < e by descendant dirs top top }; let dir = dirs[top] in traversal a dirs dir.left s top ++ Cons top ( traversal a dirs dir.right (top+1) e) end

We traverse the tree <construct_dirs a> in-order from the root <find_smaller a>, and we collect the indices. Last 2 arguments of <traversal> are ghost.

We show that the result is the list [0..(a.length-1)], the in-order traversal of the tree traverses elements from 0 to (a.length-1)

let in_order a requires { forall i j. 0 <= i < j < a.length -> a[i] <> a[j] } ensures { forall x. mem x result <-> 0 <= x < a.length } ensures { StrictIncr.sorted result } = traversal a (construct_dirs a) (find_smaller a) 0 a.length

download ZIP archive

# Why3 Proof Results for Project "verifythis_2019_cartesian_trees"

## Theory "verifythis_2019_cartesian_trees.Top": fully verified

Obligations | Alt-Ergo 2.3.3 | Alt-Ergo 2.4.1 | Alt-Ergo 2.4.2 | CVC5 1.0.5 | |||||

Decr.Transitive.Trans | 0.00 | --- | --- | --- | |||||

VC for destruct | 0.01 | --- | --- | --- | |||||

VC for peek | 0.01 | --- | --- | --- | |||||

VC for tail | 0.00 | --- | --- | --- | |||||

destruct_peek_tail | 0.02 | --- | --- | --- | |||||

VC for smaller_left | --- | --- | --- | --- | |||||

split_vc | |||||||||

array creation size | 0.00 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.00 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.00 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.00 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

index in array bounds | 0.00 | --- | --- | --- | |||||

precondition | 0.00 | --- | --- | --- | |||||

index in array bounds | 0.01 | --- | --- | --- | |||||

precondition | 0.01 | --- | --- | --- | |||||

loop variant decrease | 0.03 | --- | --- | --- | |||||

loop invariant preservation | --- | --- | --- | 0.31 | |||||

loop invariant preservation | 0.03 | --- | --- | --- | |||||

loop invariant preservation | 0.04 | --- | --- | --- | |||||

loop invariant preservation | 0.89 | --- | --- | --- | |||||

loop invariant preservation | 0.86 | --- | --- | --- | |||||

loop invariant preservation | 0.21 | --- | --- | --- | |||||

assertion | 0.01 | --- | --- | --- | |||||

index in array bounds | 0.01 | --- | --- | --- | |||||

assertion | 0.02 | --- | --- | --- | |||||

loop invariant preservation | 0.04 | --- | --- | --- | |||||

loop invariant preservation | 0.02 | --- | --- | --- | |||||

loop invariant preservation | 0.05 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.07 | --- | --- | --- | |||||

loop invariant preservation | 0.19 | --- | --- | --- | |||||

loop invariant preservation | 0.03 | --- | --- | --- | |||||

loop invariant preservation | 0.06 | --- | --- | --- | |||||

precondition | 0.01 | --- | --- | --- | |||||

index in array bounds | 0.01 | --- | --- | --- | |||||

assertion | 0.02 | --- | --- | --- | |||||

loop invariant preservation | 0.06 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.08 | --- | --- | --- | |||||

loop invariant preservation | 0.07 | --- | --- | --- | |||||

loop invariant preservation | 0.18 | --- | --- | --- | |||||

loop invariant preservation | --- | --- | --- | 0.43 | |||||

loop invariant preservation | 2.56 | --- | --- | --- | |||||

loop invariant preservation | 0.27 | --- | --- | --- | |||||

postcondition | 0.01 | --- | --- | --- | |||||

postcondition | 0.02 | --- | --- | --- | |||||

postcondition | 0.02 | --- | --- | --- | |||||

postcondition | 0.01 | --- | --- | --- | |||||

out of loop bounds | 0.00 | --- | --- | --- | |||||

VC for construct_dirs | --- | --- | --- | --- | |||||

split_vc | |||||||||

array creation size | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.02 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.02 | --- | --- | --- | |||||

index in array bounds | 0.01 | --- | --- | --- | |||||

index in array bounds | 0.01 | --- | --- | --- | |||||

index in array bounds | 0.02 | --- | --- | --- | |||||

index in array bounds | 0.02 | --- | --- | --- | |||||

index in array bounds | 0.02 | --- | --- | --- | |||||

index in array bounds | 0.02 | --- | --- | --- | |||||

loop invariant preservation | --- | --- | --- | --- | |||||

case (j = li) | |||||||||

true case (loop invariant preservation) | 0.18 | --- | --- | --- | |||||

false case (loop invariant preservation) | --- | 2.76 | --- | --- | |||||

loop invariant preservation | --- | --- | --- | 0.18 | |||||

loop invariant preservation | --- | --- | --- | --- | |||||

case (p = li) | |||||||||

true case (loop invariant preservation) | 0.08 | --- | --- | --- | |||||

false case (loop invariant preservation) | 1.13 | --- | --- | --- | |||||

index in array bounds | 0.02 | --- | --- | --- | |||||

index in array bounds | 0.02 | --- | --- | --- | |||||

loop invariant preservation | --- | --- | --- | --- | |||||

case (j = ri) | |||||||||

true case (loop invariant preservation) | 0.18 | --- | --- | --- | |||||

false case (loop invariant preservation) | 3.21 | --- | --- | --- | |||||

loop invariant preservation | --- | --- | --- | 0.33 | |||||

loop invariant preservation | --- | --- | --- | --- | |||||

case (p = ri) | |||||||||

true case (loop invariant preservation) | 0.06 | --- | --- | --- | |||||

false case (loop invariant preservation) | 0.73 | --- | --- | --- | |||||

index in array bounds | 0.02 | --- | --- | --- | |||||

index in array bounds | 0.02 | --- | --- | --- | |||||

loop invariant preservation | --- | --- | --- | --- | |||||

case (j = li) | |||||||||

true case (loop invariant preservation) | 0.11 | --- | --- | --- | |||||

false case (loop invariant preservation) | 0.58 | --- | --- | --- | |||||

loop invariant preservation | 0.88 | --- | --- | --- | |||||

loop invariant preservation | --- | --- | --- | --- | |||||

case (p = li) | |||||||||

true case (loop invariant preservation) | 0.06 | --- | --- | --- | |||||

false case (loop invariant preservation) | 0.53 | --- | --- | --- | |||||

index in array bounds | 0.02 | --- | --- | --- | |||||

index in array bounds | 0.02 | --- | --- | --- | |||||

loop invariant preservation | --- | --- | --- | --- | |||||

case (j = ri) | |||||||||

true case (loop invariant preservation) | 0.12 | --- | --- | --- | |||||

false case (loop invariant preservation) | 0.48 | --- | --- | --- | |||||

loop invariant preservation | 0.71 | --- | --- | --- | |||||

loop invariant preservation | --- | --- | --- | --- | |||||

case (p = ri) | |||||||||

true case (loop invariant preservation) | 0.04 | --- | --- | --- | |||||

false case (loop invariant preservation) | 0.71 | --- | --- | --- | |||||

loop invariant preservation | --- | --- | --- | --- | |||||

case (j = ri) | |||||||||

true case (loop invariant preservation) | 0.02 | --- | --- | --- | |||||

false case (loop invariant preservation) | 0.06 | --- | --- | --- | |||||

loop invariant preservation | 0.04 | --- | --- | --- | |||||

loop invariant preservation | --- | --- | --- | --- | |||||

case (p = ri) | |||||||||

true case (loop invariant preservation) | 0.02 | --- | --- | --- | |||||

false case (loop invariant preservation) | 0.03 | --- | --- | --- | |||||

postcondition | 0.01 | --- | --- | --- | |||||

postcondition | 0.04 | --- | --- | --- | |||||

postcondition | --- | --- | --- | --- | |||||

revert p | |||||||||

postcondition | --- | --- | --- | --- | |||||

revert s | |||||||||

postcondition | --- | --- | --- | --- | |||||

induction_pr | |||||||||

postcondition | 0.02 | --- | --- | --- | |||||

postcondition | 0.04 | --- | --- | --- | |||||

postcondition | 0.04 | --- | --- | --- | |||||

postcondition | --- | --- | --- | --- | |||||

revert p2 | |||||||||

postcondition | --- | --- | --- | --- | |||||

revert s | |||||||||

postcondition | --- | --- | --- | --- | |||||

induction_pr | |||||||||

postcondition | 0.02 | --- | --- | --- | |||||

postcondition | --- | --- | --- | --- | |||||

split_vc | |||||||||

VC for construct_dirs | 0.02 | --- | --- | --- | |||||

VC for construct_dirs | 0.06 | --- | --- | --- | |||||

postcondition | 0.08 | --- | --- | --- | |||||

postcondition | --- | --- | --- | --- | |||||

unfold parent | |||||||||

postcondition | 0.89 | --- | --- | --- | |||||

postcondition | 0.02 | --- | --- | --- | |||||

postcondition | 0.04 | --- | --- | --- | |||||

postcondition | 0.03 | --- | --- | --- | |||||

out of loop bounds | 0.02 | --- | --- | --- | |||||

VC for par | --- | --- | --- | --- | |||||

split_vc | |||||||||

assertion | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

loop invariant init | 0.01 | --- | --- | --- | |||||

index in array bounds | 0.01 | --- | --- | --- | |||||

index in array bounds | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.02 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.02 | --- | --- | --- | |||||

index in array bounds | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.02 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.04 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.04 | --- | --- | --- | |||||

index in array bounds | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.03 | --- | --- | --- | |||||

loop invariant preservation | 0.01 | --- | --- | --- | |||||

loop invariant preservation | 0.02 | --- | --- | --- | |||||

postcondition | 0.01 | --- | --- | --- | |||||

postcondition | 0.01 | --- | --- | --- | |||||

out of loop bounds | 0.01 | --- | --- | --- | |||||

VC for all_descendant_root | --- | --- | --- | --- | |||||

split_vc | |||||||||

index in array bounds | 0.01 | --- | --- | --- | |||||

index in array bounds | 0.01 | --- | --- | --- | |||||

precondition | --- | --- | --- | --- | |||||

assert (not is_smallest a j) | |||||||||

asserted formula | 0.01 | --- | --- | --- | |||||

precondition | 0.01 | --- | --- | --- | |||||

precondition | 0.01 | --- | --- | --- | |||||

precondition | 0.04 | --- | --- | --- | |||||

variant decrease | 0.02 | --- | --- | --- | |||||

precondition | 0.00 | --- | --- | --- | |||||

precondition | 0.04 | --- | --- | --- | |||||

precondition | 0.02 | --- | --- | --- | |||||

precondition | 0.01 | --- | --- | --- | |||||

precondition | 0.01 | --- | --- | --- | |||||

precondition | 0.02 | --- | --- | --- | |||||

postcondition | 0.02 | --- | --- | --- | |||||

VC for find_smaller | --- | --- | --- | --- | |||||

split_all_full | |||||||||

loop invariant init | 0.01 | --- | --- | --- | |||||

index in array bounds | 0.01 | --- | --- | --- | |||||

index in array bounds | 0.02 | --- | --- | --- | |||||

loop invariant preservation | 0.02 | --- | --- | --- | |||||

loop invariant preservation | 0.02 | --- | --- | --- | |||||

loop invariant preservation | 0.02 | --- | --- | --- | |||||

postcondition | 0.02 | --- | --- | --- | |||||

out of loop bounds | 0.01 | --- | --- | --- | |||||

other_descendant | --- | --- | --- | --- | |||||

induction_pr | |||||||||

other_descendant.0 | --- | --- | --- | 0.08 | |||||

other_descendant.1 | 0.01 | --- | --- | --- | |||||

other_descendant.2 | 0.01 | --- | --- | --- | |||||

inv_other_descendant | --- | --- | --- | --- | |||||

induction_pr | |||||||||

inv_other_descendant.0 | 0.01 | --- | --- | --- | |||||

inv_other_descendant.1 | --- | --- | --- | --- | |||||

split_vc | |||||||||

inv_other_descendant.1.0 | --- | --- | --- | --- | |||||

case (p1 = s1) | |||||||||

true case | --- | --- | --- | --- | |||||

right | |||||||||

right case | --- | --- | --- | --- | |||||

exists s | |||||||||

inv_other_descendant.1.0.0.0.0 | 0.01 | --- | --- | --- | |||||

false case | 0.02 | --- | --- | --- | |||||

inv_other_descendant.2 | --- | --- | --- | --- | |||||

split_vc | |||||||||

inv_other_descendant.2.0 | --- | --- | --- | --- | |||||

case (p1 = s1) | |||||||||

true case | --- | --- | --- | --- | |||||

right | |||||||||

right case | --- | --- | --- | --- | |||||

exists s | |||||||||

inv_other_descendant.2.0.0.0.0 | 0.01 | --- | --- | --- | |||||

false case | 0.02 | --- | --- | --- | |||||

StrictIncr.Transitive.Trans | 0.01 | --- | --- | --- | |||||

VC for traversal | --- | --- | --- | --- | |||||

split_vc | |||||||||

assertion | --- | --- | --- | --- | |||||

split_vc | |||||||||

assertion | 0.01 | --- | --- | --- | |||||

VC for traversal | 0.01 | --- | --- | --- | |||||

VC for traversal | 0.01 | --- | --- | --- | |||||

index in array bounds | 0.01 | --- | --- | --- | |||||

variant decrease | 0.01 | --- | --- | --- | |||||

precondition | 0.00 | --- | --- | --- | |||||

precondition | 0.01 | --- | --- | --- | |||||

precondition | 0.01 | --- | --- | --- | |||||

precondition | 0.02 | --- | --- | --- | |||||

precondition | --- | --- | --- | --- | |||||

split_vc | |||||||||

precondition | --- | --- | --- | --- | |||||

unfold parent in other_descendant | |||||||||

precondition | 0.02 | --- | --- | --- | |||||

precondition | --- | --- | --- | --- | |||||

unfold parent in other_descendant | |||||||||

precondition | --- | --- | --- | 0.14 | |||||

precondition | --- | --- | --- | --- | |||||

assert (descendant dirs x1 son) | |||||||||

asserted formula | 0.02 | --- | --- | --- | |||||

precondition | 0.04 | --- | --- | --- | |||||

precondition | --- | --- | --- | --- | |||||

case (x + 1 = e) | |||||||||

true case (precondition) | 0.01 | --- | --- | --- | |||||

false case (precondition) | --- | --- | --- | --- | |||||

assert (descendant dirs x (x+1)) | |||||||||

asserted formula | 0.02 | --- | --- | --- | |||||

false case (precondition) | 0.02 | --- | --- | --- | |||||

variant decrease | 0.01 | --- | --- | --- | |||||

precondition | 0.00 | --- | --- | --- | |||||

precondition | 0.01 | --- | --- | --- | |||||

precondition | 0.02 | --- | --- | --- | |||||

precondition | 0.02 | --- | --- | --- | |||||

precondition | --- | --- | --- | --- | |||||

split_vc | |||||||||

precondition | --- | --- | --- | --- | |||||

unfold parent in other_descendant | |||||||||

precondition | --- | --- | --- | 0.04 | |||||

precondition | --- | --- | --- | --- | |||||

unfold parent in other_descendant | |||||||||

precondition | 0.02 | --- | --- | --- | |||||

precondition | --- | --- | --- | --- | |||||

assert (descendant dirs x1 son) | |||||||||

asserted formula | 0.02 | --- | --- | --- | |||||

precondition | 0.05 | --- | --- | --- | |||||

precondition | --- | --- | --- | --- | |||||

case (s = x) | |||||||||

true case (precondition) | 0.01 | --- | --- | --- | |||||

false case (precondition) | --- | --- | --- | --- | |||||

assert (descendant dirs x s) | |||||||||

asserted formula | 0.02 | --- | --- | --- | |||||

false case (precondition) | --- | --- | --- | --- | |||||

split_all_full | |||||||||

false case (precondition) | 0.02 | --- | --- | --- | |||||

postcondition | --- | --- | --- | --- | |||||

destruct H | |||||||||

postcondition | 0.01 | --- | --- | --- | |||||

postcondition | 0.16 | --- | --- | --- | |||||

postcondition | --- | --- | --- | --- | |||||

destruct H | |||||||||

postcondition | --- | --- | --- | 0.08 | |||||

postcondition | --- | --- | 0.50 | --- | |||||

VC for in_order | --- | --- | --- | --- | |||||

split_vc | |||||||||

precondition | 0.01 | --- | --- | --- | |||||

precondition | 0.01 | --- | --- | --- | |||||

precondition | 0.02 | --- | --- | --- | |||||

precondition | 0.02 | --- | --- | --- | |||||

precondition | 0.02 | --- | --- | --- | |||||

precondition | --- | --- | --- | --- | |||||

split_vc | |||||||||

precondition | 0.02 | --- | --- | --- | |||||

precondition | 0.02 | --- | --- | --- | |||||

precondition | 0.04 | --- | --- | --- | |||||

precondition | 0.01 | --- | --- | --- | |||||

postcondition | 0.02 | --- | --- | --- | |||||

postcondition | 0.01 | --- | --- | --- |