Select Git revision
Forked from
Per Lindgren / D7050E
Source project has a limited visibility.
syntaxref.tex 28.84 KiB
\chapter{Language Reference}
\label{chap:syntaxref}
%HEVEA\cutname{syntaxref.html}
In this chapter, we describe the syntax and semantics of \whyml.
This chapter is not yet fully updated to the new syntax of \why 1.00, so it not distributed for the moment.
\endinput
\section{Lexical Conventions}
\label{sec:lexer}
%Lexical conventions of \whyml are similar to those of OCaml.
%
Blank characters are space, horizontal tab, carriage return,
and line feed. Blanks separate lexemes but are otherwise ignored.
%
Comments are enclosed by \texttt{(*} and \texttt{*)} and can be nested.
Note that \texttt{(*)} does not start a comment.
Strings are enclosed in double quotes (\verb!"!). Double quotes can be
escaped inside strings using the backslash character (\verb!\!).
The other special sequences are \verb!\n! for line feed and \verb!\t!
for horizontal tab.
In the following, strings are referred to with the non-terminal
\nonterm{string}{}\spacefalse.
%\subsection{Constants}
The syntax for numerical constants is given by the following rules:
%\begin{figure}[ht]
\begin{center}\input{./generated/constant_bnf.tex}\end{center}
%\caption{Syntax for numerical constants.}
%\label{fig:bnf:constant}
%\end{figure}
%in Figure~\ref{fig:bnf:constant}.
Integer and real constants have arbitrary precision.
Integer constants can be given in base 10, 16, 8 or 2.
Real constants can be given in base 10 or 16.
Notice that the exponent in hexadecimal real constants is written in base 10.
%\subsection{Identifiers}
Identifiers are composed of letters, digits, the underscore character,
and the quote character. %, as shown in Figure~\ref{fig:bnf:ident}.
The syntax distinguishes identifiers that start with a lowercase letter
or an underscore (\nonterm{lident}{}\spacefalse) and identifiers that
start with an uppercase letter (\nonterm{uident}{}\spacefalse):
%\begin{figure}[ht]
\begin{center}\input{./generated/ident_bnf.tex}\end{center}
%\caption{Syntax for identifiers.}
%\label{fig:bnf:ident}
%\end{figure}
Identifiers that contain a quote followed by a letter,
such as \texttt{int32'max}, are reserved for symbols
introduced by \why transformations and cannot be used
for user-defined symbols.
%\subsection{Operators}
Prefix and infix operators are built from characters organized in four
precedence groups (\textsl{op-char-1} to \textsl{op-char-4}):
%as shown in Figure~\ref{fig:bnf:operator}.
%\begin{figure}[ht]
\begin{center}\input{./generated/operator_bnf.tex}\end{center}
%\caption{Syntax for operators.}
%\label{fig:bnf:operator}
%\end{figure}
The infix operators from a high-numbered group bind stronger
than the infix operators from a low-numbered group,
and prefix operators bind stronger than infix operators.
For example, the infix operator \texttt{.*.} (from \textsl{infix-op-3})would have a higher precedence than the infix operator \texttt{->-}
(from \textsl{infix-op-1}).
The so-called ``bang operators'' are prefix operators that have even
higher precedence than the juxtaposition (application) operator,
allowing us to write expressions like \texttt{inv !x}.
An operator from \textsl{infix-op-4} or \textsl{prefix-op}
cannot start with \texttt{!} or \texttt{?}: such operators
are always recognized as bang operators.
%Infix operators from groups 2-4 are left-associative.
%Infix operators from group 1 are non-associative and
%may instead be chained, as explained in Section~\ref{sec:terms}.
%An operator inside parenthesis can act as a lowercase identifier.
%Qualified identifiers are prefixed with a sequence of uppercase
%identifiers, e.g., \texttt{App.S.get}:
%\begin{figure}[ht]
%\begin{center}\input{./generated/qualid_bnf.tex}\end{center}
%\caption{Syntax for qualified identifiers.}
%\label{fig:bnf:qualid}
%\end{figure}
Finally, any identifier, term, formula, or expression
in a \whyml source can be tagged either with a string
\textit{attribute} or a location:
\begin{center}\input{./generated/attribute_bnf.tex}\end{center}
An attribute cannot contain newlines or closing square brackets;
leading and trailing spaces are ignored.
A location consists of a file name in double quotes,
a line number, and starting and ending character positions.
\section{Type expressions}
\label{sec:types}
\whyml features an ML-style type system with polymorphic types,
variants (sum types), and records that can have mutable fields.
The syntax for type expressions is the following:
\begin{center}\input{./generated/type_bnf.tex}\end{center}
Built-in types are \texttt{int} (arbitrary precision integers),
\texttt{real} (real numbers), \texttt{bool}, the arrow type
(also called the \textit{mapping type}, right-associative),
and the tuple types.
The empty tuple type is also called the \textit{unit type}
and can be written as \texttt{unit}.
Note that the syntax for type expressions notably differs from
the usual ML syntax. In particular, the type of polymorphic lists
is written \texttt{list 'a}, and not \texttt{'a list}.
\textit{Snapshot types} are specific to \whyml, they denote
the types of ghost values produced by pure logical functions in
\whyml programs. A snapshot of an immutable type is the type
itself: thus, \texttt{\{int\}} is the same as \texttt{int} and
\texttt{\{list 'a\}} is the same as \texttt{list 'a}.
A snapshot of a mutable type, however, represents a snapshot
value which cannot be modified anymore. Thus, a snapshot array
\texttt{a} of type \texttt{\{array int\}} can be read from
(\texttt{a[42]} is accepted) but not written into
(\texttt{a[42] <- 0} is rejected). Generally speaking,
a program function that expects an argument of a mutable type
will accept an argument of the corresponding snapshot type
as long as it is not modified by the function.
\section{Logical expressions: terms and formulas}
\label{sec:terms}
A significant part of a typical \whyml source file is occupied
by non-executable logical content intended for specification
and proof: function contracts, assertions, definitions of
logical functions and predicates, axioms, lemmas, etc.
Logical expressions are called \textit{terms}. Boolean
terms are called \textit{formulas}. Internally, \why distinguishes
the proper formulas (produced by predicate symbols, propositional
connectives and quantifiers) and the terms of type \texttt{bool}
(produced by Boolean variables and logical functions that return
\texttt{bool}). However, this distinction is not enforced on the
syntactical level, and \why will perform the necessary conversions
behind the scenes.
\begin{figure}[p!]
\begin{center}\input{./generated/term1_bnf.tex}\end{center}
\caption{\whyml terms (part I).}
\label{fig:bnf:term1}
\end{figure}
\begin{figure}[ht]
\begin{center}\input{./generated/term2_bnf.tex}\end{center}
\caption{\whyml terms (part II).}
\label{fig:bnf:term2}
\end{figure}
\begin{figure}[ht]
\begin{center}\input{./generated/term3_bnf.tex}\end{center}
\caption{\whyml terms (part III).}
\label{fig:bnf:term3}
\end{figure}
The syntax of \whyml terms is given in
Figures~\ref{fig:bnf:term1}-\ref{fig:bnf:term3}.
The constructions are listed in the order of
decreasing precedence.
For example, as was mentioned above,
bang operators have the highest precedence of all operators,
so that \texttt{-p.x} denotes the negation of the
record field \texttt{p.x}, whereas \texttt{!p.x}
denotes the field \texttt{x} of a record stored
in the reference \texttt{p}.
An operator inside parentheses can act as an identifier
referring to that operator, for example, in a definition.
To distinguish between prefix and infix operators, an
underscore symbol is appended at the end: for example,
\texttt{(-)} refers to the binary subtraction and
\texttt{(-\_)} to the unary negation.
Bang operators cannot be used as infix operators,
and thus do not require disambiguation.
In addition to prefix and infix operators, \whyml
supports several mixfix bracket operators to
manipulate various collection types: dictionaries,
arrays, sequences, etc. Bracket operators do not have
any predefined meaning and may be used to denote access
and update operations for various user-defined collection types.
Notice that the in-place update operator (\texttt{a[i] <- v})
cannot be used inside logical terms: all effectful operations
are restricted to program expressions. To represent the result
of a collection update, we should use a pure logical update
operator (\texttt{a[i <- v]}) instead.
The \texttt{at} and \texttt{old} operators are used inside
postconditions and assertions to refer to the value of
a mutable program variable at some past moment of execution
(see the next section for details).
These operators have higher precedence than the infix
operators from group 1 (\textsl{infix-op-1}): \texttt{old i > j}
is parsed as \texttt{(old i) > j} and not as \texttt{old (i > j)}.
Infix operators from groups 2-4 are left-associative.
Infix operators from group 1 are non-associative and
can be chained. For example, the term \texttt{0 <= i < j < length a}is parsed as the conjunction of three inequalities \texttt{0 <= i},
\texttt{i < j}, and \texttt{j < length a}.
In order to refer to symbols introduced in different namespaces
(\textit{scopes}), we can put a dot-separated
``qualifier prefix'' in front of an identifier
(e.g.~\texttt{Map.S.get m i}) or in front of a term in parentheses
(e.g.~\texttt{Map.S.(m[i])}, though parentheses can be omitted
if the term is a record or a record update). This notation allows
us to use the symbol \texttt{get} or the collection access operator
\texttt{([])} from the scope \texttt{Map.S} without importing
them in the current namespace.
The propositional connectives in \whyml formulas are listed in
Figure~\ref{fig:bnf:term2}. The non-standard connectives ---
asymmetric conjunction (\texttt{\&\&}), asymmetric disjunction
(\texttt{||}), proof indication (\texttt{by}), and consequence
indication (\texttt{so}) --- are used to control the goal-splitting
transformations of \why and provide integrated proofs for
\whyml assertions, postconditions, lemmas, etc.
The semantics of these connectives
follows the rules below:
\begin{itemize}
\item A proof of \texttt{A \&\& B} is split into
separate proofs of \texttt{A} and \texttt{A -> B}.
If \texttt{A \&\& B} occurs as a premise, it behaves
as a normal conjunction.
\item A case analysis over \texttt{A || B} is split into
disjoint cases \texttt{A} and \texttt{not A {/\char92} B}.
If \texttt{A || B} occurs as a goal, it behaves
as a normal disjunction.
\item An occurrence of \texttt{A by B} generates a side condition
\texttt{B -> A} (the proof justifies the conclusion).
When \texttt{A by B} occurs as a premise,
it is reduced to \texttt{A} (the proof is discarded).
When \texttt{A by B} occurs as a goal,
it is reduced to \texttt{B} (the proof is verified).
\item An occurrence of \texttt{A so B} generates a side condition
\texttt{A -> B} (the premise justifies the consequence).
When \texttt{A so B} occurs as a premise,
it behaves as a conjunction \texttt{A {/\char92} B}
(we use both the premise and the consequence).
When \texttt{A so B} occurs as a goal,
it is reduced to \texttt{A} (the premise is verified).
\end{itemize}
For example, full splitting of the goal
\texttt{(A by (exists x. B so C)) \&\& D}
produces four subgoals:
\texttt{exists x. B} (the premise is verified),
\texttt{forall x. B -> C} (the premise justifies the consequence),
\texttt{(exists x. B {/\char92} C) -> A} (the proof justifies the conclusion),
and finally, \texttt{A -> D} (the proof of \texttt{A} is discarded
and \texttt{A} is used to prove \texttt{D}).
%Figure~\ref{fig:byso} contains more examples of usage of
%\texttt{\&\&}, \texttt{||}, \texttt{by}, and \texttt{so}.
%\begin{figure}[ht]
%\begin{center}
%\begin{tabular}{c|c}
%\multicolumn{1}{c|}{Initial goal} &
%\multicolumn{1}{c}{Goals after full splitting} \\
%\hline
%\texttt{A -> (B {/\char92} C)} & \texttt{A -> B}, \:\: \texttt{A -> C} \\
%\texttt{(A {\char92/} B) -> C} & \texttt{A -> C}, \:\: \texttt{B -> C} \\[1ex]
%\texttt{A -> (B {\&\&} C)} & \texttt{A -> B}, \:\: \texttt{A -> (B -> C)} \\
%\texttt{(A || B) -> C} & \texttt{A -> C}, \:\: \texttt{(not A {/\char92} B) -> C} \\[1ex]
%\texttt{A -> (B by C)} & \texttt{A -> C}, \:\: \texttt{A -> (C -> B)} \\
%\texttt{(A so B) -> C} & \texttt{A -> B}, \:\: \texttt{(A {/\char92} B) -> C} \\[1ex]
%\texttt{A by (B by C)} & \texttt{C}, \:\:
% \texttt{C -> B}, \:\: \texttt{B -> A} \\%\texttt{A by (B so C)} & \texttt{B}, \:\:
% \texttt{B -> C}, \:\: \texttt{(B {/\char92} C) -> A} \\
%\end{tabular}
%\end{center}
%\caption{Non-standard propositional connectives.}
%\label{fig:byso}
%\end{figure}
The behaviour of the splitting transformations is further
controlled by attributes \texttt{[@stop\_split]} and
\texttt{[@case\_split]}. Consult Section~\ref{tech:trans:split}
for details.
Among the propositional connectives,
\texttt{not} has the highest precedence,
\texttt{\&\&} has the same precedence as \texttt{/\char92}
(weaker than negation),
\texttt{||} has the same precedence as \texttt{\char92/}
(weaker than conjunction),
\texttt{by}, \texttt{so}, \texttt{->}, and \texttt{<->}
all have the same precedence (weaker than disjunction).
All binary connectives except equivalence are right-associative.
Equivalence is non-associative and is chained instead:
\texttt{A <-> B <-> C} is transformed into a conjunction
of \texttt{A <-> B} and \texttt{B <-> C}.
To reduce ambiguity, \whyml forbids to place
a non-parenthesised implication at the right-hand side
of an equivalence: \texttt{A <-> B -> C} is rejected.
\newpage
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{The \why Language}
\subsection{Terms}
The syntax for terms is given in Figure~\ref{fig:bnf:term1}.
The various constructs have the following priorities and
associativities, from lowest to greatest priority:
\begin{center}
\begin{tabular}{|l|l|}
\hline
construct & associativity \\
\hline\hline
\texttt{if then else} / \texttt{let in} & -- \\
label & -- \\
cast & -- \\
infix-op level 1 & left \\
infix-op level 2 & left \\
infix-op level 3 & left \\
infix-op level 4 & left \\
prefix-op & -- \\
function application & left \\
brackets / ternary brackets & -- \\
bang-op & -- \\
\hline
\end{tabular}
\end{center}
Note the curryfied syntax for function application, though partial
application is not allowed (rejected at typing).
\subsection{Formulas}
The syntax for formulas is given Figure~\ref{fig:bnf:formula}.
The various constructs have the following priorities and
associativities, from lowest to greatest priority:
\begin{center}
\begin{tabular}{|l|l|} \hline
construct & associativity \\
\hline\hline
\texttt{if then else} / \texttt{let in} & -- \\
label & -- \\
\texttt{->} / \texttt{<->} & right \\
\texttt{by} / \texttt{so} & right \\
\verb!\/! / \verb!||! & right \\
\verb|/\| / \verb!&&! & right \\
\texttt{not} & -- \\
infix level 1 & left \\
infix level 2 & left \\
infix level 3 & left \\
infix level 4 & left \\
prefix & -- \\
\hline
\end{tabular}
\end{center}
Note that infix symbols of level 1 include equality (\texttt{=}) and
disequality (\texttt{<>}).
\begin{figure}
\begin{center}\framebox{\input{./generated/formula_bnf.tex}}\end{center}
\caption{Syntax for formulas.}
\label{fig:bnf:formula}
\end{figure}
Notice that there are two symbols for the conjunction: \verb|/\|
and \verb|&&|, and similarly for disjunction. They are logically
equivalent, but may be treated slightly differently by some
transformations. For instance, \texttt{split} transforms the goal
\verb|A /\ B| into subgoals \verb|A| and \verb|B|, whereas it transforms
\verb|A && B| into subgoals \verb|A| and \verb|A -> B|. Similarly, it
transforms \verb!not (A || B)! into subgoals \verb|not A| and
\verb|not ((not A) /\ B)|.
The \texttt{by}/\texttt{so} connectives are proof indications. They are
logically equivalent to their first argument, but may affect the result
of some transformations. For instance, the \texttt{split\_goal}
transformations interpret those connectives as introduction of logical cuts
(see~\ref{tech:trans:split} for details).
\subsection{Theories}
The syntax for theories is given on Figure~\ref{fig:bnf:theorya} and~\ref{fig:bnf:theoryb}.
\begin{figure}
\begin{center}\framebox{\input{./generated/theory_bnf.tex}}\end{center}
\caption{Syntax for theories (part 1).}
\label{fig:bnf:theorya}
\end{figure}
\begin{figure}
\begin{center}\framebox{\input{./generated/theory2_bnf.tex}}\end{center}
\caption{Syntax for theories (part 2).}
\label{fig:bnf:theoryb}
\end{figure}
\subsubsection{Algebraic types}
TO BE COMPLETED
\subsubsection{Record types}
TO BE COMPLETED
\subsubsection{Range types}
\label{sec:rangetypes}
A declaration of the form \texttt{type r = < range \textit{a b} >}
defines a type that projects into the integer range\texttt{[\textit{a,b}]}. Note that in order to make such a declaration
the theory \texttt{int.Int} must be imported.
Why3 let you cast an integer literal in a range type
(e.g. \texttt{(42:r)}) and will check at typing that the literal is in
range. Defining such a range type $r$ automatically introduces the
following:
\begin{whycode}
function r'int r : int
constant r'maxInt : int
constant r'minInt : int
\end{whycode}
The function \texttt{r'int} projects a term of type \texttt{r} to its
integer value. The two constants represent the high bound and low
bound of the range respectively.
Unless specified otherwise with the meta \texttt{"keep:literal"} on
\texttt{r}, the transformation \emph{eliminate\_literal} introduces an
axiom
\begin{whycode}
axiom r'axiom : forall i:r. r'minInt <= r'int i <= r'maxInt
\end{whycode}
and replaces all casts of the form \texttt{(42:r)} with a constant and
an axiom as in:
\begin{whycode}
constant rliteral7 : r
axiom rliteral7_axiom : r'int rliteral7 = 42
\end{whycode}
This type is used in the standard library in the theories
\texttt{bv.BV8}, \texttt{bv.BV16}, \texttt{bv.BV32}, \texttt{bv.BV64}.
\subsubsection{Floating-point Types}
A declaration of the form \texttt{type f = < float \textit{eb sb} >}
defines a type of floating-point numbers as specified by the IEEE-754
standard~\cite{ieee754-2008}. Here the literal \texttt{\textit{eb}}
represents the number of bits in the exponent and the literal
\texttt{\textit{sb}} the number of bits in the significand (including
the hidden bit). Note that in order to make such a declaration the
theory \texttt{real.Real} must be imported.
Why3 let you cast a real literal in a float type
(e.g. \texttt{(0.5:f)}) and will check at typing that the literal is
representable in the format. Note that Why3 do not implicitly round a
real literal when casting to a float type, it refuses the cast if the
literal is not representable.
Defining such a type \texttt{f} automatically introduces the following:
\begin{whycode}
predicate f'isFinite f
function f'real f : real
constant f'eb : int
constant f'sb : int
\end{whycode}
As specified by the IEEE standard, float formats includes infinite
values and also a special NaN value (Not-a-Number) to represent
results of undefined operations such as $0/0$. The predicate
\texttt{f'isFinite} indicates whether its argument is neither infinite
nor NaN. The function \texttt{f'real} projects a finite term of type
\texttt{f} to its real value, its result is not specified for non finite
terms.
Unless specified otherwise with the meta \texttt{"keep:literal"} on
\texttt{f}, the transformation \emph{eliminate\_literal} will
introduce an axiom
\begin{whycode}
axiom f'axiom :
forall x:f. f'isFinite x -> -. max_real <=. f'real x <=. max_real\end{whycode}
where \texttt{max\_real} is the value of the biggest finite float in
the specified format. The transformation also replaces all casts of
the form \texttt{(0.5:f)} with a constant and an axiom as in:
\begin{whycode}
constant fliteral42 : f
axiom fliteral42_axiom : f'real fliteral42 = 0.5 /\ f'isFinite fliteral42
\end{whycode}
This type is used in the standard library in the theories
\texttt{ieee\_float.Float32} and \texttt{ieee\_float.Float64}.
\subsection{Files}
A \why input file is a (possibly empty) list of theories.
\begin{center}\framebox{\input{./generated/why_file_bnf.tex}}\end{center}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\clearpage
\section{The \whyml Language}\label{sec:syntax:whyml}
\subsection{Specification}
The syntax for specification clauses in programs
is given in Figure~\ref{fig:bnf:spec}.
\begin{figure}
\begin{center}\framebox{\input{./generated/spec_bnf.tex}}\end{center}
\caption{Specification clauses in programs.}
\label{fig:bnf:spec}
\end{figure}
Within specifications, terms are extended with new constructs
\verb|old| and \verb|at|:
\begin{center}\framebox{\input{./generated/term_old_at_bnf.tex}}\end{center}
Within a postcondition, $\verb|old|~t$ refers to the value of term $t$
in the prestate. Within the scope of a code mark $L$,
the term $\verb|at|~t~\verb|'|L$ refers to the value of term $t$ at the program
point corresponding to $L$.
\subsection{Expressions}
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{./generated/expr_bnf.tex}}\end{center}
\caption{Syntax for program expressions (part 1).}
\label{fig:bnf:expra}
\end{figure}
\begin{figure}
\begin{center}\framebox{\input{./generated/expr2_bnf.tex}}\end{center}
\caption{Syntax for program expressions (part 2).}
\label{fig:bnf:exprb}
\end{figure}
In applications, arguments are evaluated from right to left.
This includes applications of infix operators, with the only exception of
lazy operators \verb|&&| and \verb+||+ that evaluate from left to
right, lazily.
% In the following we describe the informal semantics of each
% constructs, and provide the corresponding rule for computing the
% weakest precondition.
% \subsubsection{Constant Expressions, Unary and Binary Operators}
% Integer and real constants are as in the logic language, as weel as the unary and binary operators.
% \subsubsection{Array accesses and updates, fields access and updates}
% \todo{}
% \subsubsection{Let binding, sequences}
% \todo{}
% \subsubsection{Function definition}
% \todo{fun, let rec}
% \subsubsection{Function call}
% \todo{}
% \subsubsection{Exception throwing and catching}
% \todo{raise, try with end}
% \subsubsection{Conditional expression, pattern matching}
% \todo{if then else. Discuss standard WP versus fast WP}
% \subsubsection{Iteration Expressions}
% There are three kind of expressions for iterating: bounded, unbounded and infinite.
% \begin{itemize}
% \item A bounded iteration has the form
% \begin{flushleft}\ttfamily
% for $i$=$a$ to $b$ do invariant \{ $I$ \} $e$ done
% \end{flushleft}
% Expressions $a$ and $b$ are evaluated first and only once, then expression $e$ si evaluated successively for $i$ from $a$ to $b$ included. Nothing is executed if $a > b$. The invariant $I$ must hold at each iteration including before entering the loop and when leaving it. The rule for computing WP is as follows:
% \begin{eqnarray*}
% WP(\texttt{for} \ldots, Q) &=& I(a) \land \\
% && \forall \vec{w} (\forall i, a \leq i \leq b \land I(i) \rightarrow WP(e,I(i+1))) \land (I(b+1) \rightarrow Q)
% \end{eqnarray*}
% where $\vec{w}$ is the set of references modified by $e$.
% A downward bounded iteration is also available, under the form
% \begin{flushleft}\ttfamily
% for $i$=$a$ downto $b$ do invariant \{ $I$ \} $e$ done
% \end{flushleft}
% \item An unbounded iteration has the form
% \begin{flushleft}\ttfamily
% while $c$ do invariant \{ $I$ \} $e$ done
% \end{flushleft}
% it iterates the loop body $e$ until the condition $c$ becomes false.
% \begin{eqnarray*}
% WP(\texttt{while} \ldots, Q) &=& I \land \\
% && \forall \vec{w} (c \land I \rightarrow WP(e,I)) \land (\neg c \land I \rightarrow Q)
% \end{eqnarray*}
% where $\vec{w}$ is the set of references modified by $e$.
% Additionally, such a loop can be given a variant $v$, a quantity that must decreases ar each iteration, so as to prove its termination.
% \item An infinite iteration has the form
% \begin{flushleft}\ttfamily
% loop invariant \{ $I$ \} $e$ end
% \end{flushleft}
% it iterates the loop forever, hence the only way to exit such a loop is to raise an exception.
% \begin{eqnarray*}
% WP(\texttt{loop} \ldots, Q \mid Exc \Rightarrow R) &=& I \land \\
% && \forall \vec{w} (I \rightarrow WP(e,I)) \land (I \rightarrow WP(e,Exc \Rightarrow R))
% \end{eqnarray*}% \end{itemize}
% \subsubsection{Assertions, Code Contracts}
% There are several form of expressions for inserting annotations in the code.
% The first form of those are the \emph{assertions} which have the form
% \begin{flushleft}\ttfamily
% \textsl{keyword} \{ \textsl{proposition} \}
% \end{flushleft}
% where \textsl{keyword} is either \texttt{assert}, \texttt{assume} or
% \texttt{check}. They all state that the given proposition holds at the given program point. The differences are:
% \begin{itemize}
% \item \texttt{assert} requires to prove that the proposition holds, and then make it available in the context of the remaining of the code
% \item \texttt{check} requires to prove that the proposition holds, but
% does not make it visible in the remaining
% \item \texttt{assume} assumes that the proposition holds and make it
% visible in the context of the remaining code, without requiring to
% prove it. It acts like an axiom, but within a program.
% \end{itemize}
% The corresponding rules for computing WP are as follows:
% \begin{eqnarray*}
% WP(\texttt{assert} \{ P \}, Q) &=& P \mathop{\&\&} Q = P \land (P \rightarrow Q)\\
% WP(\texttt{check} \{ P \}, Q) &=& P \land Q \\
% WP(\texttt{assume} \{ P \}, Q) &=& P \rightarrow Q
% \end{eqnarray*}
% The other forms of code contracts allow to abstract a piece of code by specifications.
% \begin{itemize}
% \item $\texttt{any}~\{ P \}~\tau~\epsilon~\{ Q \}$ is a
% non-deterministic expression that requires the precondition $P$ to
% hold, then makes some side effects $\epsilon$, and returns any value
% of type $\tau$ such that $Q$ holds. This construct acts as an axiom
% in the sense that it does not check whether there exists any program
% that can effectively establish the post-condition (similarly as the
% introduction of a \texttt{val} at the global level).
% \item $\texttt{abstract}~e~\{ Q \}$ makes sure that the evaluation of
% expression $e$ establishes the post-condition $Q$, and then abstract
% away the program state by the post-condition $Q$ (similarly to the
% \texttt{any} construct).
% \end{itemize}
% The corresponding rules for computing WP are as follows:
% \[
% \begin{array}{l}
% WP(\texttt{any}~\{ P \}~\tau~\epsilon~\{ Q \mid exn_i \Rightarrow R_i \} ,
% Q' exn_i \Rightarrow R'_i) = \\
% \qquad\qquad P \mathop{\&\&} \forall result, \epsilon.
% (Q \rightarrow Q') \land (R_i \rightarrow R'_i) \\
% WP(\texttt{abstract}~e~\{ Q \mid exn_i \Rightarrow R_i \} ,
% Q' \mid exn_i \Rightarrow R'_i) = \\
% \qquad\qquad WP(e,Q \mid exn_i \Rightarrow R_i) \land
% \forall result, \epsilon, Q \rightarrow Q' \land R_i \rightarrow R'_i
% \end{array}
% \]
% \subsubsection{Labels, Operators \texttt{old} and \texttt{at}}
% \todo{Labels, old, at}
\subsection{Modules}
The syntax for modules is given in Figure~\ref{fig:bnf:module}.
\begin{figure}
\begin{center}\framebox{\input{./generated/module_bnf.tex}}\end{center}
\caption{Syntax for modules.}
\label{fig:bnf:module}
\end{figure}
Any declaration which is accepted in a theory is also accepted in a
module. Additionally, modules can introduce record types with mutable
fields and declarations which are specific to programs (global
variables, functions, exceptions).
\subsection{Files}
A \whyml input file is a (possibly empty) list of theories and modules.
\begin{center}\framebox{\input{./generated/whyml_file_bnf.tex}}\end{center}
A theory defined in a \whyml file can only be used within that
file. If a theory is supposed to be reused from other files, be they
\why or \whyml files, it should be defined in a \why file.
\section{The \why Standard Library}
\label{sec:library}\index{standard library}\index{library}
The \why standard library provides general-purpose
modules, to be used in logic and/or programs.
It can be browsed on-line at \url{http://why3.lri.fr/stdlib/}.
Each file contains one or several modules.
To \texttt{use} or \texttt{clone} a module \texttt{M} from file
\texttt{file}, use the syntax \texttt{file.M}, since \texttt{file} is
available in \why's default load path. For instance, the module of
integers and the module of references are imported as follows:
\begin{whycode}
use import int.Int
use import ref.Ref
\end{whycode}
A sub-directory \texttt{mach/} provides various modules to model
machine arithmetic.
For instance, the module of 63-bit integers and the module of arrays
indexed by 63-bit integers are imported as follows:
\begin{whycode}
use import mach.int.Int63
use import mach.array.Array63
\end{whycode}
In particular, the types and operations from these modules are mapped
to native OCaml's types and operations when \why code is extracted to
OCaml (see Section~\ref{sec:extract}).
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: