syntaxref.tex 13.3 KB
Newer Older
1
\chapter{Language Reference}
MARCHE Claude's avatar
MARCHE Claude committed
2
3
\label{chap:syntaxref}

4
This chapter gives the grammar and semantics for \why and \whyml input files.
5
6
7

\section{Lexical conventions}

MARCHE Claude's avatar
MARCHE Claude committed
8
Lexical conventions are common to \why and \whyml.
MARCHE Claude's avatar
MARCHE Claude committed
9

10
11
12
13
14
15
% TODO: blanks

\paragraph{Comments.}
Comments are enclosed by \texttt{(*} and \texttt{*)} and can be nested.

\paragraph{Strings.}
16
Strings are enclosed in double quotes (\verb!"!). Double quotes can be
MARCHE Claude's avatar
MARCHE Claude committed
17
inserted in strings using the backslash character (\verb!\!).
18
19
In the following, strings are referred to with the non-terminal
\nonterm{string}{}.
20
21

% TODO: escape sequences for strings
22

23
\paragraph{Identifiers.} The syntax distinguishes lowercase and
24
uppercase identifiers and, similarly, lowercase and uppercase
25
qualified identifiers.
26

27
28
\begin{center}\framebox{\input{./qualid_bnf.tex}}\end{center}

29
\paragraph{Constants.}
30
The syntax for constants is given in Figure~\ref{fig:bnf:constant}.
31
32
33
Integer and real constants have arbitrary precision.
Integer constants may be given in base 16, 10, 8 or 2.
Real constants may be given in base 16 or 10.
34

MARCHE Claude's avatar
MARCHE Claude committed
35
\begin{figure}
36
37
38
39
40
\begin{center}\framebox{\input{./constant_bnf.tex}}\end{center}
  \caption{Syntax for constants.}
\label{fig:bnf:constant}
\end{figure}

41
\paragraph{Operators.}
42
43
44
45
46
Prefix and infix operators are built from characters organized in four
categories (\textsl{op-char-1} to \textsl{op-char-4}).
\begin{center}\framebox{\input{./operator_bnf.tex}}\end{center}
Infix operators are classified into 4 categories, according to the
characters they are built from:
47
\begin{itemize}
48
\item level 4: operators containing only characters from
49
\textit{op-char-4};
50
\item level 3: those containing
51
 characters from \textit{op-char-3} or \textit{op-char-4};
52
\item level 2: those containing
53
 characters from \textit{op-char-2}, \textit{op-char-3} or
54
 \textit{op-char-4};
55
\item level 1: all other operators (non-terminal \textit{infix-op-1}).
56
57
\end{itemize}

58
59
60
61
62
63
\paragraph{Labels.} Identifiers, terms, formulas, program expressions
can all be labeled, either with a string, or with a location tag.
\begin{center}\framebox{\input{./label_bnf.tex}}\end{center}
A location tag consists of a file name, a line number, and starting
and ending characters.

64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
MARCHE Claude's avatar
MARCHE Claude committed
65

66
67
\section{Why3 Language}

68
\paragraph{Terms.}
69
The syntax for terms is given in Figure~\ref{fig:bnf:term}.
70
71
72
73
74
75
76
77
78
79
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  & -- \\
80
81
82
83
84
85
86
87
    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       & --   \\
88
89
90
91
    \hline
  \end{tabular}
\end{center}

92
93
Note the curryfied syntax for function application, though partial
application is not allowed (rejected at typing).
94

MARCHE Claude's avatar
MARCHE Claude committed
95
\begin{figure}
96
  \begin{center}\framebox{\input{./term_bnf.tex}}\end{center}
97
  \caption{Syntax for terms.}
98
99
100
\label{fig:bnf:term}
\end{figure}

101
\paragraph{Type Expressions.} The syntax for type expressions is the following:
102
\begin{center}\framebox{\input{./type_bnf.tex}}\end{center}
103
104
105
106
Built-in types are \texttt{int}, \texttt{real}, and tuple types.
Note that the syntax for type
expressions notably differs from the usual ML syntax (\emph{e.g.} the
type of polymorphic lists is written \texttt{list 'a}, not \texttt{'a list}).
107

108
\paragraph{Formulas.}
109
The syntax for formulas is given Figure~\ref{fig:bnf:formula}.
110
111
112
113
114
115
116
117
118
119
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 \\
120
121
    \verb!\/! / \verb!||! & right \\
    \verb|/\| / \verb!&&! & right \\
122
123
124
125
126
127
128
129
130
131
132
    \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{<>}).
133

MARCHE Claude's avatar
MARCHE Claude committed
134
\begin{figure}
135
  \begin{center}\framebox{\input{./formula_bnf.tex}}\end{center}
136
  \caption{Syntax for formulas.}
137
138
\label{fig:bnf:formula}
\end{figure}
MARCHE Claude's avatar
MARCHE Claude committed
139

140
141
Notice that there are two symbols for the conjunction: \verb|/\|
and \verb|&&|, and similarly for disjunction. They are logically
MARCHE Claude's avatar
MARCHE Claude committed
142
equivalent, but may be treated slightly differently by some
143
144
145
146
147
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)|.
MARCHE Claude's avatar
MARCHE Claude committed
148

149
\paragraph{Theories.}
150
The syntax for theories is given on Figure~\ref{fig:bnf:theorya} and~\ref{fig:bnf:theoryb}.
151

MARCHE Claude's avatar
MARCHE Claude committed
152
\begin{figure}
153
  \begin{center}\framebox{\input{./theory_bnf.tex}}\end{center}
154
155
156
157
158
159
160
161
  \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}
162
163
\end{figure}

164
\paragraph{Files.}
MARCHE Claude's avatar
MARCHE Claude committed
165
A \why input file is a (possibly empty) list of theories.
166
167
168
169
\begin{center}\framebox{\input{./why_file_bnf.tex}}\end{center}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
MARCHE Claude's avatar
MARCHE Claude committed
170
\clearpage
171
\section{WhyML Language}\label{sec:syntax:whyml}
172

Andrei Paskevich's avatar
Andrei Paskevich committed
173
\subsection{Specification}
174

Andrei Paskevich's avatar
Andrei Paskevich committed
175
176
The syntax for specification clauses in programs 
is given in Figure~\ref{fig:bnf:spec}.
MARCHE Claude's avatar
MARCHE Claude committed
177
\begin{figure}
Andrei Paskevich's avatar
Andrei Paskevich committed
178
179
180
  \begin{center}\framebox{\input{./spec_bnf.tex}}\end{center}
  \caption{Specification clauses in programs.}
\label{fig:bnf:spec}
181
\end{figure}
182
183
184
185
186
187
188
Within specifications, terms are extended with new constructs
\verb|old| and \verb|at|:
\begin{center}\framebox{\input{./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$.
189

190
191
192
193
\subsection{Expressions}

The syntax for program expressions is given in
Figure~\ref{fig:bnf:expra} and~Figure~\ref{fig:bnf:exprb}.
MARCHE Claude's avatar
MARCHE Claude committed
194
\begin{figure}
195
  \begin{center}\framebox{\input{./expr_bnf.tex}}\end{center}
MARCHE Claude's avatar
MARCHE Claude committed
196
  \caption{Syntax for program expressions (part 1).}
197
198
199
200
201
\label{fig:bnf:expra}
\end{figure}

\begin{figure}
  \begin{center}\framebox{\input{./expr2_bnf.tex}}\end{center}
MARCHE Claude's avatar
MARCHE Claude committed
202
  \caption{Syntax for program expressions (part 2).}
203
\label{fig:bnf:exprb}
204
205
\end{figure}

206
207
208
209
210
211
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.


Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
212
213
214
% In the following we describe the informal semantics of each
% constructs, and provide the corresponding rule for computing the
% weakest precondition.
215
216


Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
217
% \subsubsection{Constant Expressions, Unary and Binary Operators}
218
219


Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
220
% Integer and real constants are as in the logic language, as weel as the unary and binary operators.
221

222

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
223
% \subsubsection{Array accesses and updates, fields access and updates}
224

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
225
% \todo{}
226

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
% \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}
348
349
350

\subsection{Modules}

351
The syntax for modules is given in Figure~\ref{fig:bnf:module}.
MARCHE Claude's avatar
MARCHE Claude committed
352
\begin{figure}
353
354
355
356
  \begin{center}\framebox{\input{./module_bnf.tex}}\end{center}
  \caption{Syntax for modules.}
\label{fig:bnf:module}
\end{figure}
357
358
359
360
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).
361

362
363
\subsection{Files}

MARCHE Claude's avatar
MARCHE Claude committed
364
A \whyml input file is a (possibly empty) list of theories and modules.
365
\begin{center}\framebox{\input{./whyml_file_bnf.tex}}\end{center}
366
367
368
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.
369

MARCHE Claude's avatar
MARCHE Claude committed
370

MARCHE Claude's avatar
MARCHE Claude committed
371
372
373
374
375
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: