Commit fce5a9a2 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

why3doc documentation of some theories

parent 92ec2022
......@@ -806,6 +806,8 @@ to verified goals.
\section{The \texttt{why3doc} tool}
\label{sec:why3doc}
This tool can produce HTML pages from \why source code.
\todo{Documenter}
......
(** {1 Formalization of Floating-Point Arithmetic}
This formalization follows the {h <a href="http://ieeexplore.ieee.org/servlet/opac?punumber=4610933">IEEE-754 norm</a>}
......@@ -15,7 +14,14 @@ theory Rounding
end
(** {2 handling of IEEE-754 special values +\infty, -\infty, NaN, +0, -0} *)
(** {2 handling of IEEE-754 special values}
Special values are +infinity, -infinity; NaN, +0, -0. These are
handled as described in {h <a
href="http://www.lri.fr/~marche/ayad10ijcar.pdf">[Ayad, March&eacute;,
IJCAR, 2010]</a>}
*)
theory SpecialValues
type class = Finite | Infinite | NaN
......
(** {1 Theory of integers}
(** {1 Theory of integers}
This file provides the basic theory of integers, and several additional theories for classical functions
This file provides the basic theory of integers, and several additional
theories for classical functions
*)
......@@ -99,7 +100,7 @@ end
(** {2 Division by 2}
The particular case of Euclidean division by 2
The particular case of Euclidean division by 2
*)
theory Div2
......@@ -113,10 +114,9 @@ end
(** {2 Computer Division}
Division and modulo operators with the same conventions as
mainstream programming language such C, Java, OCaml, that is
division rounds towards zero, and thus [mod x y] has the same sign
as x
Division and modulo operators with the same conventions as mainstream
programming language such C, Java, OCaml, that is division rounds
towards zero, and thus [mod x y] has the same sign as x
*)
......@@ -172,6 +172,7 @@ theory ComputerDivision
end
(** {2 Generic Exponentation of something to an integer exponent} *)
theory Exponentiation
use import Int
......@@ -205,10 +206,11 @@ theory Power
end
(** {2 Number of elements satisfying a given predicate}
(** {2 Number of elements satisfying a given predicate}
This theory is parametrized by a predicate [pr]. It is supposed to be cloned
with needed instances for [pr]. It is also parametrized by a type [param] to be used as an additional parameter to [pr].
This theory is parametrized by a predicate [pr]. It is supposed to be
cloned with needed instances for [pr]. It is also parametrized by a
type [param] to be used as an additional parameter to [pr].
*)
theory NumOfParam
......@@ -305,7 +307,7 @@ end
(** {2 Factorial function} *)
theory Fact
theory Fact
use export Int
......@@ -337,6 +339,7 @@ theory Iter
end
(** {2 Integers extended with an infinite value} *)
theory IntInf
use import Int
......@@ -372,8 +375,9 @@ end
(** {2 Induction principle on integers}
This theory can be cloned with the wanted predicate, to perform an induction, either
on non-negative integers, or more generally on integers greater or equal a given bound.
This theory can be cloned with the wanted predicate, to perform an
induction, either on non-negative integers, or more generally on
integers greater or equal a given bound.
*)
......
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