syntaxref.tex 10.9 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 MARCHE Claude committed Jun 01, 2012 173 174 \subsection{Types} MARCHE Claude committed May 09, 2012 175 The syntax for program types is given in Figure~\ref{fig:bnf:typev}. MARCHE Claude committed Jul 02, 2011 176 \begin{figure} Jean-Christophe Filliâtre committed May 31, 2011 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} MARCHE Claude committed Jun 01, 2012 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 committed Jul 02, 2011 186 \begin{figure} Jean-Christophe Filliâtre committed May 31, 2011 187 \begin{center}\framebox{\input{./expr_bnf.tex}}\end{center} MARCHE Claude committed May 09, 2012 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} Jean-Christophe Filliâtre committed May 31, 2011 196 197 \end{figure} MARCHE Claude committed Jun 01, 2012 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} Guillaume Melquiond committed Oct 11, 2012 203 \todo{Integer and real constants are as in the logic language} MARCHE Claude committed Jun 01, 2012 204 205 206 \subsubsection{Unary and Binary Operators} Guillaume Melquiond committed Oct 11, 2012 207 208 \todo{} MARCHE Claude committed Jun 01, 2012 209 210 \subsubsection{Array accesses and updates, fields access and updates} Guillaume Melquiond committed Oct 11, 2012 211 \todo{} MARCHE Claude committed Jun 01, 2012 212 213 214 \subsubsection{Let binding, sequences} Guillaume Melquiond committed Oct 11, 2012 215 \todo{} MARCHE Claude committed Jun 01, 2012 216 217 218 \subsubsection{Function definition} Guillaume Melquiond committed Oct 11, 2012 219 \todo{fun, let rec} MARCHE Claude committed Jun 01, 2012 220 221 222 \subsubsection{Function call} Guillaume Melquiond committed Oct 11, 2012 223 \todo{} MARCHE Claude committed Jun 01, 2012 224 225 226 \subsubsection{Exception throwing and catching} Guillaume Melquiond committed Oct 11, 2012 227 \todo{raise, try with end} MARCHE Claude committed Jun 01, 2012 228 229 230 \subsubsection{Conditional expression, pattern matching} Guillaume Melquiond committed Oct 11, 2012 231 \todo{if then else. Discuss standard WP versus fast WP} MARCHE Claude committed Jun 01, 2012 232 233 234 \subsubsection{Loops} Guillaume Melquiond committed Oct 11, 2012 235 \todo{while, loop, for} MARCHE Claude committed Jun 01, 2012 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 Guillaume Melquiond committed Oct 11, 2012 251 visible in the context of the remaining code, without requiring to MARCHE Claude committed Jun 01, 2012 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 Guillaume Melquiond committed Oct 11, 2012 264 265 non-deterministic expression that requires the precondition $P$ to hold, then makes some side effects $\epsilon$, and returns any value MARCHE Claude committed Jun 01, 2012 266 of type $\tau$ such that $Q$ holds. This construct acts as an axiom Guillaume Melquiond committed Oct 11, 2012 267 in the sense that it does not check whether there exists any program MARCHE Claude committed Jun 01, 2012 268 269 that can effectively establish the post-condition (similarly as the introduction of a \texttt{val} at the global level). Guillaume Melquiond committed Oct 11, 2012 270 \item $\texttt{contract}~e~\{ Q \}$ evaluates the expression $e$ and MARCHE Claude committed Jun 01, 2012 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 MARCHE Claude committed Jun 01, 2012 290 \forall result, \epsilon, Q \rightarrow Q' \land R_i \rightarrow R'_i MARCHE Claude committed Jun 01, 2012 291 292 293 \end{array}$ Guillaume Melquiond committed Oct 11, 2012 294 \todo{? sandbox:} MARCHE Claude committed Jun 01, 2012 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} Guillaume Melquiond committed Oct 11, 2012 302 \todo{} MARCHE Claude committed Jun 01, 2012 303 304 305 \subsection{Modules} MARCHE Claude committed May 09, 2012 306 The syntax for modules is given in Figure~\ref{fig:bnf:module}. MARCHE Claude committed Jul 02, 2011 307 \begin{figure} Jean-Christophe Filliâtre committed May 31, 2011 308 309 310 311 \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 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). Jean-Christophe Filliâtre committed May 31, 2011 316 MARCHE Claude committed Jun 01, 2012 317 318 \subsection{Files} MARCHE Claude committed Jul 02, 2011 319 A \whyml input file is a (possibly empty) list of theories and modules. Jean-Christophe Filliâtre committed May 31, 2011 320 \begin{center}\framebox{\input{./whyml_file_bnf.tex}}\end{center} Jean-Christophe Filliâtre committed Jul 04, 2011 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. Jean-Christophe Filliâtre committed May 31, 2011 324 MARCHE Claude committed Dec 13, 2010 325 326 327 328 329 %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: