Commit c9031b7a authored by MARCHE Claude's avatar MARCHE Claude

Improved why3doc for some theories

parent e65924cf
......@@ -79,7 +79,7 @@ theory SimplePath
predicate edge graph vertex vertex
(* [simple_path g src [x1;...;xn] dst] is a path
(** [simple_path g src [x1;...;xn] dst] is a path
src --> x1 --> x2 --> ... --> xn --> dst without repetition. *)
inductive simple_path graph vertex (list vertex) vertex =
| Path_empty :
......
......@@ -358,7 +358,7 @@ theory Iter
type t
function f t : t
(* f^k(x) *)
(** [iter k x] is [f^k(x)] *)
function iter int t : t
axiom iter_0: forall x: t. iter 0 x = x
......
......@@ -342,7 +342,7 @@ theory NumOcc
use import int.Int
use import List
(* number of occurrence of x in l *)
(** number of occurrences of [x] in [l] *)
function num_occ (x: 'a) (l: list 'a) : int =
match l with
| Nil -> 0
......
......@@ -13,7 +13,7 @@ theory Map
function get (map 'a 'b) 'a : 'b
function set (map 'a 'b) 'a 'b : map 'a 'b
(* syntactic sugar *)
(** syntactic sugar *)
function ([]) (a : map 'a 'b) (i : 'a) : 'b = get a i
function ([<-]) (a : map 'a 'b) (i : 'a) (v : 'b) : map 'a 'b = set a i v
......@@ -44,7 +44,8 @@ theory MapSorted
predicate le elt elt
(* a[l..u) is sorted for le *)
(** [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]
......@@ -67,15 +68,23 @@ 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]
(** [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)
(** [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
(** 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
......@@ -89,6 +98,9 @@ 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]
......@@ -97,6 +109,13 @@ theory MapPermut
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
......@@ -133,7 +152,7 @@ theory MapSum
use import int.Int
use export Map
(* [sum m l h] is the sum of m[i] for l <= i < h *)
(** [sum m l h] is the sum of [m[i]] for [l <= i < h] *)
type container = map int int
clone export sum.Sum with type container = container, function f = get
......@@ -173,7 +192,7 @@ theory BitVector
forall v1 v2:bv, n:int. 0 <= n < size ->
nth (bw_and v1 v2) n = andb (nth v1 n) (nth v2 n)
(* logical shift right *)
(** logical shift right *)
function lsr bv int : bv
axiom Lsr_nth_low:
......@@ -182,7 +201,7 @@ theory BitVector
axiom Lsr_nth_high:
forall b:bv,n s:int. n+s >= size -> nth (lsr b s) n = False
(* arithmetic shift right *)
(** arithmetic shift right *)
function asr bv int : bv
axiom Asr_nth_low:
......@@ -191,7 +210,7 @@ theory BitVector
axiom Asr_nth_high:
forall b:bv,n s:int. n+s >= size -> nth (asr b s) n = nth b (size-1)
(* logical shift left *)
(** logical shift left *)
function lsl bv int : bv
axiom Lsl_nth_high:
......
......@@ -7,10 +7,10 @@ theory Sum "Sum of the elements of an indexed container"
type container
(* [f c i] is the [i]-th element in the container [c] *)
(** [f c i] is the [i]-th element in the container [c] *)
function f container int : int
(* [sum c i j] is the sum Sum_{i <= k < j} f c k *)
(** [sum c i j] is the sum Sum_{i <= k < j} f c k *)
function sum container int int : int
axiom Sum_def_empty :
......
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