syntaxref.tex 13.3 KB
 Jean-Christophe Filliâtre committed Jul 04, 2011 1 \chapter{Language Reference}  MARCHE Claude committed Dec 13, 2010 2 3 \label{chap:syntaxref}  Jean-Christophe Filliâtre committed Jul 04, 2011 4 This chapter gives the grammar and semantics for \why and \whyml input files.  Jean-Christophe Filliâtre committed May 31, 2011 5 6 7  \section{Lexical conventions}  MARCHE Claude committed Jul 02, 2011 8 Lexical conventions are common to \why and \whyml.  MARCHE Claude committed Dec 13, 2010 9   Jean-Christophe Filliâtre committed Dec 15, 2010 10 11 12 13 14 15 % TODO: blanks \paragraph{Comments.} Comments are enclosed by \texttt{(*} and \texttt{*)} and can be nested. \paragraph{Strings.}  Andrei Paskevich committed Dec 20, 2010 16 Strings are enclosed in double quotes (\verb!"!). Double quotes can be  MARCHE Claude committed Dec 15, 2010 17 inserted in strings using the backslash character (\verb!\!).  Jean-Christophe Filliâtre committed Jul 05, 2011 18 19 In the following, strings are referred to with the non-terminal \nonterm{string}{}.  Jean-Christophe Filliâtre committed Dec 15, 2010 20 21  % TODO: escape sequences for strings  Jean-Christophe Filliâtre committed Dec 15, 2010 22   Jean-Christophe Filliâtre committed Dec 15, 2010 23 \paragraph{Identifiers.} The syntax distinguishes lowercase and  Jean-Christophe Filliâtre committed Dec 15, 2010 24 uppercase identifiers and, similarly, lowercase and uppercase  Jean-Christophe Filliâtre committed Dec 15, 2010 25 qualified identifiers.  Andrei Paskevich committed Dec 20, 2010 26   Jean-Christophe Filliâtre committed Dec 15, 2010 27 28 \begin{center}\framebox{\input{./qualid_bnf.tex}}\end{center}  Jean-Christophe Filliâtre committed Dec 15, 2010 29 \paragraph{Constants.}  Andrei Paskevich committed Dec 20, 2010 30 The syntax for constants is given in Figure~\ref{fig:bnf:constant}.  Jean-Christophe Filliâtre committed Dec 16, 2010 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.  Andrei Paskevich committed Dec 20, 2010 34   MARCHE Claude committed Dec 20, 2010 35 \begin{figure}  Jean-Christophe Filliâtre committed Dec 15, 2010 36 37 38 39 40 \begin{center}\framebox{\input{./constant_bnf.tex}}\end{center} \caption{Syntax for constants.} \label{fig:bnf:constant} \end{figure}  Andrei Paskevich committed Dec 20, 2010 41 \paragraph{Operators.}  Jean-Christophe Filliâtre committed Dec 16, 2010 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:  Jean-Christophe Filliâtre committed Dec 15, 2010 47 \begin{itemize}  Jean-Christophe Filliâtre committed Dec 16, 2010 48 \item level 4: operators containing only characters from  Jean-Christophe Filliâtre committed Dec 15, 2010 49 \textit{op-char-4};  Jean-Christophe Filliâtre committed Dec 16, 2010 50 \item level 3: those containing  Jean-Christophe Filliâtre committed Dec 15, 2010 51  characters from \textit{op-char-3} or \textit{op-char-4};  Jean-Christophe Filliâtre committed Dec 16, 2010 52 \item level 2: those containing  Jean-Christophe Filliâtre committed Dec 15, 2010 53  characters from \textit{op-char-2}, \textit{op-char-3} or  Andrei Paskevich committed Dec 20, 2010 54  \textit{op-char-4};  Jean-Christophe Filliâtre committed Jan 24, 2011 55 \item level 1: all other operators (non-terminal \textit{infix-op-1}).  Jean-Christophe Filliâtre committed Dec 15, 2010 56 57 \end{itemize}  Jean-Christophe Filliâtre committed Jul 05, 2011 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.  Jean-Christophe Filliâtre committed May 31, 2011 64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  MARCHE Claude committed Jul 02, 2011 65   Jean-Christophe Filliâtre committed May 31, 2011 66 67 \section{Why3 Language}  Jean-Christophe Filliâtre committed Dec 15, 2010 68 \paragraph{Terms.}  Andrei Paskevich committed Dec 20, 2010 69 The syntax for terms is given in Figure~\ref{fig:bnf:term}.  Jean-Christophe Filliâtre committed Dec 16, 2010 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 & -- \\  Jean-Christophe Filliâtre committed Jan 24, 2011 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 & -- \\  Jean-Christophe Filliâtre committed Dec 16, 2010 88 89 90 91  \hline \end{tabular} \end{center}  Jean-Christophe Filliâtre committed Dec 15, 2010 92 93 Note the curryfied syntax for function application, though partial application is not allowed (rejected at typing).  Jean-Christophe Filliâtre committed Dec 15, 2010 94   MARCHE Claude committed Dec 20, 2010 95 \begin{figure}  Jean-Christophe Filliâtre committed Dec 15, 2010 96  \begin{center}\framebox{\input{./term_bnf.tex}}\end{center}  Jean-Christophe Filliâtre committed Dec 15, 2010 97  \caption{Syntax for terms.}  Jean-Christophe Filliâtre committed Dec 15, 2010 98 99 100 \label{fig:bnf:term} \end{figure}  Jean-Christophe Filliâtre committed Jul 04, 2011 101 \paragraph{Type Expressions.} The syntax for type expressions is the following:  Jean-Christophe Filliâtre committed Dec 15, 2010 102 \begin{center}\framebox{\input{./type_bnf.tex}}\end{center}  Jean-Christophe Filliâtre committed Jul 04, 2011 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}).  Jean-Christophe Filliâtre committed Dec 15, 2010 107   Jean-Christophe Filliâtre committed Dec 15, 2010 108 \paragraph{Formulas.}  Jean-Christophe Filliâtre committed Dec 15, 2010 109 The syntax for formulas is given Figure~\ref{fig:bnf:formula}.  Jean-Christophe Filliâtre committed Dec 16, 2010 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 \\  Andrei Paskevich committed Jun 30, 2011 120 121  \verb!\/! / \verb!||! & right \\ \verb|/\| / \verb!&&! & right \\  Jean-Christophe Filliâtre committed Dec 16, 2010 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{<>}).  Jean-Christophe Filliâtre committed Dec 15, 2010 133   MARCHE Claude committed Dec 20, 2010 134 \begin{figure}  Jean-Christophe Filliâtre committed Dec 15, 2010 135  \begin{center}\framebox{\input{./formula_bnf.tex}}\end{center}  Jean-Christophe Filliâtre committed Dec 15, 2010 136  \caption{Syntax for formulas.}  Jean-Christophe Filliâtre committed Dec 15, 2010 137 138 \label{fig:bnf:formula} \end{figure}  MARCHE Claude committed Dec 13, 2010 139   Guillaume Melquiond committed Oct 11, 2012 140 141 Notice that there are two symbols for the conjunction: \verb|/\| and \verb|&&|, and similarly for disjunction. They are logically  MARCHE Claude committed Dec 20, 2010 142 equivalent, but may be treated slightly differently by some  Guillaume Melquiond committed Oct 11, 2012 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 committed Dec 20, 2010 148   Jean-Christophe Filliâtre committed Dec 15, 2010 149 \paragraph{Theories.}  MARCHE Claude committed May 09, 2012 150 The syntax for theories is given on Figure~\ref{fig:bnf:theorya} and~\ref{fig:bnf:theoryb}.  Jean-Christophe Filliâtre committed Dec 15, 2010 151   MARCHE Claude committed Jul 02, 2011 152 \begin{figure}  Jean-Christophe Filliâtre committed Dec 15, 2010 153  \begin{center}\framebox{\input{./theory_bnf.tex}}\end{center}  MARCHE Claude committed May 09, 2012 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}  Jean-Christophe Filliâtre committed Dec 15, 2010 162 163 \end{figure}  Jean-Christophe Filliâtre committed May 31, 2011 164 \paragraph{Files.}  MARCHE Claude committed Jul 02, 2011 165 A \why input file is a (possibly empty) list of theories.  Jean-Christophe Filliâtre committed May 31, 2011 166 167 168 169 \begin{center}\framebox{\input{./why_file_bnf.tex}}\end{center} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  MARCHE Claude committed Jul 02, 2011 170 \clearpage  Jean-Christophe Filliâtre committed Aug 03, 2012 171 \section{WhyML Language}\label{sec:syntax:whyml}  Jean-Christophe Filliâtre committed May 31, 2011 172   Andrei Paskevich committed Oct 23, 2012 173 \subsection{Specification}  MARCHE Claude committed Jun 01, 2012 174   Andrei Paskevich committed Oct 23, 2012 175 176 The syntax for specification clauses in programs is given in Figure~\ref{fig:bnf:spec}.  MARCHE Claude committed Jul 02, 2011 177 \begin{figure}  Andrei Paskevich committed Oct 23, 2012 178 179 180  \begin{center}\framebox{\input{./spec_bnf.tex}}\end{center} \caption{Specification clauses in programs.} \label{fig:bnf:spec}  Jean-Christophe Filliâtre committed May 31, 2011 181 \end{figure}  Jean-Christophe Filliâtre committed Feb 21, 2013 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$.  Jean-Christophe Filliâtre committed May 31, 2011 189   MARCHE Claude committed Jun 01, 2012 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 committed Jul 02, 2011 194 \begin{figure}  Jean-Christophe Filliâtre committed May 31, 2011 195  \begin{center}\framebox{\input{./expr_bnf.tex}}\end{center}  MARCHE Claude committed Oct 31, 2012 196  \caption{Syntax for program expressions (part 1).}  MARCHE Claude committed May 09, 2012 197 198 199 200 201 \label{fig:bnf:expra} \end{figure} \begin{figure} \begin{center}\framebox{\input{./expr2_bnf.tex}}\end{center}  MARCHE Claude committed Oct 31, 2012 202  \caption{Syntax for program expressions (part 2).}  MARCHE Claude committed May 09, 2012 203 \label{fig:bnf:exprb}  Jean-Christophe Filliâtre committed May 31, 2011 204 205 \end{figure}  Jean-Christophe Filliâtre committed Feb 21, 2013 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 committed Oct 29, 2012 212 213 214 % In the following we describe the informal semantics of each % constructs, and provide the corresponding rule for computing the % weakest precondition.  MARCHE Claude committed Jun 01, 2012 215 216   Jean-Christophe Filliâtre committed Oct 29, 2012 217 % \subsubsection{Constant Expressions, Unary and Binary Operators}  MARCHE Claude committed Jun 01, 2012 218 219   Jean-Christophe Filliâtre committed Oct 29, 2012 220 % Integer and real constants are as in the logic language, as weel as the unary and binary operators.  MARCHE Claude committed Jun 01, 2012 221   Guillaume Melquiond committed Oct 11, 2012 222   Jean-Christophe Filliâtre committed Oct 29, 2012 223 % \subsubsection{Array accesses and updates, fields access and updates}  MARCHE Claude committed Jun 01, 2012 224   Jean-Christophe Filliâtre committed Oct 29, 2012 225 % \todo{}  MARCHE Claude committed Jun 01, 2012 226   Jean-Christophe Filliâtre committed Oct 29, 2012 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}  MARCHE Claude committed Jun 01, 2012 348 349 350  \subsection{Modules}  MARCHE Claude committed May 09, 2012 351 The syntax for modules is given in Figure~\ref{fig:bnf:module}.  MARCHE Claude committed Jul 02, 2011 352 \begin{figure}  Jean-Christophe Filliâtre committed May 31, 2011 353 354 355 356  \begin{center}\framebox{\input{./module_bnf.tex}}\end{center} \caption{Syntax for modules.} \label{fig:bnf:module} \end{figure}  Jean-Christophe Filliâtre committed Jul 04, 2011 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).  Jean-Christophe Filliâtre committed May 31, 2011 361   MARCHE Claude committed Jun 01, 2012 362 363 \subsection{Files}  MARCHE Claude committed Jul 02, 2011 364 A \whyml input file is a (possibly empty) list of theories and modules.  Jean-Christophe Filliâtre committed May 31, 2011 365 \begin{center}\framebox{\input{./whyml_file_bnf.tex}}\end{center}  Jean-Christophe Filliâtre committed Jul 04, 2011 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.  Jean-Christophe Filliâtre committed May 31, 2011 369   MARCHE Claude committed Oct 31, 2012 370   MARCHE Claude committed Dec 13, 2010 371 372 373 374 375 %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: