Commit 4d12ced3 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use the postfix form of documentation for theories and modules.

parent 5da314b8
......@@ -8,58 +8,59 @@ module Pqueue
(** {3 Types} *)
type elt
(** the abstract type of elements *)
(** [elt] is equipped with a total order [rel] *)
clone export relations.TotalOrder with type t = elt
(** [elt] is equipped with a total order [rel] *)
(** the priority queue is modeled as a list of elements *)
use import list.List
use import list.Mem
use import list.Permut
use import list.Length
type t model { mutable elts: list elt }
(** the priority queue is modeled as a list of elements *)
(** {3 Operations} *)
(** creates a fresh, empty queue *)
val create () : t ensures { result.elts = Nil }
(** create a fresh, empty queue *)
(** pushes an element in a queue *)
val push (x: elt) (q: t) : unit writes {q}
ensures { q.elts = Cons x (old q.elts) }
(** push an element in a queue *)
(** exception raised by [pop] and [peek] to signal an empty queue *)
exception Empty
(** exception raised by [pop] and [peek] to signal an empty queue *)
(** [pop] and [peek] return the minimal element, defined as follows *)
predicate minimal_elt (x: elt) (s: list elt) =
mem x s /\ forall e: elt. mem e s -> rel x e
(** property of the element returned by [pop] and [peek] *)
(** removes and returns the minimal element *)
val pop (q: t) : elt writes {q}
ensures { permut (Cons result q.elts) (old q.elts) }
ensures { minimal_elt result (old q.elts) }
raises { Empty -> q.elts = (old q.elts) = Nil }
(** remove and return the minimal element *)
(** returns the minimal element, without modifying the queue *)
val peek (q: t) : elt
ensures { minimal_elt result q.elts }
raises { Empty -> q.elts = Nil }
(** return the minimal element, without modifying the queue *)
(** empties the queue *)
val clear (q: t) : unit writes {q} ensures { q.elts = Nil }
(** empty the queue *)
(** returns a fresh copy of the queue *)
val copy (q: t) : t ensures { result = q }
(** return a fresh copy of the queue *)
(** checks whether the queue is empty *)
val is_empty (q: t) : bool
ensures { result = True <-> q.elts = Nil }
(** check whether the queue is empty *)
(** returns the number of elements in the queue *)
val length (q: t) : int
ensures { result = length q.elts }
(** return the number of elements in the queue *)
end
......@@ -73,56 +74,56 @@ module PqueueNoDup
(** {3 Types} *)
(** the abstract type of elements *)
type elt
(** the abstract type of elements *)
(** [elt] is equipped with a total order [rel] *)
clone export relations.TotalOrder with type t = elt
(** [elt] is equipped with a total order [rel] *)
(** the priority queue is modeled as a finite set of elements *)
use import set.Fset
type t model { mutable elts: set elt }
(** the priority queue is modeled as a finite set of elements *)
(** {3 Operations} *)
(** creates a fresh, empty queue *)
val create () : t ensures { result.elts = empty }
(** create a fresh, empty queue *)
(** pushes an element in a queue *)
val push (x: elt) (q: t) : unit writes {q}
ensures { q.elts = add x (old q.elts) }
(** push an element in a queue *)
(** exception raised by [pop] and [peek] to signal an empty queue *)
exception Empty
(** exception raised by [pop] and [peek] to signal an empty queue *)
(** [pop] and [peek] return the minimal element, defined as follows *)
predicate minimal_elt (x: elt) (s: set elt) =
mem x s /\ forall e: elt. mem e s -> rel x e
(** property of the element returned by [pop] and [peek] *)
(** removes and returns the minimal element *)
val pop (q: t) : elt writes {q}
ensures { q.elts = remove result (old q.elts) }
ensures { minimal_elt result (old q.elts) }
raises { Empty -> q.elts = (old q.elts) = empty }
(** remove and returns the minimal element *)
(** returns the minimal element, without modifying the queue *)
val peek (q: t) : elt
ensures { minimal_elt result q.elts }
raises { Empty -> q.elts = empty }
(** return the minimal element, without modifying the queue *)
(** empties the queue *)
val clear (q: t) : unit writes {q} ensures {q.elts = empty }
(** empty the queue *)
(** returns a fresh copy of the queue *)
val copy (q: t) : t ensures { result = q }
(** return a fresh copy of the queue *)
(** checks whether the queue is empty *)
val is_empty (q: t) : bool
ensures { result=True <-> q.elts = empty }
(** check whether the queue is empty *)
(** returns the number of elements in the queue *)
val length (q: t) : int
ensures { result = cardinal q.elts }
(** return the number of elements in the queue *)
end
......@@ -10,14 +10,14 @@ theory Path
predicate edge vertex vertex
(** [path v0 [v0; v1; ...; vn-1] vn]
means a path from [v0] to [vn] composed of [n] edges [(vi,vi+1)]. *)
inductive path vertex (list vertex) vertex =
| Path_empty:
forall x: vertex. path x Nil x
| Path_cons:
forall x y z: vertex, l: list vertex.
edge x y -> path y l z -> path x (Cons x l) z
(** [path v0 [v0; v1; ...; vn-1] vn]
means a path from [v0] to [vn] composed of [n] edges [(vi,vi+1)]. *)
lemma path_right_extension:
forall x y z: vertex, l: list vertex.
......@@ -49,12 +49,12 @@ theory IntPathWeight
function weight vertex vertex : int
(** the total weight of a path [path _ l dst] *)
function path_weight (l: list vertex) (dst: vertex) : int = match l with
| Nil -> 0
| Cons x Nil -> weight x dst
| Cons x ((Cons y _) as r) -> weight x y + path_weight r dst
end
(** the total weight of a path [path _ l dst] *)
lemma path_weight_right_extension:
forall x y: vertex, l: list vertex.
......
......@@ -253,8 +253,8 @@ theory NumOfParam
predicate pr param int
(** number of [n] such that [a <= n < b] and [pr p n] *)
function num_of (p : param) (a b : int) : int
(** number of [n] such that [a <= n < b] and [pr p n] *)
axiom Num_of_empty :
forall p : param, a b : int.
......@@ -358,8 +358,8 @@ theory Iter
type t
function f t : t
(** [iter k x] is [f^k(x)] *)
function iter int t : t
(** [iter k x] is [f^k(x)] *)
axiom iter_0: forall x: t. iter 0 x = x
axiom iter_s: forall k: int, x: t. 0 < k -> iter k x = iter (k-1) (f x)
......
......@@ -356,12 +356,12 @@ theory NumOcc
use import int.Int
use import List
(** number of occurrences of [x] in [l] *)
function num_occ (x: 'a) (l: list 'a) : int =
match l with
| Nil -> 0
| Cons y r -> (if x = y then 1 else 0) + num_occ x r
end
end
(** number of occurrences of [x] in [l] *)
use import Mem
......
......@@ -44,10 +44,10 @@ theory MapSorted
predicate le elt elt
(** [sorted_sub a l u] is true whenever the array segment [a(l..u-1)]
is sorted w.r.t order relation [le] *)
predicate sorted_sub (a : map int elt) (l u : int) =
forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2]
(** [sorted_sub a l u] is true whenever the array segment [a(l..u-1)]
is sorted w.r.t order relation [le] *)
end
......@@ -68,26 +68,26 @@ theory MapInjection
use import int.Int
use export Map
(** [injective a n] is true when [a] is an injection
on the domain [(0..n-1)] *)
predicate injective (a: map int int) (n: int) =
forall i j: int. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]
(** [injective a n] is true when [a] is an injection
on the domain [(0..n-1)] *)
(** [surjective a n] is true when [a] is a surjection
from [(0..n-1)] to [(0..n-1)] *)
predicate surjective (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i)
(** [surjective a n] is true when [a] is a surjection
from [(0..n-1)] to [(0..n-1)] *)
(** [range a n] is true when [a] maps the domain
[(0..n-1)] into [(0..n-1)] *)
predicate range (a: map int int) (n: int) =
forall i: int. 0 <= i < n -> 0 <= a[i] < n
(** [range a n] is true when [a] maps the domain
[(0..n-1)] into [(0..n-1)] *)
(** main lemma: an injection on [(0..n-1)] that
ranges into [(0..n-1)] is also a surjection *)
lemma injective_surjective:
forall a: map int int, n: int.
injective a n -> range a n -> surjective a n
(** main lemma: an injection on [(0..n-1)] that
ranges into [(0..n-1)] is also a surjection *)
end
......@@ -98,24 +98,17 @@ theory MapPermut
use import int.Int
use export Map
(** [exchange m1 m2 i j] is true when the maps [m1]
and [m2] are identical except at indexes [i]
and [j], where the values are exchanged *)
predicate exchange (a1 a2 : map int 'a) (i j : int) =
a1[i] = a2[j] /\ a2[i] = a1[j] /\
forall k:int. (k <> i /\ k <> j) -> a1[k] = a2[k]
(** [exchange m1 m2 i j] is true when the maps [m1]
and [m2] are identical except at indexes [i]
and [j], where the values are exchanged *)
lemma exchange_set :
forall a : map int 'a. forall i j : int.
exchange a a[i <- a[j]][j <- a[i]] i j
(** [permut_sub m1 m2 l u] is true when the segment
[m1(l..u-1)] is a permutation of the segment
[m2(l..u-1)]
It is defined inductively as the smallest
equivalence relation that contains the
exchanges *)
inductive permut_sub (map int 'a) (map int 'a) int int =
| permut_refl :
forall a : map int 'a. forall l u : int. permut_sub a a l u
......@@ -128,6 +121,13 @@ theory MapPermut
| permut_exchange :
forall a1 a2 : map int 'a. forall l u i j : int.
l <= i < u -> l <= j < u -> exchange a1 a2 i j -> permut_sub a1 a2 l u
(** [permut_sub m1 m2 l u] is true when the segment
[m1(l..u-1)] is a permutation of the segment
[m2(l..u-1)]
It is defined inductively as the smallest
equivalence relation that contains the
exchanges *)
lemma permut_weakening :
forall a1 a2 : map int 'a. forall l1 r1 l2 r2 : int.
......
......@@ -7,11 +7,11 @@ theory Sum "Sum of the elements of an indexed container"
type container
(** [f c i] is the [i]-th element in the container [c] *)
function f container int : int
(** [f c i] is the [i]-th element in the container [c] *)
(** [sum c i j] is the sum Sum_{i <= k < j} f c k *)
function sum container int int : int
(** [sum c i j] is the sum Sum_{i <= k < j} f c k *)
axiom Sum_def_empty :
forall c : container, i j : int. j <= i -> sum c i j = 0
......
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