VerifyThis 2021: DLL to BST

solution to VerifyThis 2021 challenge 2

Topics: List Data Structure / Trees

Tools: Why3

References: VerifyThis @ ETAPS 2021

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

VerifyThis @ ETAPS 2021 competition Challenge 2: DLL to BST

See https://www.pm.inf.ethz.ch/research/verifythis.html

Authors: - Jean-Christophe FilliĆ¢tre (CNRS) - Andrei Paskevich (Univ. Paris-Saclay)

Summary:

- all tasks verified

- balanced tree: we show 2^(h-1) <= size(t) < 2^h where h is the height of the returned tree t, which implies h = O(log(size(t)))

- There are pointer-based data structures in Why3, so we devised a customed memory model for this problem (see type `loc` and maps `prev` and `next` below).

- The only precondition of `dll_to_bst`, namely

requires { dll prev next s head 0 (length s) }

states that, in the initial memory state, head points to a well-formed doubly-linked list, whose contents (locations of list cells) is represented by (injective) sequence s.

- The fact that the tree is a BST follows from the postcondition of `dll_to_bst`

ensures { inorder s t == s }

that states that the nodes of t, taken in order, are exactly the cells of the input list.

```use int.Int
use int.ComputerDivision
use fmap.Fmap
use seq.Seq
use bintree.Tree
use bintree.Size

type loc

val eq (x y: loc) : bool ensures { result <-> x = y }

clone fmap.MapImp as I with type key = loc, val eq = eq

let ([]) = I.find
let ([]<-) (l: loc) (m: I.t 'a) (v: 'a) : unit
requires { I.mem l m }
ensures  { m = add l v (old m) }
= I.add l v m

val constant null: loc

val data: I.t int
val prev: I.t loc
val next: I.t loc

predicate valid (prev next: fmap loc loc) (s: seq loc)
= forall i . 0 <= i < length s ->
s[i] <> null /\ mem s[i] prev /\ mem s[i] next /\
forall j . i < j < length s -> s[i] <> s[j]

predicate dll (prev next: fmap loc loc) (s: seq loc) (head: loc) (lo hi: int)
= valid prev next s /\
0 <= lo <= hi <= length s /\
(head = if lo = length s then null else s[lo]) /\
(forall i . lo <= i < hi - 1 -> next s[i] = s[i+1]) /\
(forall i . lo <  i < hi     -> prev s[i] = s[i-1]) /\
(lo < hi -> next s[hi - 1] = if hi = length s then null else s[hi]) /\
(lo < hi -> prev s[lo] = if lo = 0 then null else s[lo-1])

predicate tree (prev next: fmap loc loc) (s: seq loc) (root: loc) (t: tree int) (lo hi: int)
= valid prev next s /\
0 <= lo <= hi <= length s /\
match t with
| Empty ->
root = null /\ lo = hi
| Node l p r ->
lo <= p < hi /\ root = s[p] /\
tree prev next s (prev root) l lo p /\
tree prev next s (next root) r (p + 1) hi
end

let rec lemma tree_frame (prev next prev' next': fmap loc loc) (s: seq loc) (root: loc) (t: tree int) (lo hi: int)
requires { tree prev next s root t lo hi }
requires { valid prev' next' s }
requires { forall i. lo <= i < hi -> prev' s[i] = prev s[i] /\ next' s[i] = next s[i] }
ensures  { tree prev' next' s root t lo hi }
variant  { t }
= match t with
| Empty -> ()
| Node l p r ->
tree_frame prev next prev' next' s (prev.contents root) l lo p;
tree_frame prev next prev' next' s (next.contents root) r (p + 1) hi
end

use bintree.Height
use int.Power

let rec dll_to_bst_rec (ghost s: seq loc)
(head: loc) (ghost ihead: int) (n: int)
: (root: loc, right: loc, ghost t: tree int)
requires { dll prev next s head ihead (ihead + n) }
ensures  { right = if ihead + n = length s then null else s[ihead + n] }
ensures  { tree prev next s root t ihead (ihead + n) }
ensures  { Fmap.S.(domain prev == old (domain prev)) }
ensures  { Fmap.S.(domain next == old (domain next)) }
ensures  { forall i. 0 <= i < ihead -> prev s[i] = old prev s[i] }
ensures  { forall i. ihead + n <= i < length s -> prev s[i] = old prev s[i] }
ensures  { forall i. 0 <= i < ihead -> next s[i] = old next s[i] }
ensures  { forall i. ihead + n <= i < length s -> next s[i] = old next s[i] }
ensures  { n > 0 -> let h = height t in power 2 (h - 1) <= n < power 2 h }
variant  { n }
= if n = 0 then return null, head, Empty;
let nl = div n 2 in
let left, root, l = dll_to_bst_rec s head ihead nl in
root[prev] <- left;
let temp, right, r = dll_to_bst_rec s root[next] (ihead + nl + 1) (n - nl - 1) in
root[next] <- temp;
root, right, Node l (ihead + nl) r

let rec lemma tree_size (prev next: fmap loc loc) (s: seq loc) (root: loc) (t: tree int) (lo hi: int)
requires { tree prev next s root t lo hi }
ensures  { size t = hi - lo }
variant  { t }
= match t with
| Empty -> ()
| Node l p r ->
tree_size prev next s (prev.contents root) l lo p;
tree_size prev next s (next.contents root) r (p + 1) hi
end

function inorder (s: seq loc) (t: tree int) : seq loc
= match t with
| Empty      -> empty
| Node l p r -> inorder s l ++ cons s[p] (inorder s r)
end

let rec lemma tree_inorder (prev next: fmap loc loc) (s: seq loc) (root: loc) (t: tree int) (lo hi: int)
requires { tree prev next s root t lo hi }
ensures  { inorder s t == s[lo..hi] }
variant  { t }
= match t with
| Empty -> ()
| Node l p r ->
tree_inorder prev next s (prev.contents root) l lo p;
tree_inorder prev next s (next.contents root) r (p + 1) hi
end

(* recursive `size` *)

let rec size (ghost s: seq loc) (head: loc) (ghost ihead: int): int
requires { dll prev next s head ihead (length s) }
ensures  { result = length s - ihead }
variant  { length s - ihead }
= if eq head null then 0 else 1 + size s head[next] (ihead + 1)

let dll_to_bst (ghost s: seq loc) (head: loc) : (root: loc, ghost t: tree int)
requires { dll prev next s head 0 (length s) }
ensures  { tree prev next s root t 0 (length s) }
ensures  { size t = length s }
ensures  { inorder s t == s }
ensures  { length s > 0 -> let h = height t in
power 2 (h - 1) <= length s < power 2 h }
= let n = size s head 0 in
let root, _, t = dll_to_bst_rec s head 0 n in
root, t

(* iterative `size` *)

let size_alt (ghost s: seq loc) (head: loc) : int
requires { dll prev next s head 0 (length s) }
ensures  { result = length s }
= let ref p = head in
let ref len = 0 in
while not (eq p null) do
invariant { dll prev next s p len (length s) }
variant   { length s - len }
p <- p[next];
len <- len + 1
done;
len

let dll_to_bst_alt (ghost s: seq loc) (head: loc) : (root: loc, ghost t: tree int)
requires { dll prev next s head 0 (length s) }
ensures  { tree prev next s root t 0 (length s) }
ensures  { size t = length s }
ensures  { inorder s t == s }
ensures  { length s > 0 -> let h = height t in
power 2 (h - 1) <= length s < power 2 h }
= let n = size_alt s head in
let root, _, t = dll_to_bst_rec s head 0 n in
root, t
```

download ZIP archive

Why3 Proof Results for Project "verifythis_2021_dll_to_bst"

Theory "verifythis_2021_dll_to_bst.Top": fully verified

 Obligations Alt-Ergo 2.0.0 Alt-Ergo 2.3.3 Alt-Ergo 2.4.0 CVC3 2.4.1 CVC4 1.7 CVC4 1.8 Z3 3.2 Z3 4.8.10 VC for eq'refn --- --- --- --- --- 0.05 --- --- VC for mixfix []<- --- --- --- --- --- 0.06 --- --- VC for tree_frame --- --- --- --- --- --- --- --- split_vc variant decrease --- --- --- --- --- 0.10 --- --- precondition --- --- --- --- --- 0.12 --- --- precondition --- --- --- --- --- 0.06 --- --- precondition --- --- --- --- --- 0.19 --- --- variant decrease --- --- --- --- --- 0.10 --- --- precondition --- --- --- --- --- 0.11 --- --- precondition --- --- --- --- --- 0.06 --- --- precondition --- --- --- --- --- 0.17 --- --- postcondition --- --- --- --- --- --- --- --- unfold tree VC for tree_frame --- --- --- --- --- --- --- --- split_vc VC for tree_frame --- --- --- --- --- 0.06 --- --- VC for tree_frame --- 0.02 --- --- --- --- --- --- VC for tree_frame --- 0.02 --- --- --- --- --- --- VC for tree_frame --- 0.02 --- --- --- --- --- --- VC for tree_frame --- 0.02 --- --- --- --- --- --- VC for tree_frame --- 0.02 --- --- --- --- --- --- VC for tree_frame --- --- --- --- --- 0.13 --- --- VC for tree_frame --- --- --- --- --- 0.11 --- --- VC for tree_frame --- --- --- --- --- 0.14 --- --- VC for tree_frame --- --- --- --- --- 0.12 --- --- VC for tree_frame --- --- --- --- --- 0.13 --- --- VC for dll_to_bst_rec --- --- --- --- --- --- --- --- split_vc postcondition --- --- --- --- --- 0.07 --- --- postcondition --- 0.02 --- --- --- --- --- --- postcondition --- --- --- --- --- 0.11 --- --- postcondition --- --- --- --- --- 0.10 --- --- postcondition --- --- --- --- --- 0.07 --- --- postcondition --- --- --- --- --- 0.06 --- --- postcondition --- --- --- --- --- 0.07 --- --- postcondition --- --- --- --- --- 0.05 --- --- postcondition --- --- --- --- --- 0.08 --- --- precondition --- --- --- --- --- 0.06 --- --- variant decrease --- --- --- --- --- 0.10 --- --- precondition --- --- --- --- --- 0.12 --- --- precondition --- --- --- --- --- 0.18 --- --- precondition --- --- --- --- --- 0.22 --- --- variant decrease --- --- --- --- --- 0.11 --- --- precondition --- --- --- --- --- --- --- --- unfold dll VC for dll_to_bst_rec --- --- --- --- --- --- --- --- split_vc VC for dll_to_bst_rec 3.22 --- --- --- --- --- --- --- remove zero,one,(-),(>),(<=),(>=),abs,min,max,get1,set1,([]'),([<-]''),(==''),subset,is_empty2,singleton1,disjoint,is_empty1,([<-]'),singleton,cons,snoc,(++),is_empty,size,height,dll,next'unused'unused1,prev'unused'unused1,(=)'result'unused'unused,nl,div'result'unused'unused,next'unused'unused,prev'unused'unused,dll_to_bst_rec'result'unused'unused,m'unused'unused,([])'result'unused'unused,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,Abs_le,Abs_pos,Min_r,Max_l,Min_comm,Max_comm,Min_assoc,Max_assoc,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,Power_0,Power_s,Power_s_alt,Power_1,Power_sum,Power_mult,Power_comm1,Power_comm2,Power_non_neg,Power_pos,Power_monotonic,extensionality1,subset_refl,subset_trans,is_empty_empty1,empty_is_empty,mem_singleton,remove_def,add_remove,remove_add,subset_remove,union_def,subset_union_1,subset_union_2,inter_def,subset_inter_1,subset_inter_2,diff_def,subset_diff,pick_def,disjoint_inter_empty,disjoint_diff_eq,disjoint_diff_s2,filter_def,subset_filter,map_def,mem_map,cardinal_nonneg,cardinal_empty,cardinal_add,cardinal_remove,cardinal_subset,subset_eq,cardinal1,cardinal_union,cardinal_inter_disjoint,cardinal_diff,cardinal_filter,cardinal_map,mk_domain,mk_contents,is_empty_empty,add_contents_k,add_contents_other,find_def,remove_contents,remove_domain,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,is_empty'spec,size_nonneg,size_empty,height_nonneg,tree_frame,Requires,H,Ensures9,Ensures8,Ensures7,Ensures6,Ensures5,Ensures4,Ensures,Ensures3,Ensures2 VC for dll_to_bst_rec 0.56 --- --- --- --- --- --- 0.16 VC for dll_to_bst_rec --- --- --- --- --- 0.10 --- --- VC for dll_to_bst_rec --- --- --- --- --- 0.15 --- --- VC for dll_to_bst_rec --- --- --- --- --- 0.12 --- --- VC for dll_to_bst_rec --- 0.15 --- --- --- --- --- --- VC for dll_to_bst_rec --- --- --- --- --- 0.16 --- --- VC for dll_to_bst_rec --- --- --- --- --- 1.00 --- --- VC for dll_to_bst_rec --- --- --- --- --- 0.14 --- --- VC for dll_to_bst_rec --- --- --- --- --- 0.84 --- --- precondition --- --- --- --- --- 0.41 --- --- postcondition --- --- --- --- --- 0.08 --- --- postcondition --- --- --- --- --- --- --- --- unfold tree VC for dll_to_bst_rec --- --- --- --- --- --- --- --- split_vc VC for dll_to_bst_rec 3.00 --- --- --- --- --- --- --- remove zero,one,(-),(>),(<=),(>=),abs,min,max,get1,set1,([]'),([<-]''),(==''),subset,is_empty2,singleton1,disjoint,(=='),mapsto,is_empty1,([<-]'),size1,([]),singleton,cons,snoc,(++),is_empty,size,height,dll,next'unused'unused2,prev'unused'unused2,(=)'result'unused'unused,nl,div'result'unused'unused,next'unused'unused1,prev'unused'unused1,dll_to_bst_rec'result'unused'unused1,m'unused'unused1,([])'result'unused'unused,next'unused'unused,prev'unused'unused,dll_to_bst_rec'result'unused'unused,m'unused'unused,result'unused,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,Abs_le,Abs_pos,Min_r,Max_l,Min_comm,Max_comm,Min_assoc,Max_assoc,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,Power_0,Power_s,Power_s_alt,Power_1,Power_sum,Power_mult,Power_comm1,Power_comm2,Power_non_neg,Power_pos,Power_monotonic,extensionality1,subset_refl,subset_trans,is_empty_empty1,empty_is_empty,mem_singleton,remove_def,add_remove,remove_add,subset_remove,union_def,subset_union_1,subset_union_2,inter_def,subset_inter_1,subset_inter_2,diff_def,subset_diff,pick_def,disjoint_inter_empty,disjoint_diff_eq,disjoint_diff_s2,filter_def,subset_filter,map_def,mem_map,cardinal_nonneg,cardinal_empty,cardinal_add,cardinal_remove,cardinal_subset,subset_eq,cardinal1,cardinal_union,cardinal_inter_disjoint,cardinal_diff,cardinal_filter,cardinal_map,extensionality,mk_domain,mk_contents,is_empty_empty,add_contents_k,add_contents_other,find_def,remove_contents,remove_domain,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,is_empty'spec,size_nonneg,size_empty,height_nonneg,tree_frame,Requires,H,Ensures20,Ensures19,Ensures18,Ensures17,Ensures16,Ensures15,Ensures12,Ensures11,Ensures9,Ensures8,Ensures7,Ensures6,Ensures5,Ensures4,Ensures,Ensures14,Ensures13,Ensures3,Ensures2 VC for dll_to_bst_rec 0.66 --- --- --- --- --- --- --- VC for dll_to_bst_rec --- --- --- --- --- 0.13 --- --- VC for dll_to_bst_rec --- --- --- --- --- 0.13 --- --- VC for dll_to_bst_rec --- --- --- --- --- 0.14 --- --- VC for dll_to_bst_rec --- --- --- --- --- 0.12 --- --- VC for dll_to_bst_rec --- --- --- --- --- 0.13 --- --- VC for dll_to_bst_rec --- --- --- --- --- 0.19 --- --- VC for dll_to_bst_rec --- --- --- --- --- --- --- --- apply tree_frame with prev2.to_fmap,next2.to_fmap apply premises --- 0.06 --- --- --- 0.15 --- --- apply premises 2.97 --- --- --- --- --- --- --- remove zero,one,(-),(>),(<=),(>=),abs,min,max,get1,set1,([]'),([<-]''),(==''),subset,is_empty2,singleton1,disjoint,(=='),mapsto,is_empty1,([<-]'),size1,([]),singleton,cons,snoc,(++),is_empty,size,height,dll,next'unused'unused2,prev'unused'unused2,(=)'result'unused'unused,nl,div'result'unused'unused,next'unused'unused1,prev'unused'unused1,dll_to_bst_rec'result'unused'unused1,m'unused'unused1,([])'result'unused'unused,next'unused'unused,prev'unused'unused,dll_to_bst_rec'result'unused'unused,m'unused'unused,result'unused,p,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,Abs_le,Abs_pos,Min_r,Max_l,Min_comm,Max_comm,Min_assoc,Max_assoc,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,Power_0,Power_s,Power_s_alt,Power_1,Power_sum,Power_mult,Power_comm1,Power_comm2,Power_non_neg,Power_pos,Power_monotonic,extensionality1,subset_refl,subset_trans,is_empty_empty1,empty_is_empty,mem_singleton,remove_def,add_remove,remove_add,subset_remove,union_def,subset_union_1,subset_union_2,inter_def,subset_inter_1,subset_inter_2,diff_def,subset_diff,pick_def,disjoint_inter_empty,disjoint_diff_eq,disjoint_diff_s2,filter_def,subset_filter,map_def,mem_map,cardinal_nonneg,cardinal_empty,cardinal_add,cardinal_remove,cardinal_subset,subset_eq,cardinal1,cardinal_union,cardinal_inter_disjoint,cardinal_diff,cardinal_filter,cardinal_map,extensionality,mk_domain,mk_contents,is_empty_empty,add_contents_k,add_contents_other,find_def,remove_contents,remove_domain,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,is_empty'spec,size_nonneg,size_empty,height_nonneg,tree_frame,Requires,H,Ensures20,Ensures19,Ensures18,Ensures17,Ensures16,Ensures15,Ensures12,Ensures11,Ensures9,Ensures8,Ensures7,Ensures6,Ensures5,Ensures4,Ensures,Ensures14,Ensures13,Ensures3,Ensures2 apply premises 0.62 --- --- --- --- --- --- 0.27 apply premises --- --- --- 2.59 --- --- --- --- remove zero,one,(-),(>),(<=),(>=),abs,min,max,get1,set1,([<-]''),(==''),subset,is_empty2,singleton1,disjoint,(=='),mem,mapsto,is_empty1,([<-]'),size1,([]),singleton,cons,snoc,(++),is_empty,size,height,dll,next'unused'unused2,prev'unused'unused2,(=)'result'unused'unused,nl,div'result'unused'unused,next'unused'unused1,prev'unused'unused1,dll_to_bst_rec'result'unused'unused1,m'unused'unused1,([])'result'unused'unused,next'unused'unused,prev'unused'unused,dll_to_bst_rec'result'unused'unused,m'unused'unused,result'unused,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,Abs_le,Abs_pos,Min_r,Max_l,Min_comm,Max_comm,Min_assoc,Max_assoc,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,Power_0,Power_s,Power_s_alt,Power_1,Power_sum,Power_mult,Power_comm1,Power_comm2,Power_non_neg,Power_pos,Power_monotonic,extensionality1,subset_refl,subset_trans,is_empty_empty1,empty_is_empty,add_def,mem_singleton,remove_def,add_remove,remove_add,subset_remove,union_def,subset_union_1,subset_union_2,inter_def,subset_inter_1,subset_inter_2,diff_def,subset_diff,pick_def,disjoint_inter_empty,disjoint_diff_eq,disjoint_diff_s2,filter_def,subset_filter,map_def,mem_map,cardinal_nonneg,cardinal_empty,cardinal_add,cardinal_remove,cardinal_subset,subset_eq,cardinal1,cardinal_union,cardinal_inter_disjoint,cardinal_diff,cardinal_filter,cardinal_map,extensionality,mem_mapsto,mk_domain,mk_contents,is_empty_empty,add_contents_k,add_domain,find_def,remove_contents,remove_domain,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,is_empty'spec,size_nonneg,size_empty,height_nonneg,tree_frame,Requires,H,Ensures20,Ensures19,Ensures18,Ensures17,Ensures16,Ensures15,Ensures11,Ensures9,Ensures8,Ensures6,Ensures4,Ensures,Ensures14,Ensures13,Ensures3,Ensures2 apply premises --- --- --- 0.03 --- --- --- 0.02 VC for dll_to_bst_rec --- --- --- --- --- --- --- --- apply tree_frame with prev.to_fmap,next1.to_fmap apply premises --- 0.03 --- --- --- 0.10 --- 0.04 apply premises 2.96 --- --- --- --- --- --- --- remove zero,one,(-),(>),(<=),(>=),abs,min,max,get1,set1,([]'),([<-]''),(==''),subset,is_empty2,singleton1,disjoint,(=='),mapsto,is_empty1,([<-]'),size1,([]),singleton,cons,snoc,height,dll,next'unused'unused2,prev'unused'unused2,(=)'result'unused'unused,nl,div'result'unused'unused,next'unused'unused1,prev'unused'unused1,dll_to_bst_rec'result'unused'unused1,m'unused'unused1,([])'result'unused'unused,next'unused'unused,prev'unused'unused,dll_to_bst_rec'result'unused'unused,m'unused'unused,result'unused,p,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,Abs_le,Abs_pos,Min_r,Max_l,Min_comm,Max_comm,Min_assoc,Max_assoc,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,Power_0,Power_s,Power_s_alt,Power_1,Power_sum,Power_mult,Power_comm1,Power_comm2,Power_non_neg,Power_pos,Power_monotonic,extensionality1,subset_refl,subset_trans,is_empty_empty1,empty_is_empty,mem_singleton,remove_def,add_remove,remove_add,subset_remove,union_def,subset_union_1,subset_union_2,inter_def,subset_inter_1,subset_inter_2,diff_def,subset_diff,pick_def,disjoint_inter_empty,disjoint_diff_eq,disjoint_diff_s2,filter_def,subset_filter,map_def,mem_map,cardinal_nonneg,cardinal_empty,cardinal_add,cardinal_remove,cardinal_subset,subset_eq,cardinal1,cardinal_union,cardinal_inter_disjoint,cardinal_diff,cardinal_filter,cardinal_map,extensionality,mk_domain,mk_contents,is_empty_empty,add_contents_k,add_contents_other,find_def,remove_contents,remove_domain,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'def,height_nonneg,tree_frame,Requires,H,Ensures20,Ensures19,Ensures18,Ensures17,Ensures16,Ensures15,Ensures12,Ensures9,Ensures8,Ensures7,Ensures6,Ensures5,Ensures4,Ensures,Ensures14,Ensures13,Ensures3,Ensures2 apply premises 0.71 --- 0.04 --- --- --- --- --- apply premises --- --- --- --- --- --- --- 0.06 postcondition --- --- --- --- --- 0.46 --- --- postcondition --- --- --- --- --- 0.36 --- --- postcondition --- --- --- --- --- 1.13 --- --- postcondition --- --- --- --- --- 1.10 --- --- postcondition --- --- --- --- --- --- --- 0.06 postcondition --- --- --- 0.82 --- --- 1.84 --- remove zero,one,(-),(>),(<=),(>=),abs,min,max,get1,set1,([<-]''),(==''),subset,is_empty2,singleton1,disjoint,(=='),mem,mapsto,is_empty1,([<-]'),size1,([]),singleton,cons,snoc,(++),is_empty,size,height,dll,next'unused'unused2,prev'unused'unused2,(=)'result'unused'unused,nl,div'result'unused'unused,next'unused'unused1,prev'unused'unused1,dll_to_bst_rec'result'unused'unused1,m'unused'unused1,([])'result'unused'unused,next'unused'unused,prev'unused'unused,dll_to_bst_rec'result'unused'unused,m'unused'unused,result'unused,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,Abs_le,Abs_pos,Min_r,Max_l,Min_comm,Max_comm,Min_assoc,Max_assoc,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,Power_0,Power_s,Power_s_alt,Power_1,Power_sum,Power_mult,Power_comm1,Power_comm2,Power_non_neg,Power_pos,Power_monotonic,subset_refl,subset_trans,is_empty_empty1,empty_is_empty,add_def,mem_singleton,remove_def,add_remove,remove_add,subset_remove,union_def,subset_union_1,subset_union_2,inter_def,subset_inter_1,subset_inter_2,diff_def,subset_diff,pick_def,disjoint_inter_empty,disjoint_diff_eq,disjoint_diff_s2,filter_def,subset_filter,map_def,mem_map,cardinal_nonneg,cardinal_empty,cardinal_add,cardinal_remove,cardinal_subset,subset_eq,cardinal1,cardinal_union,cardinal_inter_disjoint,cardinal_diff,cardinal_filter,cardinal_map,extensionality,mem_mapsto,mk_domain,mk_contents,is_empty_empty,add_contents_k,add_domain,find_def,remove_contents,remove_domain,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,is_empty'spec,size_nonneg,size_empty,height_nonneg,tree_frame,Requires,H2,Ensures25,Ensures24,Ensures23,Ensures22,Ensures21,Ensures20,Ensures18,Ensures17,Ensures16,Ensures14,Ensures13,Ensures12,Ensures11,Ensures10,Ensures8,Ensures6,Ensures4,Ensures3,Ensures2,Ensures1,Ensures postcondition --- --- --- 0.04 0.06 --- --- --- postcondition --- --- --- --- --- 0.60 --- --- VC for tree_size --- --- --- --- --- 0.10 --- --- VC for tree_inorder --- 0.19 --- --- --- --- --- --- VC for size --- --- --- --- --- 0.26 --- --- VC for dll_to_bst --- --- --- --- --- 0.17 --- --- split_vc precondition --- --- --- --- --- 0.08 --- --- precondition --- --- --- --- --- 0.07 --- --- postcondition --- --- --- --- --- 0.07 --- --- postcondition --- --- --- --- --- 0.12 --- --- postcondition --- 0.14 --- --- --- --- --- --- postcondition --- --- --- --- --- 0.08 --- --- VC for size_alt --- --- --- --- --- 0.26 --- --- VC for dll_to_bst_alt --- --- --- --- --- 0.17 --- --- split_vc precondition --- --- --- --- --- 0.08 --- --- precondition --- --- --- --- --- 0.09 --- --- postcondition --- --- --- --- --- 0.08 --- --- postcondition --- --- --- --- --- 0.14 --- --- postcondition --- 0.13 --- --- --- --- --- --- postcondition --- --- --- --- --- 0.08 --- ---