new example: skew heaps

various stuff added to in_progress
parent 4b8b9981
theory Dyck
use export list.List
use export list.Append
type paren = L | R
type word = list paren
(* D -> eps | L D R D *)
inductive dyck word =
| Dyck_nil:
dyck Nil
| Dyck_ind:
forall w1 w2. dyck w1 -> dyck w2 -> dyck (Cons L (w1 ++ Cons R w2))
lemma dyck_concat:
forall w1 w2. dyck w1 -> dyck w2 -> dyck (w1 ++ w2)
(* the first letter, if any, must be L *)
lemma dyck_word_first:
forall w: word. dyck w ->
match w with Nil -> true | Cons c _ -> c = L end
lemma dyck_decomp:
forall w1 w2: word. dyck (w1 ++ w2) -> dyck w1 -> dyck w2
end
module Check
use import Dyck
use import list.Length
exception Failure
let rec is_dyck_rec (w: word) : word
ensures { exists p: word. dyck p && w = p ++ result &&
match result with Cons L _ -> false | _ -> true end }
raises { Failure -> forall p s: word. w = p ++ s -> not (dyck p) }
variant { length w }
=
match w with
| Cons L w ->
match is_dyck_rec w with
| Cons R w -> is_dyck_rec w
| _ -> raise Failure
end
| _ ->
w
end
let is_dyck (w: word) : bool
ensures { result <-> dyck w }
=
try is_dyck_rec w = Nil with Failure -> false end
end
......@@ -38,6 +38,7 @@ module Check
use import int.Int
use import Dyck
(* open n w = L^n w *)
function open (n: int) (w: word) : word
axiom open0: forall w: word. open 0 w = w
axiom openS: forall w: word, n: int. 0 < n ->
......
(** Warshall algorithm
Computes the transitive closure of a graph implemented as a Boolean
matrix. *)
module WarshallAlgorithm
use import int.Int
use import matrix.Matrix
(* path m i j k =
there is a path from i to j, using only vertices smaller than k *)
inductive path (matrix bool) int int int =
| Path_empty:
forall m: matrix bool, i j k: int.
get m (i,j) -> path m i j k
| Path_cons:
forall m: matrix bool, i x j k: int.
0 <= x < k -> path m i x k -> path m x j k -> path m i j k
lemma weakening:
forall m i j k1 k2. 0 <= k2 <= k1 ->
path m i j k1 -> path m i j k2
let transitive_closure (m: matrix bool) : matrix bool
requires { m.rows = m.columns }
ensures { let n = m.rows in
forall x y: int. 0 <= x < n -> 0 <= y < n ->
get result (x,y) <-> path m x y n }
=
let t = copy m in
let n = m.rows in
for k = 0 to n - 1 do
invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
get t (x,y) <-> path m x y k }
for i = 0 to n - 1 do
invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
get t (x,y) <->
(path m x y k || x < i && path m x y (k+1)) }
for j = 0 to n - 1 do
invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
get t (x,y) <->
(path m x y k || x < i && path m x y (k+1)
|| x = i && y < j && path m x y (k+1)) }
set t (i,j) (get t (i,j) || get t (i,k) && get t (k,j))
done
done
done;
t
end
module SkewHeaps
use import bintree.Tree
use import bintree.Size
type elt
predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le
predicate eq (x y: elt) = le x y && le y x
clone import bintree.Occ with type elt = elt, predicate eq = eq
(* [e] is no greater than the root of [t], if any *)
predicate le_root (e: elt) (t: tree elt) = match t with
| Empty -> true
| Node _ x _ -> le e x
end
(* [t] is a heap *)
predicate heap (t: tree elt) = match t with
| Empty -> true
| Node l x r -> le_root x l && heap l && le_root x r && heap r
end
predicate is_minimum (x: elt) (t: tree elt) =
mem x t && forall e. mem e t -> le x e
(* the root is the smallest element *)
let rec lemma root_is_min (l: tree elt) (x: elt) (r: tree elt) : unit
requires { heap (Node l x r) } variant { size (Node l x r) }
ensures { is_minimum x (Node l x r) }
=
match l with Empty -> () | Node ll lx lr -> root_is_min ll lx lr end;
match r with Empty -> () | Node rl rx rr -> root_is_min rl rx rr end;
()
let get_min (t: tree elt) : elt
requires { heap t && t <> Empty }
ensures { is_minimum result t }
=
match t with
| Empty -> absurd
| Node _ x _ -> x
end
let rec merge (t1 t2: tree elt) : tree elt
requires { heap t1 && heap t2 }
ensures { heap result }
ensures { forall e. occ e result = occ e t1 + occ e t2 }
variant { size t1 + size t2 }
=
match t1, t2 with
| Empty, _ -> t2
| _, Empty -> t1
| Node l1 x1 r1, Node l2 x2 r2 ->
if le x1 x2 then
Node (merge r1 t2) x1 l1
else
Node (merge r2 t1) x2 l2
end
let add (x: elt) (t: tree elt) : tree elt
requires { heap t }
ensures { heap result }
ensures { occ x result = occ x t + 1 }
ensures { forall e. not (eq e x) -> occ e result = occ e t }
=
merge (Node Empty x Empty) t
let remove_minimum (t: tree elt) : tree elt
requires { heap t && t <> Empty }
ensures { heap result }
ensures { forall e. if is_minimum e t then occ e result = occ e t - 1
else occ e result = occ e t }
=
match t with
| Empty -> absurd
| Node l _ r -> merge l r
end
end
This diff is collapsed.
......@@ -21,6 +21,28 @@ theory Size "number of nodes"
end
theory Occ "occurrences in a binary tree"
use export Tree
use export int.Int
type elt
predicate eq elt elt
function occ (x: elt) (t: tree elt) : int = match t with
| Empty -> 0
| Node l y r -> (if eq y x then 1 else 0) + occ x l + occ x r
end
lemma occ_nonneg:
forall x: elt, t: tree elt. 0 <= occ x t
predicate mem (x: elt) (t: tree elt) =
0 < occ x t
end
theory Inorder "inorder traversal"
use export Tree
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover
id="0"
name="Alt-Ergo"
version="0.95.2"/>
<file
name="../bintree.why"
verified="true"
expanded="false">
<theory
name="Tree"
locfile="../bintree.why"
loclnum="4" loccnumb="7" loccnume="11"
verified="true"
expanded="false">
</theory>
<theory
name="Size"
locfile="../bintree.why"
loclnum="10" loccnumb="7" loccnume="11"
verified="true"
expanded="false">
<label
name="number of nodes"/>
<goal
name="size_nonneg"
locfile="../bintree.why"
loclnum="20" loccnumb="8" loccnume="19"
sum="cb8c289d9686ccc4e3509e0890619661"
proved="true"
expanded="false"
shape="ainfix &lt;=c0asizeV0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="false">
<goal
name="size_nonneg.1"
locfile="../bintree.why"
loclnum="20" loccnumb="8" loccnume="19"
expl="1."
sum="12d53d1b4d232aed7f7f83d7cb5e3f42"
proved="true"
expanded="false"
shape="Cainfix &lt;=c0asizeV0aEmptyainfix &lt;=c0asizeV0Iainfix &lt;=c0asizeV1Iainfix &lt;=c0asizeV3aNodeVVVV0F">
<proof
prover="0"
timelimit="6"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
</theory>
<theory
name="Occ"
locfile="../bintree.why"
loclnum="24" loccnumb="7" loccnume="10"
verified="true"
expanded="false">
<label
name="occurrences in a binary tree"/>
<goal
name="occ_nonneg"
locfile="../bintree.why"
loclnum="38" loccnumb="8" loccnume="18"
sum="f2106ad0f6afef73c8d8659379f4e159"
proved="true"
expanded="false"
shape="ainfix &lt;=c0aoccV0V1F">
<transf
name="induction_ty_lex"
proved="true"
expanded="false">
<goal
name="occ_nonneg.1"
locfile="../bintree.why"
loclnum="38" loccnumb="8" loccnume="18"
expl="1."
sum="6ad4875c535741780c16685271aaf9e3"
proved="true"
expanded="false"
shape="Cainfix &lt;=c0aoccV0V1aEmptyainfix &lt;=c0aoccV0V1Iainfix &lt;=c0aoccV0V2Iainfix &lt;=c0aoccV0V4aNodeVVVV1F">
<proof
prover="0"
timelimit="6"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
</theory>
<theory
name="Inorder"
locfile="../bintree.why"
loclnum="46" loccnumb="7" loccnume="14"
verified="true"
expanded="false">
<label
name="inorder traversal"/>
</theory>
<theory
name="Preorder"
locfile="../bintree.why"
loclnum="58" loccnumb="7" loccnume="15"
verified="true"
expanded="false">
<label
name="preorder traversal"/>
</theory>
<theory
name="InorderLength"
locfile="../bintree.why"
loclnum="70" loccnumb="7" loccnume="20"
verified="true"
expanded="false">
<goal
name="inorder_length"
locfile="../bintree.why"
loclnum="76" loccnumb="8" loccnume="22"
sum="35f8a02ac76b338b12bc12823565d6c2"
proved="true"
expanded="false"
shape="ainfix =alengthainorderV0asizeV0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="false">
<goal
name="inorder_length.1"
locfile="../bintree.why"
loclnum="76" loccnumb="8" loccnume="22"
expl="1."
sum="a14cd8e33cdb1250c6764bf6b3d4c8b8"
proved="true"
expanded="false"
shape="Cainfix =alengthainorderV0asizeV0aEmptyainfix =alengthainorderV0asizeV0Iainfix =alengthainorderV1asizeV1Iainfix =alengthainorderV3asizeV3aNodeVVVV0F">
<proof
prover="0"
timelimit="6"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
</theory>
<theory
name="Zipper"
locfile="../bintree.why"
loclnum="80" loccnumb="7" loccnume="13"
verified="true"
expanded="false">
<label
name="Huet&apos;s zipper"/>
</theory>
</file>
</why3session>
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