new examples (in progress)

parent 0b8f8dad
(* Depth-First Search
(following François Pottier's lecture INF431 at École Polytechnique)
We are given memory cells with two (possibly null) [left] and [right]
neighbours and a mutable Boolean attribute [marked]. In Java, it would
look like
class Cell { Cell left, right; boolean marked; ... }
We mark all cells that are reachable from a given cell [root] using
depth-first search, that is using the following recursive function:
static void dfs(Cell c) {
if (c != null && !c.marked) {
c.marked = true;
dfs(c.left);
dfs(c.right);
}
}
We wish to prove that, assuming that all cells are initially unmarked,
a call to dfs(root) will mark all cells reachable from root, and only
those cells.
*)
module DFS
use import bool.Bool
use import map.Map
use import ref.Ref
type loc
constant null: loc
constant root: loc
function left loc: loc
function right loc: loc
type marks = map loc bool
val marked: ref marks
val ghost busy: ref marks
predicate edge (x y: loc) = x <> null && (left x = y || right x = y)
inductive path (x y: loc) =
| path_nil: forall x: loc. path x x
| path_cons: forall x y z: loc. path x y -> edge y z -> path x z
predicate only_descendants_are_marked (marked: marks) =
forall x: loc. x <> null && marked[x] = True -> path root x
predicate well_colored (marked busy: marks) =
forall x y: loc. edge x y -> y <> null ->
busy[x] = True || (marked[x] = True -> marked[y] = True)
let rec dfs (c: loc) : unit
requires { well_colored !marked !busy }
requires { only_descendants_are_marked !marked }
requires { path root c }
ensures { well_colored !marked !busy }
ensures { forall x: loc. (old !marked)[x] = True -> !marked[x] = True }
ensures { c <> null -> !marked[c] = True }
ensures { forall x: loc. !busy[x] = True -> (old !busy)[x] = True }
ensures { only_descendants_are_marked !marked }
=
if c <> null && not !marked[c] then begin
ghost busy := !busy[c <- True];
marked := !marked[c <- True];
dfs (left c);
dfs (right c);
busy := !busy[c <- False]
end
predicate all_descendants_are_marked (marked: marks) =
root <> null ->
marked[root] = True &&
forall x y: loc. edge x y -> marked[x] = True -> marked[y] = True
lemma reformulation:
forall marked: marks.
all_descendants_are_marked marked ->
forall x: loc. x <> null -> path root x -> marked[x] = True
let traverse () : unit
requires { forall x: loc. x <> null ->
!marked[x] = False && !busy[x] = False }
ensures { only_descendants_are_marked !marked }
ensures { all_descendants_are_marked !marked }
ensures { forall x: loc. x <> null -> !busy[x] = False }
=
(* assert { well_colored !marked !busy }; *)
dfs root
end
\ No newline at end of file
This diff is collapsed.
(* Simple queue implemented by an array
From
Developing Verified Programs with Dafny.
K. Rustan M. Leino. Tutorial notes, ICSE 2013.
For a similar data structure, see vstte12_ring_buffer.mlw
*)
module ToList
use import int.Int
use export array.Array
use export list.List
(** the list of elements a[l..u[ *)
function to_list (a: array 'a) (l u: int) : list 'a
axiom to_list_nil:
forall a: array 'a, l u: int. u <= l -> to_list a l u = Nil
axiom to_list_cons:
forall a: array 'a, l u: int. l < u ->
to_list a l u = Cons a[l] (to_list a (l+1) u)
lemma to_list_one:
forall a: array 'a, l: int. to_list a l (l+1) = Cons a[l] Nil
use import list.Append
lemma to_list_append:
forall a: array 'a, l m u: int. l <= m <= u ->
to_list a l u = to_list a l m ++ to_list a m u
lemma to_list_eq:
forall a1 a2: array 'a, l1 l2 u1 u2 len: int.
(forall i: int. 0 <= i < len -> a1[l1 + i] = a2[l2 + i]) ->
u1 - l1 = len -> u2 - l2 = len ->
to_list a1 l1 u1 = to_list a2 l2 u2
lemma to_list_frame:
forall a: array 'a, l u i: int, x: 'a.
(i < l \/ i >= u) -> to_list a[i <- x] l u = to_list a l u
end
module SimpleQueue
use import int.Int
use import array.Array
use import ToList
use import list.Append
type t 'a = {
mutable data: array 'a;
mutable m: int;
mutable n: int;
ghost mutable contents: list 'a; (* data[m..n[ *)
}
invariant { 0 < length self.data }
invariant { 0 <= self.m <= self.n <= length self.data }
invariant { self.contents = to_list self.data self.m self.n }
let create (x: 'a) : t 'a
ensures { result.contents = Nil }
=
{ data = Array.make 10 x;
m = 0; n = 0;
contents = Nil; }
let dequeue (q: t 'a) : 'a
requires { q.contents <> Nil }
writes { q.m, q.contents }
ensures { match old q.contents with
| Nil -> false
| Cons x tl -> result = x && q.contents = tl end }
=
let r = q.data[q.m] in
q.m <- q.m + 1;
ghost
match q.contents with Nil -> absurd | Cons _ tl -> q.contents <- tl end;
r
let enqueue (q: t 'a) (x: 'a) : unit
requires { q.n < length q.data }
(* writes { q.data, q.data.elts, q.m, q.n, q.contents } *)
writes { q.data.elts, q.n, q.contents }
ensures { q.contents = (old q.contents) ++ Cons x Nil }
=
(*
let len = q.n - q.m in
if q.n = length q.data then begin
if q.m = 0 then begin
let new = Array.make (2 * length q.data) q.data[0] in
Array.blit q.data q.m new 0 len;
q.data <- new
end else
Array.self_blit q.data q.m 0 len;
q.n <- len;
q.m <- 0
end;
*)
q.data[q.n] <- x;
q.n <- q.n + 1;
ghost q.contents <- q.contents ++ Cons x Nil
end
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
(* Why3 assumption *)
Inductive list
(a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (@list a a_WT) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
Parameter to_list: forall {a:Type} {a_WT:WhyType a}, (@array a a_WT) -> Z
-> Z -> (@list a a_WT).
Axiom to_list_nil : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)) (l:Z) (u:Z), (u <= l)%Z -> ((to_list a1 l u) = (Nil :(@list
a a_WT))).
Axiom to_list_cons : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)) (l:Z) (u:Z), (l < u)%Z -> ((to_list a1 l u) = (Cons (get a1 l)
(to_list a1 (l + 1%Z)%Z u))).
Axiom to_list_one : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)) (l:Z), ((to_list a1 l (l + 1%Z)%Z) = (Cons (get a1 l) (Nil :(@list
a a_WT)))).
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a} (l1:(@list a a_WT)) (l2:(@list
a a_WT)) {struct l1}: (@list a a_WT) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(@list
a a_WT)) (l2:(@list a a_WT)) (l3:(@list a a_WT)), ((infix_plpl l1
(infix_plpl l2 l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(@list
a a_WT)), ((infix_plpl l (Nil :(@list a a_WT))) = l).
(* Why3 assumption *)
Fixpoint length1 {a:Type} {a_WT:WhyType a} (l:(@list
a a_WT)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length1 r))%Z
end.
Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(@list
a a_WT)), (0%Z <= (length1 l))%Z.
Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(@list
a a_WT)), ((length1 l) = 0%Z) <-> (l = (Nil :(@list a a_WT))).
Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(@list
a a_WT)) (l2:(@list a a_WT)), ((length1 (infix_plpl l1
l2)) = ((length1 l1) + (length1 l2))%Z).
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(@list
a a_WT)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(@list
a a_WT)) (l2:(@list a a_WT)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/
(mem x l2)).
Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(@list
a a_WT)), (mem x l) -> exists l1:(@list a a_WT), exists l2:(@list a a_WT),
(l = (infix_plpl l1 (Cons x l2))).
Axiom to_list_append : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)) (l:Z) (m:Z) (u:Z), ((l <= m)%Z /\ (m <= u)%Z) -> ((to_list a1 l
u) = (infix_plpl (to_list a1 l m) (to_list a1 m u))).
Axiom to_list_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)) (a2:(@array a a_WT)) (l1:Z) (l2:Z) (u1:Z) (u2:Z) (len:Z),
(forall (i:Z), ((0%Z <= i)%Z /\ (i < len)%Z) -> ((get a1
(l1 + i)%Z) = (get a2 (l2 + i)%Z))) -> (((u1 - l1)%Z = len) ->
(((u2 - l2)%Z = len) -> ((to_list a1 l1 u1) = (to_list a2 l2 u2)))).
Axiom to_list_frame : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array
a a_WT)) (l:Z) (u:Z) (i:Z) (x:a), ((i < l)%Z \/ (u <= i)%Z) ->
((to_list (set a1 i x) l u) = (to_list a1 l u)).
(* Why3 assumption *)
Inductive t
(a:Type) {a_WT:WhyType a} :=
| mk_t : (@array a a_WT) -> Z -> Z -> (@list a a_WT) -> t a.
Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (t a).
Existing Instance t_WhyType.
Implicit Arguments mk_t [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): (@list
a a_WT) := match v with
| (mk_t x x1 x2 x3) => x3
end.
(* Why3 assumption *)
Definition n {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): Z :=
match v with
| (mk_t x x1 x2 x3) => x2
end.
(* Why3 assumption *)
Definition m {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): Z :=
match v with
| (mk_t x x1 x2 x3) => x1
end.
(* Why3 assumption *)
Definition data {a:Type} {a_WT:WhyType a} (v:(@t a a_WT)): (@array a a_WT) :=
match v with
| (mk_t x x1 x2 x3) => x
end.
Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem WP_parameter_enqueue : forall {a:Type} {a_WT:WhyType a},
forall (x:a), forall (rho:(@list a a_WT)) (rho1:Z) (rho2:Z) (rho3:Z)
(rho4:(@map.Map.map Z _ a a_WT)), (((((0%Z < rho3)%Z /\
(((0%Z <= rho2)%Z /\ (rho2 <= rho1)%Z) /\ (rho1 <= rho3)%Z)) /\
(rho = (to_list (mk_array rho3 rho4) rho2 rho1))) /\ (0%Z <= rho3)%Z) /\
(rho1 < rho3)%Z) -> (((0%Z <= rho1)%Z /\ (rho1 < rho3)%Z) ->
forall (o:(@map.Map.map Z _ a a_WT)), ((0%Z <= rho3)%Z /\
(o = (map.Map.set rho4 rho1 x))) -> forall (rho5:Z),
(rho5 = (rho1 + 1%Z)%Z) -> forall (rho6:(@list a a_WT)),
(rho6 = (infix_plpl rho (Cons x (Nil :(@list a a_WT))))) ->
(rho6 = (to_list (mk_array rho3 o) rho2 rho5))).
(* Why3 intros a a_WT x rho rho1 rho2 rho3 rho4
((((h1,((h2,h3),h4)),h5),h6),h7) (h8,h9) o (h10,h11) rho5 h12 rho6
h13. *)
intros a a_WT x rho rho1 rho2 rho3 rho4 ((((h1,((h2,h3),h4)),h5),h6),h7)
(h8,h9) o (h10,h11) rho5 h12 rho6 h13.
subst rho6.
symmetry.
rename rho2 into m.
rename rho1 into n.
rewrite (to_list_append _ m n rho5).
apply f_equal2.
3: omega.
rewrite to_list_eq with (mk_array rho3 o) (mk_array rho3 rho4) m m n n (n-m)%Z.
ae.
ae.
ae.
ae.
rewrite to_list_cons.
apply f_equal2.
ae.
ae.
ae.
Qed.
This diff is collapsed.
......@@ -92,6 +92,15 @@ module Array
ensures { forall i:int.
ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2] }
val self_blit (a: array 'a) (ofs1: int) (ofs2: int) (len: int) : unit
writes {a}
requires { 0 <= ofs1 /\ 0 <= len /\ ofs1 + len <= length a }
requires { 0 <= ofs2 /\ ofs2 + len <= length a }
ensures { forall i:int.
(0 <= i < ofs2 \/ ofs2 + len <= i < length a) -> a[i] = (old a)[i] }
ensures { forall i:int.
ofs2 <= i < ofs2 + len -> a[i] = (old a)[ofs1 + i - ofs2] }
(*** TODO?
- concat : 'a array list -> 'a array
- to_list
......
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