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

173 174
\subsection{Types}

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

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

198 199 200 201 202
In the following we describe the informal semantics of each constructs, and provide the corresponding rule for computing the weakest precondition.


\subsubsection{Constant expressions}

203
\todo{Integer and real constants are as in the logic language}
204 205 206

\subsubsection{Unary and Binary Operators}

207 208
\todo{}

209 210
\subsubsection{Array accesses and updates, fields access and updates}

211
\todo{}
212 213 214

\subsubsection{Let binding, sequences}

215
\todo{}
216 217 218

\subsubsection{Function definition}

219
\todo{fun, let rec}
220 221 222

\subsubsection{Function call}

223
\todo{}
224 225 226

\subsubsection{Exception throwing and catching}

227
\todo{raise, try with end}
228 229 230

\subsubsection{Conditional expression, pattern matching}

231
\todo{if then else. Discuss standard WP versus fast WP}
232 233 234

\subsubsection{Loops}

235
\todo{while, loop, for}
236 237 238 239 240 241 242 243 244 245 246 247 248 249 250

\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
251
  visible in the context of the remaining code, without requiring to
252 253 254 255 256 257 258 259 260 261 262 263
  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
264 265
  non-deterministic expression that requires the precondition $P$ to
  hold, then makes some side effects $\epsilon$, and returns any value
266
  of type $\tau$ such that $Q$ holds. This construct acts as an axiom
267
  in the sense that it does not check whether there exists any program
268 269
  that can effectively establish the post-condition (similarly as the
  introduction of a \texttt{val} at the global level).
270
\item $\texttt{contract}~e~\{ Q \}$ evaluates the expression $e$ and
271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289
  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
290
  \forall result, \epsilon, Q \rightarrow Q' \land R_i \rightarrow R'_i
291 292 293
\end{array}
\]

294
\todo{? sandbox:}
295 296 297 298 299 300 301
\[
WP(\texttt{sandbox}~e, Q) = WP(e,true) \land Q
\]
(side-effects in $e$ are "forgotten"...)

\subsubsection{Labels, old, at}

302
\todo{}
303 304 305

\subsection{Modules}

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

317 318
\subsection{Files}

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

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