Commit ab22e2ca authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update theories bintree and int.MinMax

parent b85a9fa4
......@@ -24,11 +24,12 @@ module BraunHeaps
type elt
predicate le elt elt
val predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le
(* [e] is no greater than the root of [t], if any *)
predicate le_root (e: elt) (t: tree elt) = match t with
let predicate le_root (e: elt) (t: tree elt) = match t with
| Empty -> true
| Node _ x _ -> le e x
end
......@@ -52,8 +53,8 @@ module BraunHeaps
= match t with
| Empty -> absurd
| Node l _ r ->
if l <> Empty then root_is_min l;
if r <> Empty then root_is_min r
if not is_empty l then root_is_min l;
if not is_empty r then root_is_min r
end
predicate inv (t: tree elt) = match t with
......@@ -68,16 +69,6 @@ module BraunHeaps
ensures { forall e. not (mem e result) }
= Empty
let is_empty (t: tree elt) : bool
ensures { result <-> size t = 0 }
=
t = Empty
let size (t: tree elt) : int
ensures { result = size t }
=
size t
let get_min (t: tree elt) : elt
requires { heap t && 0 < size t }
ensures { result = minimum t }
......
This diff is collapsed.
......@@ -5,6 +5,9 @@ theory Tree
type tree 'a = Empty | Node (tree 'a) 'a (tree 'a)
let function is_empty (t:tree 'a) : bool =
match t with Empty -> true | Node _ _ _ -> false end
end
theory Size "number of nodes"
......@@ -12,7 +15,7 @@ theory Size "number of nodes"
use import Tree
use import int.Int
function size (t: tree 'a) : int = match t with
let rec function size (t: tree 'a) : int = match t with
| Empty -> 0
| Node l _ r -> 1 + size l + size r
end
......@@ -47,7 +50,7 @@ theory Height "height of a tree"
use import int.Int
use import int.MinMax
function height (t: tree 'a) : int = match t with
let rec function height (t: tree 'a) : int = match t with
| Empty ->
0
| Node l _ r ->
......
......@@ -57,10 +57,21 @@ end
theory MinMax
use import Int
clone export relations.MinMax with type t = int, predicate le = (<=),
clone export relations.MinMax with
type t = int, predicate le = (<=),
goal TotalOrder.Refl, goal TotalOrder.Trans,
goal TotalOrder.Antisymm, goal TotalOrder.Total
let min (x y : int) : int
ensures { result = min x y }
= if x <= y then x else y
let max (x y : int) : int
ensures { result = max x y }
= if x <= y then y else x
end
(** {2 The Basic Well-Founded Order on Integers} *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment