Commit 1cbd210d authored by MARCHE Claude's avatar MARCHE Claude

docs

parent 55f2ec5d
......@@ -30,6 +30,9 @@
= Roadmap for 2011 =
* Jessie3
......@@ -37,7 +40,10 @@
* Coq plugin
== Papers to write ==
= Papers to write =
* Encodings and transformations (Andrei+Francois, CADE 2011, deadline January 2011)
* Caml code ?
......
......@@ -4,7 +4,7 @@
\section{Architecture and Terminology}
Everything in Why3 revolves around the notion of
\emph{task}\index{task}. Why3, as a platform, as a tool that
\emph{task}\index{task}. Why3, as a platform, is a tool that
translates its input to a number of tasks, and dispatches these tasks
to external provers.
......@@ -22,6 +22,8 @@ extended with
%\item Hilbert's epsilon construct
\end{itemize}
TODO: continue
\section{Organization of this document}
This document is organized as follows. The first three chapters are
......@@ -35,12 +37,19 @@ theories and goals, call external provers for trying to solve them,
apply transformations to simplify them. The two first chapters are
thus to read for the beginners.
Chapter~\ref{chap:library} documents the standard library of theories
distributed with Why3. Chapter~\ref{chap:whyml} presents the
verification condition generator built upon the Why3 core. The two
next chapters are for users with a little more experience, in
particular those who wants to use Why for verification of algorithms.
Chapter~\ref{chap:api} presents how to use Why3 programmatically,
using the API. It is for the more advanced users, who wants to link
Why3 library with their own code.
using the API. It is for the experimented users, who wants to link
Why3 library with their own code.
Chapter~\ref{chap:manpages} are the technical manual pages for the tools of
the platform. All tool options, and all the configuration files are described in details there.
Chapter~\ref{chap:manpages} are the technical manual pages for the
tools of the platform. All tool options, and all the configuration
files are described in details there.
Chapter~\ref{chap:apidoc} is the technical documentation of the API.
......
\chapter{Standard Library}
\label{chap:library}
\section{Integers}
\section{Integer divisions}
Euclidean versus Computer division
\section{Arrays}
\section{Real numbers}
\section{Floating-point numbers}
\cite{ayad10ijcar}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
......@@ -75,6 +75,10 @@ We gratefully thank all the people who contributed to this document:
\input{ide.tex}
\input{library.tex}
\input{whyml.tex}
\input{api.tex}
\input{manpages.tex}
......@@ -85,8 +89,8 @@ We gratefully thank all the people who contributed to this document:
\input{./apidoc.tex}
\bibliographystyle{abbrv}
\bibliography{manual}
%\bibliography{manual}
\input{biblio-demons}
\end{document}
......
\chapter{Why ML and Verification Condition Generator}
\label{chap:whyml}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
(* Why driver for SMT syntax *)
prelude ";;; this is a prelude for veriT"
printer "smtv1"
filename "%f-%t-%g.smt"
valid "^unsat"
unknown "^\\(unknown\\|sat\\)" "Unknown"
(* À discuter *)
transformation "simplify_recursive_definition"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
transformation "encoding_smt"
transformation "encoding_simple2"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax logic (=) "(= %1 %2)"
end
theory int.Int
prelude ";;; this is a prelude for integer arithmetic"
syntax logic zero "0"
syntax logic one "1"
syntax logic (+) "(+ %1 %2)"
syntax logic (-) "(- %1 %2)"
syntax logic (*) "(* %1 %2)"
syntax logic (-_) "(- %1)"
syntax logic (<=) "(<= %1 %2)"
syntax logic (<) "(< %1 %2)"
syntax logic (>=) "(>= %1 %2)"
syntax logic (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
remove prop CommutativeGroup.Unit_def
remove prop CommutativeGroup.Inv_def
remove prop Assoc.Assoc
remove prop Mul_distr
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
meta "encoding : kept" type int
end
theory real.Real
prelude ";;; this is a prelude for real arithmetic"
syntax logic zero "0.0"
syntax logic one "1.0"
syntax logic (+) "(+ %1 %2)"
syntax logic (-) "(- %1 %2)"
syntax logic (*) "(* %1 %2)"
syntax logic (/) "(/ %1 %2)"
syntax logic (-_) "(- %1)"
syntax logic inv "(/ 1.0 %1)"
syntax logic (<=) "(<= %1 %2)"
syntax logic (<) "(< %1 %2)"
syntax logic (>=) "(>= %1 %2)"
syntax logic (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
remove prop CommutativeGroup.Unit_def
remove prop CommutativeGroup.Inv_def
remove prop Inverse
remove prop Assoc.Assoc
remove prop Mul_distr
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
meta "encoding : kept" type real
end
(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
theory bool.Bool
syntax type bool "bool"
syntax logic True "true"
syntax logic False "false"
syntax logic andb "(and %1 %2)"
syntax logic orb "(or %1 %2)"
syntax logic xorb "(xor %1 %2)"
syntax logic notb "(not %1)"
meta cloned "encoding_decorate : kept" type bool
end
*)
theory int.EuclideanDivision
syntax logic div "(div %1 %2)"
syntax logic mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
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