Wiki Agenda Contact Version française

VerifyThis 2021: DLL to BST

solution to VerifyThis 2021 challenge 2


Authors: Jean-Christophe Filliâtre / Andrei Paskevich

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

ObligationsAlt-Ergo 2.0.0Alt-Ergo 2.3.3Alt-Ergo 2.4.0CVC3 2.4.1CVC4 1.7CVC4 1.8Z3 3.2Z3 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_rec3.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_rec0.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_rec3.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_rec0.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 premises2.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 premises0.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 premises2.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 premises0.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.040.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------