syntaxref.tex 10.8 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

MARCHE Claude's avatar
MARCHE Claude committed
140
Notice that there are two symbols for the conjunction: \texttt{and}
141
and \verb|&&|, and similarly for disjunction. There are logically
MARCHE Claude's avatar
MARCHE Claude committed
142
143
144
equivalent, but may be treated slightly differently by some
transformation, \eg{} the \texttt{split} transformation transforms
$A~\texttt{and}~B$ into subgoals $A$ and $B$, whereas it transforms
145
$A~\verb|&&|~B$ into subgoals $A$ and $A\rightarrow B$.
MARCHE Claude's avatar
MARCHE Claude committed
146

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

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

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


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
MARCHE Claude's avatar
MARCHE Claude committed
168
\clearpage
169
170
\section{Why3ML Language}\label{sec:syntax:whyml}

171
172
\subsection{Types}

173
The syntax for program types is given in Figure~\ref{fig:bnf:typev}.
MARCHE Claude's avatar
MARCHE Claude committed
174
\begin{figure}
175
176
177
178
179
  \begin{center}\framebox{\input{./typev_bnf.tex}}\end{center}
  \caption{Syntax for program types.}
\label{fig:bnf:typev}
\end{figure}

180
181
182
183
\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
184
\begin{figure}
185
  \begin{center}\framebox{\input{./expr_bnf.tex}}\end{center}
186
187
188
189
190
191
192
193
  \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}
194
195
\end{figure}

196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
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
In the following we describe the informal semantics of each constructs, and provide the corresponding rule for computing the weakest precondition.


\subsubsection{Constant expressions}

Integer and real constants are as in the logic language

TODO

\subsubsection{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}

if then else. Discuss standar WP versus fast WP

\subsubsection{Loops}

while, loop, for

\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 remiaing 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 which 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 is 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{contract}~e~\{ Q \}$ evaluates expression $e$ and the
  ensures that the post-condition $Q$ holds afterwards.
\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{contract}~e~\{ Q \mid exn_i \Rightarrow R_i \} ,
  Q' \mid exn_i \Rightarrow R'_i) = \\
  \qquad\qquad WP(e,Q \land Q' \mid exn_i \Rightarrow R_i \land 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
288
  \forall result, \epsilon, Q \rightarrow Q' \land R_i \rightarrow R'_i
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
\end{array}
\]

TODO ? sandbox:
\[
WP(\texttt{sandbox}~e, Q) = WP(e,true) \land Q
\]
(side-effects in $e$ are "forgotten"...)

\subsubsection{Labels, old, at}

TODO

\subsection{Modules}

304
The syntax for modules is given in Figure~\ref{fig:bnf:module}.
MARCHE Claude's avatar
MARCHE Claude committed
305
\begin{figure}
306
307
308
309
  \begin{center}\framebox{\input{./module_bnf.tex}}\end{center}
  \caption{Syntax for modules.}
\label{fig:bnf:module}
\end{figure}
310
311
312
313
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).
314

315
316
\subsection{Files}

MARCHE Claude's avatar
MARCHE Claude committed
317
A \whyml input file is a (possibly empty) list of theories and modules.
318
\begin{center}\framebox{\input{./whyml_file_bnf.tex}}\end{center}
319
320
321
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.
322

MARCHE Claude's avatar
MARCHE Claude committed
323
324
325
326
327
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: