Commit f840e0be authored by MARCHE Claude's avatar MARCHE Claude

Why3doc for modules

parent 412b6e68
......@@ -1000,11 +1000,11 @@ $(WHY3DOCDEP): $(WHY3DOCGENERATED)
byte: bin/why3doc.byte
opt: bin/why3doc.opt
bin/why3doc.opt: src/why3.cmxa $(WHY3DOCCMX)
bin/why3doc.opt: src/why3.cmxa $(PGMCMX) $(WHY3DOCCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3doc.byte: src/why3.cma $(WHY3DOCCMO)
bin/why3doc.byte: src/why3.cma $(PGMCMO) $(WHY3DOCCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
......@@ -1189,12 +1189,16 @@ STDLIBS = bool comparison relations \
option list map set bag graph
# function ? sum ? tptp ?
STDMODS = ref array arith hashtbl impset pqueue queue random stack string
STDLIBFILES = $(addsuffix .why, $(addprefix theories/, $(STDLIBS)))
STDMODFILES = $(addsuffix .mlw, $(addprefix modules/, $(STDMODS)))
stdlibdoc: $(STDLIBFILES) bin/why3doc
stdlibdoc: $(STDLIBFILES) $(STDMODFILES) bin/why3doc
mkdir -p doc/stdlibdoc
rm -f doc/stdlibdoc/style.css
WHY3LOADPATH=theories bin/why3doc -o doc/stdlibdoc $(STDLIBFILES)
WHY3LOADPATH=theories bin/why3doc -L modules -o doc/stdlibdoc \
$(STDLIBFILES) $(STDMODFILES)
clean::
rm -f doc/stdlibdoc/*
......
(* Arithmetic for programs *)
(** {1 Arithmetic for programs} *)
(** {2 Integer Division}
It is checked that divisor is not null
*)
module Int
......@@ -8,9 +14,14 @@ module Int
let (/) (x: int) (y:int) = { y <> 0 } div x y { result = div x y }
end
(* machine arithmetic (32-bit integers, etc.) will go here *)
(** {2 Machine integers}
32-bit integers and such go here
*)
module Int32
use export int.Int
......@@ -36,6 +47,11 @@ module Int32
end
(** {2 Division on real numbers}
See also Floating-Point theories
*)
module Real
use import real.Real
......@@ -46,7 +62,7 @@ module Real
end
(*
(***
Local Variables:
compile-command: "unset LANG; make -C .. modules/arith"
End:
......
(** {1 Arrays} *)
(* Arrays *)
(** {2 Generic Arrays}
The length is a non-mutable field, so that we get for free that modification of an array does not modify its length
*)
module Array
......@@ -13,7 +18,7 @@ module Array
function set (a: array 'a) (i: int) (v: 'a) : array 'a =
{| a with elts = M.set a.elts i v |}
(* syntactic sugar *)
(** syntactic sugar *)
function ([]) (a: array 'a) (i: int) : 'a = get a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
......@@ -25,7 +30,7 @@ module Array
val length (a: array 'a) : {} int { result = a.length }
(* unsafe get/set operations with no precondition *)
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: array 'a) (i: int) =
......@@ -46,7 +51,7 @@ module Array
{ n >= 0 }
array 'a
{ result = {| length = n; elts = M.const v |} }
(* { length result = n /\ forall i:int. 0 <= i < n -> result[i] = v} *)
(*** { length result = n /\ forall i:int. 0 <= i < n -> result[i] = v} *)
val append (a1: array 'a) (a2: array 'a) :
{}
......@@ -97,7 +102,7 @@ module Array
(forall i:int.
ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2]) }
(* TODO?
(*** TODO?
- concat : 'a array list -> 'a array
- to_list
- of_list
......@@ -105,6 +110,9 @@ module Array
end
(** {2 Sorted Arrays} *)
module ArraySorted
use import int.Int
......@@ -119,6 +127,8 @@ module ArraySorted
end
(** {2 Arrays Equality} *)
module ArrayEq
use import module Array
......@@ -133,6 +143,8 @@ module ArrayEq
end
(** {2 Permutation} *)
module ArrayPermut
use import int.Int
......@@ -174,12 +186,14 @@ module ArrayPermut
end
(** {2 Sum of elements} *)
module ArraySum
use import module Array
clone import map.MapSum as M
(* [sum a l h] is the sum of a[i] for l <= i < h *)
(** [sum a l h] is the sum of [a[i]] for [l <= i < h] *)
function sum (a: array int) (l h: int) : int = M.sum a.elts l h
......@@ -222,7 +236,7 @@ module TestArray
end
(*
(***
Local Variables:
compile-command: "unset LANG; make -C .. modules/array"
End:
......
(* Hash tables à la OCaml: each key is mapped to a *stack* of values,
(** {1 Hash tables}
This module provides Hash tables à la OCaml. Each key is mapped to a *stack* of values,
with [add h k v] pushing a new value [v] for key [k],
and [remove h k] popping a value for key [key]. *)
and [remove h k] popping a value for key [key].
*)
module Hashtbl
......@@ -67,7 +71,7 @@ module Hashtbl
/\
forall k': key. k' <> k -> h[k'] = (old h)[k'] }
(* TODO
(*** TODO
- val length: t 'a -> int (the number of distinct key)
- val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
- val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
......@@ -101,7 +105,7 @@ module TestHashtbl
end
(*
(***
Local Variables:
compile-command: "unset LANG; make -C .. modules/hashtbl"
End:
......
(* An imperative set is simply a reference containing a finite set *)
(** {1 Imperative sets}
An imperative set is simply a reference containing a finite set
*)
module Impset
use export set.Fset
......@@ -36,7 +41,7 @@ module Impset
end
(*
(***
Local Variables:
compile-command: "unset LANG; make -C .. modules/impset"
End:
......
(* Polymorphic mutable priority queues. *)
(** {1 Priority queues} *)
(** {2 Polymorphic mutable priority queues} *)
module Pqueue
(** {3 Types} *)
type elt
(* [elt] is equipped with a total order [rel] *)
(** [elt] is equipped with a total order [rel] *)
clone export relations.TotalOrder with type t = elt
(* the priority queue is modeled as a list of elements *)
(** the priority queue is modeled as a list of elements *)
use import list.List
use import list.Mem
use import list.Permut
......@@ -16,26 +20,26 @@ module Pqueue
type t model {| mutable elts: list elt |}
(* Operations. *)
(** {3 Operations} *)
(* creates a fresh, empty queue *)
(** creates a fresh, empty queue *)
val create: unit -> {} t { result.elts = Nil }
(* pushes an element in a queue *)
(** pushes an element in a queue *)
val push:
x: elt -> q: t ->
{ }
unit writes q
{ q.elts = Cons x (old q.elts) }
(* exception raised by pop and peek to signal an empty queue *)
(** exception raised by [pop] and [peek] to signal an empty queue *)
exception Empty
(* pop and peek return the minimal element, defined as follows *)
(** [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
(* removes and returns the minimal element *)
(** removes and returns the minimal element *)
val pop:
q: t ->
{}
......@@ -45,7 +49,7 @@ module Pqueue
minimal_elt result (old q.elts) }
| Empty -> { q.elts = (old q.elts) = Nil }
(* returns the minimal element, without modifying the queue *)
(** returns the minimal element, without modifying the queue *)
val peek:
q: t ->
{}
......@@ -53,17 +57,17 @@ module Pqueue
reads q raises Empty
{ minimal_elt result q.elts } | Empty -> { q.elts = Nil }
(* empties the queue *)
(** empties the queue *)
val clear: q: t -> {} unit writes q {q.elts = Nil }
(* returns a fresh copy of the queue *)
(** returns a fresh copy of the queue *)
val copy: q: t -> {} t reads q { result = q }
(* checks whether the queue is empty *)
(** checks whether the queue is empty *)
val is_empty:
q: t -> {} bool reads q { result=True <-> q.elts = Nil }
(* returns the number of elements in the queue *)
(** returns the number of elements in the queue *)
val length: q: t -> {} int reads q { result = length q.elts }
end
......@@ -95,43 +99,47 @@ module Test
end
(* Simpler interface when duplicate elements are not allowed *)
(** {2 Simpler interface}
when duplicate elements are not allowed
*)
module PqueueNoDup
(* Types. *)
(** {3 Types} *)
(* the abstract type of elements *)
(** the abstract type of elements *)
type elt
(* [elt] is equipped with a total order [rel] *)
(** [elt] is equipped with a total order [rel] *)
clone export relations.TotalOrder with type t = elt
(* the priority queue is modeled as a finite set of elements *)
(** the priority queue is modeled as a finite set of elements *)
use import set.Fset
type t model {| mutable elts: set elt |}
(* Operations. *)
(** {3 Operations} *)
(* creates a fresh, empty queue *)
(** creates a fresh, empty queue *)
val create: unit -> {} t { result.elts = empty }
(* pushes an element in a queue *)
(** pushes an element in a queue *)
val push:
x: elt -> q: t ->
{ }
unit writes q
{ q.elts = add x (old q.elts) }
(* exception raised by pop and peek to signal an empty queue *)
(** exception raised by [pop] and [peek] to signal an empty queue *)
exception Empty
(* pop and peek return the minimal element, defined as follows *)
(** [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
(* removes and returns the minimal element *)
(** removes and returns the minimal element *)
val pop:
q: t ->
{}
......@@ -140,7 +148,7 @@ module PqueueNoDup
{ q.elts = remove result (old q.elts) /\ minimal_elt result (old q.elts) }
| Empty -> { q.elts = (old q.elts) = empty }
(* returns the minimal element, without modifying the queue *)
(** returns the minimal element, without modifying the queue *)
val peek:
q: t ->
{}
......@@ -148,17 +156,17 @@ module PqueueNoDup
reads q raises Empty
{ minimal_elt result q.elts } | Empty -> { q.elts = empty }
(* empties the queue *)
(** empties the queue *)
val clear: q: t -> {} unit writes q {q.elts = empty }
(* returns a fresh copy of the queue *)
(** returns a fresh copy of the queue *)
val copy: q: t -> {} t reads q { result = q }
(* checks whether the queue is empty *)
(** checks whether the queue is empty *)
val is_empty:
q: t -> {} bool reads q { result=True <-> q.elts = empty }
(* returns the number of elements in the queue *)
(** returns the number of elements in the queue *)
val length: q: t -> {} int reads q { result = cardinal q.elts }
end
......@@ -190,7 +198,7 @@ module TestNoDup
end
(*
(***
Local Variables:
compile-command: "unset LANG; make -C .. modules/pqueue"
End:
......
(* Polymorphic mutable queues *)
(** {1 Polymorphic mutable queues} *)
module Queue
......@@ -68,7 +68,7 @@ module Test
end
(*
(***
Local Variables:
compile-command: "unset LANG; make -C .. modules/queue"
End:
......
(* Pseudo-random generators.
(** {1 Pseudo-random generators}
This easiest way to get random numbers (of random values of any type)
is to take advantage of the non-determinism of Hoare triples.
Simply declaring a function
val random_int: unit -> {} int {}
[val random_int: unit -> {} int {}]
is typically enough. Two calls to random_int return values that can not
is typically enough. Two calls to [random_int] return values that can not
be proved equal, which is exactly what we need.
The following modules provide slightly more: pseudo-random generators
which are deterministic according to a state. The state is either
explicit (module State) or global (module Random). Functions init allow
explicit (module [State]) or global (module [Random]). Functions init allow
to reset the generators according to a given seed.
*)
(* Purely applicative generators. *)
(** {2 Purely applicative generators} *)
theory Generator
......@@ -39,8 +40,9 @@ theory Generator
end
(* Mutable states of pseudo-random generators.
Basically a reference containing a pure generator. *)
(** {2 Mutable states of pseudo-random generators}
Basically a reference containing a pure generator. *)
module State
......@@ -71,7 +73,7 @@ module State
end
(* A global pseudo-random generator. *)
(** {2 A global pseudo-random generator} *)
module Random
......@@ -112,7 +114,7 @@ module Test
end
(*
(***
Local Variables:
compile-command: "unset LANG; make -C .. modules/random"
End:
......
(* References.
(** {1 References}
A mutable variable, or ``reference'' in ML terminology, is simply a
record with a single mutable field 'contents'.
record with a single mutable field [contents].
Creation, access, and assignment are provided as 'ref', prefix '!', and
infix ':=', respectively.
*)
(** {2 Generic references}
Creation, access, and assignment are provided as [ref], prefix [!], and
infix [:=], respectively.
*)
module Ref
......@@ -22,7 +26,9 @@ module Ref
end
(* Module Refint adds a few operations specific to integer references. *)
(** {2 Integer References}
a few operations specific to integer references *)
module Refint
......@@ -38,7 +44,7 @@ module Refint
end
(*
(***
Local Variables:
compile-command: "unset LANG; make -C .. modules/ref"
End:
......
(* Polymorphic mutable stacks *)
(** {1 Stacks} *)
(** {2 Polymorphic mutable stacks} *)
module Stack
......@@ -39,7 +41,7 @@ module Stack
val is_empty:
s: t 'a -> {} bool reads s { result=True <-> s.elts = Nil }
(*
(***
val length: s: t 'a -> {} int reads s { result = length s.elts }
*)
function length (s: t 'a) : int = L.length s.elts
......@@ -70,7 +72,7 @@ module Test
end
(*
(***
Local Variables:
compile-command: "unset LANG; make -C .. modules/stack"
End:
......
(** {1 Characters and Strings} *)
(** {2 Characters} *)
module Char
use import int.Int
......@@ -25,12 +29,14 @@ module Char
val uppercase : c:char -> {} char { result = uppercase c }
val lowercase : c:char -> {} char { result = lowercase c }
(* TODO
(*** TODO
- compare ?
*)
end
(** {2 Strings} *)
module String
use import int.Int
......@@ -82,7 +88,7 @@ module String
forall i:int. 0 <= i < length result ->
result[i] = Char.lowercase s[i] }
(* TODO
(*** TODO
- copy
- sub
- fill
......@@ -95,6 +101,8 @@ module String
end
(** {2 Buffers} *)
module Buffer
use import int.Int
......@@ -128,7 +136,7 @@ module Buffer
(forall i: int.
0 <= i < S.length s -> b.contents[old (length b) + i] = S.get s i) }
(* TODO
(*** TODO
- add_substring
- add_buffer
*)
......@@ -161,7 +169,7 @@ module Test
end
***)
(*
(***
Local Variables:
compile-command: "unset LANG; make -C .. modules/string"
End:
......
......@@ -99,7 +99,7 @@ rule scan fmt = parse
| "(*)" as s
{ pp_print_string fmt s;
scan fmt lexbuf }
| "(***"
| ' '* "(***"
{ comment fmt false lexbuf;
scan fmt lexbuf }
| ' '* "(**"
......
theory Map "Theory of maps"
(** {1 Theory of maps} *)
(** {2 Generic Maps} *)
theory Map
type map 'a 'b
......@@ -26,6 +30,8 @@ theory Map "Theory of maps"
end
(** {2 Sorted Maps (indexed by integers)} *)
theory MapSorted
use import int.Int
......@@ -41,6 +47,7 @@ theory MapSorted
end
(** {2 Maps Equality (indexed by integers)} *)
theory MapEq
use import int.Int
......@@ -51,6 +58,7 @@ theory MapEq
end
(** {2 Injectivity and surjectivity for maps (indexed by integers)} *)
theory MapInjection
use import int.Int
......@@ -72,6 +80,7 @@ theory MapInjection
end
(** {2 Map Permutation (indexed by integers)} *)
theory MapPermut
use import int.Int
......@@ -117,6 +126,7 @@ theory MapPermut
end
(** {2 Sum of elements of a map (indexed by integers)} *)
theory MapSum
use import int.Int
......@@ -129,6 +139,12 @@ theory MapSum
end
(** {2 Bitvectors (arbitrary length)}
Seen as maps from int to bool
*)
theory BitVector
use export bool.Bool
......@@ -185,6 +201,8 @@ theory BitVector
end
(** {2 32-bits Bitvectors} *)
theory BV32
constant size : int = 32
......
(* number theory *)
(** {1 Number theory} *)
(** {2 Parity properties} *)
theory Parity
......@@ -24,6 +27,8 @@ theory Parity
end
(** {2 Divisibility} *)
theory Divisibility
use export int.Int
......@@ -88,6 +93,8 @@ theory Divisibility
end
(** {2 Greateast Common Divisor} *)
theory Gcd
use export int.Int
......@@ -111,7 +118,7 @@ theory Gcd
clone algebra.AC with type t = int, function op = gcd,
lemma Comm.Comm, lemma Assoc.Assoc
(* FIXME: Alt-Ergo proves gcd_0_pos even without gcd_unique *)
(*** FIXME: Alt-Ergo proves gcd_0_pos even without gcd_unique *)
lemma gcd_0_pos: forall a: int. 0 <= a -> gcd a 0 = a
lemma gcd_0_neg: forall a: int. a < 0 -> gcd a 0 = -a
......@@ -135,6 +142,8 @@ theory Gcd
end
(** {2 Prime numbers} *)
theory Prime
use export int.Int
......@@ -164,6 +173,8 @@ theory Prime
end
(** {2 Coprime numbers} *)
theory Coprime
use export int.Int
......
(** {1 Option type} *)
theory Option
......
(** {1 Relations} *)
theory EndoRelation
type t
predicate rel t t
......
(** {1 Set theories} *)
(** {2 General Sets} *)
theory Set
type set 'a
......@@ -83,6 +85,8 @@ theory Set
end
(** {2 Set Comprehension} *)
theory SetComprehension
use export Set
......@@ -183,6 +187,8 @@ theory Fsetint
end
(** {2 Set extensionality} *)
theory FsetExt
use export Fset
......@@ -192,6 +198,8 @@ theory FsetExt
end
(** {2 Sets realized as maps} *)
theory SetMap
use import map.Map
......
Markdown is supported
0%
or