\chapter{Language Reference}
\label{chap:syntaxref}

This chapter gives the grammar and semantics for \why and \whyml input files.

\section{Lexical conventions}

Lexical conventions are common to \why and \whyml.

% TODO: blanks

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

\paragraph{Strings.}
Strings are enclosed in double quotes (\verb!"!). Double quotes can be
inserted in strings using the backslash character (\verb!\!).
In the following, strings are referred to with the non-terminal
\nonterm{string}{}.

% TODO: escape sequences for strings

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

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

\paragraph{Constants.}
The syntax for constants is given in Figure~\ref{fig:bnf:constant}.
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.

\begin{figure}
\begin{center}\framebox{\input{./constant_bnf.tex}}\end{center}
  \caption{Syntax for constants.}
\label{fig:bnf:constant}
\end{figure}

\paragraph{Operators.}
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:
\begin{itemize}
\item level 4: operators containing only characters from
\textit{op-char-4};
\item level 3: those containing
 characters from \textit{op-char-3} or \textit{op-char-4};
\item level 2: those containing
 characters from \textit{op-char-2}, \textit{op-char-3} or
 \textit{op-char-4};
\item level 1: all other operators (non-terminal \textit{infix-op-1}).
\end{itemize}

\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.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Why3 Language}

\paragraph{Terms.}
The syntax for terms is given in Figure~\ref{fig:bnf:term}.
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  & -- \\
    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       & --   \\
    \hline
  \end{tabular}
\end{center}

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

\begin{figure}
  \begin{center}\framebox{\input{./term_bnf.tex}}\end{center}
  \caption{Syntax for terms.}
\label{fig:bnf:term}
\end{figure}

\paragraph{Type Expressions.} The syntax for type expressions is the following:
\begin{center}\framebox{\input{./type_bnf.tex}}\end{center}
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}).

\paragraph{Formulas.}
The syntax for formulas is given Figure~\ref{fig:bnf:formula}.
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 \\
    \verb!\/! / \verb!||! & right \\
    \verb|/\| / \verb!&&! & right \\
    \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{<>}).

\begin{figure}
  \begin{center}\framebox{\input{./formula_bnf.tex}}\end{center}
  \caption{Syntax for formulas.}
\label{fig:bnf:formula}
\end{figure}

Notice that there are two symbols for the conjunction: \texttt{and}
and \verb|&&|, and similarly for disjunction. There are logically
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
$A~\verb|&&|~B$ into subgoals $A$ and $A\rightarrow B$.

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

\begin{figure}
  \begin{center}\framebox{\input{./theory_bnf.tex}}\end{center}
  \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}
\end{figure}

\paragraph{Files.}
A \why input file is a (possibly empty) list of theories.
\begin{center}\framebox{\input{./why_file_bnf.tex}}\end{center}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\clearpage
\section{Why3ML Language}\label{sec:syntax:whyml}

\subsection{Types}

The syntax for program types is given in Figure~\ref{fig:bnf:typev}.
\begin{figure}
  \begin{center}\framebox{\input{./typev_bnf.tex}}\end{center}
  \caption{Syntax for program types.}
\label{fig:bnf:typev}
\end{figure}

\subsection{Expressions}

The syntax for program expressions is given in
Figure~\ref{fig:bnf:expra} and~Figure~\ref{fig:bnf:exprb}.
\begin{figure}
  \begin{center}\framebox{\input{./expr_bnf.tex}}\end{center}
  \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}
\end{figure}

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
  \forall result, \epsilon, Q \rightarrow Q' \land R_i \rightarrow R'_i
\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}

The syntax for modules is given in Figure~\ref{fig:bnf:module}.
\begin{figure}
  \begin{center}\framebox{\input{./module_bnf.tex}}\end{center}
  \caption{Syntax for modules.}
\label{fig:bnf:module}
\end{figure}
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).

\subsection{Files}

A \whyml input file is a (possibly empty) list of theories and modules.
\begin{center}\framebox{\input{./whyml_file_bnf.tex}}\end{center}
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.

%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: