Commit ccad1159 authored by MARCHE Claude's avatar MARCHE Claude

Polished doc, no more todo, no more overfull boxes

parent 089cbe8f
......@@ -1109,8 +1109,8 @@ ifeq (@enable_doc@,yes)
doc: doc/manual.pdf
# doc/manual.html
BNF = qualid label constant operator term type formula theory why_file \
typev expr module whyml_file
BNF = qualid label constant operator term type formula theory theory2 \
why_file typev expr expr2 module whyml_file
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
doc/%_bnf.tex: doc/%.bnf doc/bnf
......
......@@ -175,11 +175,11 @@ See manual Section xx
* Documentation
- traiter les \todo :
- DONE traiter les \todo :
install.tex:179:% \todo{que devient l'option -to-known-prover de why3session ?
manpages.tex:790:% \todo{A adapter en fonction de la decision sur l'upgrade de prover}
manpages.tex:809:\section{The \texttt{why3doc} tool} \todo{Documenter}
DONE install.tex:179:% \todo{que devient l'option -to-known-prover de why3session ?
DONE manpages.tex:790:% \todo{A adapter en fonction de la decision sur l'upgrade de prover}
DONE manpages.tex:809:\section{The \texttt{why3doc} tool} \todo{Documenter}
- (ANDREI) complete technical.tex: section "Drivers of external
......
......@@ -13,7 +13,8 @@
| "if" expr "then" expr ("else" expr)? ; conditional
| expr ";" expr ; sequence
| "loop" loop-annot "end" ; infinite loop
| "while" expr "do" loop-annot expr "done" ; while loop
| "while" expr ; while loop
"do" loop-annot expr "done" ;
| "for" lident "=" expr to-downto expr ; for loop
"do" loop-inv expr "done" ;
| assert annotation ; assertion
......@@ -27,7 +28,7 @@
("|" expr-case)+ "end" ;
| "(" expr ("," expr)+ ")" ; tuple
| "{|" field-value+ "|}" ; record
| exopr "." lqualid ; field access
| expr "." lqualid ; field access
| expr "." lqualid "<-" expr ; field assignment
| "{|" expr "with" field-value+ "|}" ; field update
| expr ":" type ; cast
......@@ -41,14 +42,4 @@
\
triple ::= expr ;
| pre expr post ; Hoare triple
\
assert ::= "assert" | "assume" | "check"
\
to-downto ::= "to" | "downto"
\
loop-annot ::= loop-inv? variant?
\
loop-inv ::= "invariant" annotation
\
variant ::= "variant" "{" term "}" ("with" lqualid)?
\end{syntax}
\begin{syntax}
assert ::= "assert" | "assume" | "check"
\
to-downto ::= "to" | "downto"
\
loop-annot ::= loop-inv? variant?
\
loop-inv ::= "invariant" annotation
\
variant ::= "variant" "{" term "}" ("with" lqualid)?
\end{syntax}
......@@ -3,9 +3,9 @@
| formula "->" formula ; implication
| formula "<->" formula ; equivalence
| formula "/\" formula ; conjunction
| formula "&&" formula ; asymmetric conjunction
| formula "&&" formula ; asymmetric conj.
| formula "\/" formula ; disjunction
| formula "||" formula ; asymmetric disjunction
| formula "||" formula ; asymmetric disj.
| "not" formula ; negation
| lqualid ; symbol
| prefix-op term ;
......
\newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
% \newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
\newcommand{\why}{\textsf{Why3}\xspace}
\newcommand{\whyml}{\textsf{Why3ML}\xspace}
......
......@@ -62,11 +62,11 @@
\vfill
\todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
% \todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
\begin{LARGE}
Version \whyversion{}, \todo{April} 2012
Version \whyversion{}, May 2012
\end{LARGE}
\vfill
......
......@@ -4,18 +4,22 @@
mdecl ::= decl ; theory declaration
| "type" mtype-decl ("with" mtype-decl)* ; mutable types
| "let" lident label* pgm-defn ;
| "let" "rec" recfun ("with" recfun)* ;
| "val" lident label* pgm-decl ;
| "let" "rec" recfun ("with" recfun)* ;
| "val" lident label* pgm-decl ;
| "exception" lident label* type? ;
| "use" imp-exp "module" tqualid ("as" uident-opt)? ;
| "namespace" "import"? uident-opt mdecl* "end" ;
| "use" imp-exp "module" tqualid ;
("as" uident-opt)? ;
| "namespace" "import"? uident-opt ;
mdecl* "end" ;
\
mtype-decl ::= lident label* ("'" lident label*)* mtype-defn;
mtype-decl ::= lident label* ("'" lident label*)* ;
mtype-defn ;
\
mtype-defn ::= ; abstract type
| "=" type ; alias type
| "=" "|"? type-case ("|" type-case)* ; algebraic type
| "=" "{|" mrecord-field (";" mrecord-field)* "|}" ; record type
mtype-defn ::= ; abstract type
| "=" type ; alias type
| "=" "|"? type-case ("|" type-case)* ; algebraic type
| "=" "{|" mrecord-field ; record type
(";" mrecord-field)* "|}" ;
\
mrecord-field ::= "mutable"? lident label* ":" type
\
......
......@@ -145,12 +145,18 @@ $A~\texttt{and}~B$ into subgoals $A$ and $B$, whereas it transforms
$A~\verb|&&|~B$ into subgoals $A$ and $A\rightarrow B$.
\paragraph{Theories.}
The syntax for theories is given Figure~\ref{fig:bnf:theory}.
The syntax for theories is given on Figure~\ref{fig:bnf:theorya} and~\ref{fig:bnf:theoryb}.
\begin{figure}
\begin{center}\framebox{\input{./theory_bnf.tex}}\end{center}
\caption{Syntax for theories.}
\label{fig:bnf:theory}
\caption{Syntax for theories (part 1).}
\label{fig:bnf:theorya}
\end{figure}
\begin{figure}
\begin{center}\framebox{\input{./theory2_bnf.tex}}\end{center}
\caption{Syntax for theories (part 2).}
\label{fig:bnf:theoryb}
\end{figure}
\paragraph{Files.}
......@@ -163,7 +169,7 @@ A \why input file is a (possibly empty) list of theories.
\section{Why3ML Language}\label{sec:syntax:whyml}
\paragraph{Types.}
The syntax for program types is given in figure~\ref{fig:bnf:typev}.
The syntax for program types is given in Figure~\ref{fig:bnf:typev}.
\begin{figure}
\begin{center}\framebox{\input{./typev_bnf.tex}}\end{center}
\caption{Syntax for program types.}
......@@ -171,15 +177,21 @@ The syntax for program types is given in figure~\ref{fig:bnf:typev}.
\end{figure}
\paragraph{Expressions.}
The syntax for program expressions is given in figure~\ref{fig:bnf:expr}.
The syntax for program expressions is given in Figure~\ref{fig:bnf:expra} and~Figure~\ref{fig:bnf:exprb}.
\begin{figure}
\begin{center}\framebox{\input{./expr_bnf.tex}}\end{center}
\caption{Syntax for program expressions.}
\label{fig:bnf:expr}
\caption{Syntax for program expressions (part1).}
\label{fig:bnf:expra}
\end{figure}
\begin{figure}
\begin{center}\framebox{\input{./expr2_bnf.tex}}\end{center}
\caption{Syntax for program expressions (part2).}
\label{fig:bnf:exprb}
\end{figure}
\paragraph{Modules.}
The syntax for modules is given in figure~\ref{fig:bnf:module}.
The syntax for modules is given in Figure~\ref{fig:bnf:module}.
\begin{figure}
\begin{center}\framebox{\input{./module_bnf.tex}}\end{center}
\caption{Syntax for modules.}
......
......@@ -13,17 +13,6 @@
| "clone" imp-exp tqualid ("as" uident-opt)? subst? ;
| "namespace" "import"? uident-opt decl* "end" ;
\
type-decl ::= lident label* ("'" lident label*)* type-defn;
\
type-defn ::= ; abstract type
| "=" type ; alias type
| "=" "|"? type-case ("|" type-case)* ; algebraic type
| "=" "{|" record-field (";" record-field)* "|}" ; record type
\
type-case ::= uident label* type-param*
\
record-field ::= lident label* ":" type
\
logic-decl ::= function-decl ;
| predicate-decl
\
......@@ -36,12 +25,6 @@
predicate-decl ::= lident label* type-param* ;
| lident label* type-param* "=" formula
\
type-param ::= "'" lident ;
| lqualid ;
| "(" lident+ ":" type ")" ;
| "(" type ("," type)* ")" ;
| "()"
\
inductive-decl ::= lident label* type-param* "=" ;
"|"? ind-case ("|" ind-case)* ;
\
......@@ -60,5 +43,7 @@
| "lemma" uqualid ;
| "goal" uqualid ;
\
tqualid ::= uident | ident ("." ident)* "." uident ; %
tqualid ::= uident | ident ("." ident)* "." uident ;
\
type-decl ::= lident label* ("'" lident label*)* type-defn; %
\end{syntax}
\begin{syntax}
type-defn ::= ; abstract type
| "=" type ; alias type
| "=" "|"? type-case ("|" type-case)* ; algebraic type
| "=" "{|" record-field (";" record-field)* "|}" ; record type
\
type-case ::= uident label* type-param*
\
record-field ::= lident label* ":" type
\
type-param ::= "'" lident ;
| lqualid ;
| "(" lident+ ":" type ")" ;
| "(" type ("," type)* ")" ;
| "()"
\end{syntax}
......@@ -518,7 +518,9 @@ the loop is reached, \texttt{True} is returned.
{ 0 <= pos < length board }
try
for q = 0 to pos - 1 do
invariant { forall j:int. 0 <= j < q -> consistent_row board pos j }
invariant {
forall j:int. 0 <= j < q -> consistent_row board pos j
}
let bq = board[q] in
let bpos = board[pos] in
if bq = bpos then raise (Inconsistent q);
......@@ -555,7 +557,9 @@ module NQueens
{ 0 <= pos < length board }
try
for q = 0 to pos - 1 do
invariant { forall j:int. 0 <= j < q -> consistent_row board pos j }
invariant {
forall j:int. 0 <= j < q -> consistent_row board pos j
}
let bq = board[q] in
let bpos = board[pos] in
if bq = bpos then raise (Inconsistent q);
......@@ -606,7 +610,8 @@ The backtracking code is a recursive function \verb|bt_queens| which
takes the chess board, its size, and the starting row for the search.
The termination is ensured by the obvious variant \texttt{n-pos}.
\begin{verbatim}
let rec bt_queens (board: array int) (n: int) (pos: int) variant {n-pos} =
let rec bt_queens (board: array int) (n: int) (pos: int)
variant {n-pos} =
\end{verbatim}
The precondition relates \texttt{board}, \texttt{pos}, and \texttt{n}
and requires \texttt{board} to be a solution up to \texttt{pos}:
......@@ -634,7 +639,8 @@ extend this prefix with a queen on row \texttt{pos} at a column below
invariant {
eq_board board (at board 'Init) pos /\
forall b:array int. length b = n -> is_board b n ->
eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) }
eq_board board b pos -> 0 <= b[pos] < i ->
not (solution b n) }
\end{verbatim}
Then we assign column \texttt{i} to the queen on row \texttt{pos} and
we check for a possible attack with \verb|check_is_consistent|. If
......@@ -664,7 +670,8 @@ search on row 0. The postcondition is also twofold, as for
let queens (board: array int) (n: int) =
{ 0 <= length board = n }
bt_queens board n 0
{ forall b:array int. length b = n -> is_board b n -> not (solution b n) }
{ forall b:array int. length b = n -> is_board b n ->
not (solution b n) }
| Solution -> { solution board n }
\end{verbatim}
This second part of the solution is given Figure~\ref{fig:NQueens2}.
......@@ -686,7 +693,8 @@ automatically, including the verification of the lemmas themselves.
exception Solution
let rec bt_queens (board: array int) (n: int) (pos: int) variant { n - pos } =
let rec bt_queens (board: array int) (n: int) (pos: int)
variant { n - pos } =
{ length board = n /\ 0 <= pos <= n /\ solution board pos }
'Init:
if pos = n then raise Solution;
......@@ -709,7 +717,8 @@ automatically, including the verification of the lemmas themselves.
let queens (board: array int) (n: int) =
{ 0 <= length board = n }
bt_queens board n 0
{ forall b:array int. length b = n -> is_board b n -> not (solution b n) }
{ forall b:array int. length b = n -> is_board b n ->
not (solution b n) }
| Solution -> { solution board n }
end
\end{verbatim}
......@@ -854,8 +863,7 @@ module AmortizedQueue
predicate inv (q: queue 'a) =
length q.front = q.lenf >= length q.rear = q.lenr
function sequence (q: queue 'a) : list 'a =
q.front ++ reverse q.rear
function sequence (q: queue 'a) : list 'a = q.front ++ reverse q.rear
let 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