speclang_modern.tex

%; whizzy-master "main.tex"

\chapter{Specification language}
\label{chap:base}

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

\section{Lexical rules}
\nodiff

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

\section{Logic expressions}
\label{sec:expressions}

\except{guarded quantificatication}.

More precisely, grammars of terms and binders presented respectively
Figures~\ref{fig:gram:term} and~\ref{fig:gram:binders} are the same than the one
of \acsl, while Figure~\ref{fig:gram:pred} presents grammar of predicates. The
only difference between \eacsl and \acsl predicates are quantifications.

\begin{figure}[htbp]
  \begin{cadre}
    \input{term_modern.bnf}
  \end{cadre}
  \caption{Grammar of terms}
\label{fig:gram:term}
\end{figure}
\begin{figure}[htbp]
  \begin{cadre}
    \input{predicate_modern.bnf}
  \end{cadre}
  \caption{Grammar of predicates}
\label{fig:gram:pred}
\end{figure}
\begin{figure}[htbp]
  \fbox{\begin{minipage}{0.97\textwidth} \input{binders_modern.bnf}
    \end{minipage}}
  \caption{Grammar of binders and type expressions}
\label{fig:gram:binders}
\end{figure}

\begin{notimplementedenv}
  Reals are not correctly supported by the \eacsl plug-in right now. Only
  floating point numbers are supported: real constants and operations are seen as
  \C floating point constants and operations.
\end{notimplementedenv}

\subsection*{Quantification}
\eacsl quantification must be computable. They are limited to two limited forms.

\begin{description}
\item[Guarded integer quantification] Guarded universal quantification is
  denoted by
\begin{lstlisting}
\forall $\tau$ $x_1$,$\ldots$,$x_n$;
  $a_1$ <= $x_1$ <= $b_1$ $\ldots$ && $a_n$ <= $x_n$ <= $b_n$
  ==> p
\end{lstlisting} and guarded existential quantification by
\begin{lstlisting}
\exists $\tau$ $x_1$,$\ldots$,$x_n$;
  $a_1$ <= $x_1$ <= $b_1$ $\ldots$ && $a_n$ <= $x_n$ <= $b_n$
  && p
\end{lstlisting}
Each variable must be guarded exactly once and the guard of $x_i$ must appear
before the guard of $x_j$ if $i < j$ (\emph{i.e.} order of guards must follow
order of binders).

Following the definition, each quantified variable belongs to a finite
interval. Since finite interval is only computable in practice for integers,
this form of quantifier is limited to \texttt{integer} and its subtype. Thus
there is no guarded quantification over \texttt{float}, \texttt{real}, \C
pointers or logic types.

\item[{\highlightnotimplemented{Iterator quantification}}] In order to iterate
  over non-integer types, \eacsl introduces a notion of $iterators$ over types:
  standard \acsl unguarded quantifications are only allowed over a type which an
  iterator is attached to.

  Iterators are introduced by a specific construct which attachs two sets ---
  namely \texttt{nexts} and the \texttt{guards} --- to a binary predicate over a
  type $\tau$. Both sets must have the same cardinal. This construct is
  described by the grammar of Figure~\ref{fig:gram:iterator}.
  \begin{figure}[htbp]
    \begin{cadre}
      \input{iterator_modern.bnf}
    \end{cadre}
    \caption{Grammar of iterator declarations}
    \label{fig:gram:iterator}
  \end{figure}
  For a type $\tau$, \texttt{nexts} is a set of terms which take an argument of
  type $\tau$ and return a value of type $\tau$ which computes the next element
  in this type, while \texttt{guards} is a set of predicates which take an
  argument of type $\tau$ and are valid (resp. invalid) to continue (resp. stop)
  the iteration.

  Furthermore, the guard of a quantification using an iterator must be the
  predicate given in the definition of the iterator. This abstract binary
  predicate takes two arguments of the same type. One of them must be unnamed by
  using a wildcard (character underscore \texttt{'\_'}). The unnamed argument
  must be binded to the guantifier, while the other corresponds to the term from
  which the iteration begins.
  \begin{example}
    The following example introduces binary trees and a predicate which is valid
    if and only if each value of a binary tree is even.
    \cinput{link.c}
  \end{example}

\item[{\highlightnotimplemented{Unguarded quantification}}] They are only
  allowed over boolean and char.
\end{description}

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

\subsection{Operators precedence}
\nodiff

Figure~\ref{fig:precedence} summarizes operator precedences.
\begin{figure}[htbp]
  \begin{center}
    \begin{tabular}{|l|l|l|}
      \hline
      class 	& associativity & operators \\
      \hline
      selection & left & \lstinline|[$\cdots$]| \lstinline|->| \lstinline|.| \\
      unary 	& right & \lstinline|!| \lstinline|~| \lstinline|+|
      \lstinline|-| \lstinline|*| \lstinline|&| \lstinline|(cast)|
      \lstinline|sizeof| \\
      multiplicative & left & \lstinline|*| \lstinline|/|  \lstinline|%| \\
      additive & left & \lstinline|+| \lstinline|-| \\
      shift 	& left & \lstinline|<<| \lstinline|>>| \\
      comparison & left & \lstinline|<| \lstinline|<=| \lstinline|>| \lstinline|>=| \\
      comparison & left & \lstinline|==| \lstinline|!=| \\
      bitwise and & left & \lstinline|&| \\
      bitwise xor & left & \lstinline|^| \\
      bitwise or & left & \lstinline+|+ \\
      bitwise implies & left & \lstinline+-->+ \\
      bitwise equiv & left & \lstinline+<-->+ \\
      connective and     & left & \lstinline|&&| \\
      connective xor & left & \lstinline+^^+ \\
      connective or & left & \lstinline+||+ \\
      connective implies & right & \lstinline|==>| \\
      connective equiv & left & \lstinline|<==>| \\
      ternary connective & right & \lstinline|$\cdots$?$\cdots$:$\cdots$| \\
      binding & left & \Forall{} \Exists{} \Let{} \\
      naming & right & \lstinline|:| \\
      \hline
    \end{tabular}
  \end{center}
  \caption{Operator precedence}
\label{fig:precedence}
\end{figure}


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

\subsection{Semantics}
\label{sec:semantics}

\except{undefinedness and same laziness than \C}

More precisely, while \acsl is a 2-valued logic with only total
functions, \eacsl is a 3-valued logic with partial functions since
terms and predicates may be ``undefined''.

In this logic, the semantics of a term denoting a \C expression $e$ is undefined
if $e$ leads to a runtime error. Consequently the semantics of any term $t$
(resp. predicate $p$) containing a \C expression $e$ leading to a runtime error
is undefined if $e$ has to be evaluated in order to evaluate $t$ (resp. $p$).
\begin{remark}[Julien]
$e$ always terminates, thus no termination issue.
\end{remark}
\begin{example}
The semantics of all the below predicates are undefined:
\begin{itemize}
\item \lstinline|1/0 == 1/0|
\item \lstinline|f(*p)| for any logic function \lstinline|f| and invalid pointer
  \lstinline|p|
\end{itemize}
\end{example}

Furthermore, \C-like operators \lstinline|&&|, \lstinline+||+, \lstinline|^^|
and \lstinline|_ ? _ : _| are lazy like in \C: their right members are evaluated
only if required. Thus the amount of undefinedness is limited. Consequently,
predicate \lstinline|p ==> q| is also lazy since it is equivalent
to \lstinline+!p || q+. It is also the case for guarded quantifications since
guards are conjunctions and for ternary condition since it is equivalent to a
disjunction of implications.

\begin{example}\label{ex:semantics}
Below, the first, second and fourth predicates are invalid while the third
one is valid:
\begin{itemize}
\item \lstinline|\false && 1/0 == 1/0|
\item \lstinline|\forall integer x, -1 <= x <= 1 ==> 1/x > 0|
\item \lstinline|\forall integer x, 0 <= x <= 0 ==> \false ==> -1 <= 1/x <= 1|
\item \lstinline|\exists integer x, 1 <= x <= 0 && -1 <= 1/x <= 1|
\end{itemize}
In particular, the second one is invalid since the quantification is in fact an
enumeration over a finite number of elements, it amounts to 
\lstinline|1/-1 > 0 && 1/0 > 0 && 1/1 > 0|. The first atomic proposition is
invalid, so the rest of the conjunction (and in particular 1/0) is not
evaluated. The fourth one is invalid since it is an existential quantification
over an empty range.

\emph{A contrario} the semantics of predicates below is undefined:
\begin{itemize}
\item \lstinline|1/0 == 1/0 && \false|
\item \lstinline|-1 <= 1/0 <= 1 ==> \true|
\item \lstinline|\exists integer x, -1 <= x <= 1 && 1/x > 0 |
\end{itemize}
\end{example}

Furthermore, casting a term denoting a \C expression $e$ to a smaller type
$\tau$ is undefined if $e$ is not representable in $\tau$.

\begin{example}
Below, the first term is well-defined, while the second one is undefined.
\begin{itemize}
\item \lstinline|(char)127|
\item \lstinline|(char)128|
\end{itemize}
\end{example}

\paragraph{Handling undefinedness in tools}

It is the responsibility of each tool which interprets \eacsl to ensure that an
undefined term is never evaluated. For instance, they may exit with a proper
error message or, if they generate \C code, they may guard each generated
undefined \C expression in order to be sure that they are always safely used.

This behavior is consistent with both \acsl~\cite{acsl} and mainstream
specification languages for runtime assertion checking like
\jml~\cite{jml}. Consistency means that, if it exists and is defined, the \eacsl
predicate corresponding to a valid (resp. invalid) \acsl predicate is valid
(resp. invalid). Thus it is possible to reuse tools interpreting \acsl like the
\framac's value analysis plug-in~\cite{value} in order to interpret \eacsl, and
it is also possible to perform runtime assertion checking of \eacsl predicates
in the same way than \jml predicates. Reader interested by the implications
(especially issues) of such a choice may read articles of Patrice
Chalin~\cite{chalin05,chalin07}.

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

\subsection{Typing}\label{sec:typing}
\except{no user-defined types}

It is not possible to define logic types introduced by the specification writer
(see Section~\ref{sec:logicspec}).

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

\subsection{Integer arithmetic and machine integers}
\nodiff

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

\subsection{\notimplemented{Real numbers} and floating point numbers}
\nodiff

\difficults{\notimplemented{Exact real numbers} and even floating point numbers}

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

\subsection{C arrays and pointers}
\nodiff

\difficultwhy{Ensuring validity of memory accesses}{the implementation of a
  memory model}

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

\subsection{Structures, Unions and Arrays in logic}
\nodiff

\difficults{\notimplemented{Logic arrays} without an explicit length}

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

\subsection{String literals}
\nodiff

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

\section{Function contracts}
\label{sec:fn-behavior}
\index{function contract}\index{contract}

\except{no \lstinline|terminates| and \lstinline|abrupt| clauses}

Figure~\ref{fig:gram:contracts} shows grammar of function
contracts. This is a simplified version of \acsl one without
\lstinline|terminates| and \lstinline|abrupt|
clauses. Section~\ref{sec:termination} (resp.~\ref{sec:abrupt}) explains why
\eacsl has no \lstinline|terminates| (resp. \lstinline|abrupt|) clause.

\begin{figure}[htbp]
  \begin{cadre}
      \input{fn_behavior_modern.bnf}
   \end{cadre}
    \caption{Grammar of function contracts}
  \label{fig:gram:contracts}
\end{figure}

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

\subsection{Built-in constructs %
  \texorpdfstring{\old}{\textbackslash{}old} %
 and \texorpdfstring{\result}{\textbackslash{}result}}
\label{sec:builtinconstructs}

\nodiff

Figure~\ref{fig:gram:oldandresult} summarizes grammar extension of terms with
\lstinline|\old| and \lstinline|\result|.
\begin{figure}[htbp]
  \begin{cadre}
      \input{oldandresult_modern.bnf}
    \end{cadre}
    \caption{\protect\old and \protect\result in terms}
  \label{fig:gram:oldandresult}
\end{figure}

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

\subsection{Simple function contracts}
\label{sec:simplecontracts}

\nodiff

\difficultwhy{\notimplemented{\lstinline|\\assigns|}}{the implementation of a
  memory model}

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

\subsection{Contracts with named behaviors}
\label{subsec:behaviors}
\index{function behavior}\index{behavior}

\nodiff

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

\subsection{Memory locations and sets of terms}
\label{sec:locations}

\except{\notimplemented{ranges and set comprehensions} are limited in order to
  be finite}

Figure~\ref{fig:gram:locations} describes grammar of sets of terms. The only
differences with \acsl are that both lower and upper bounds of ranges are
mandatory and that the predicate inside set comprehension must be guarded and
bind only one variable. In that way, each set of terms is finite and their
members easily identifiable.
\begin{figure}[htbp]
  \fbox{\begin{minipage}{0.97\textwidth}
      \input{loc_modern.bnf}
    \end{minipage}}
  \caption{Grammar for sets of terms}
\label{fig:gram:locations}
\end{figure}

\begin{notimplementedenv}
\begin{example}\label{ex:tset}
The set \lstinlineµ{ x | integer x; 0 <= x <= 9 || 20 <= x <= 29 }µ denotes the
set of all integers between 0 and 9 and between 20 and 29.
\end{example}
\end{notimplementedenv}

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

\subsection{Default contracts, multiple contracts}
\nodiff

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

\section{Statement annotations}
\index{annotation}

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

\subsection{Assertions}
\label{sec:assertions}
\indextt{assert}
\nodiff

Figure~\ref{fig:gram:assertions} summarizes grammar for assertions.
\begin{figure}[htbp]
  \begin{cadre}
    \input{assertions_modern.bnf}
  \end{cadre}
  \caption{Grammar for assertions}
  \label{fig:gram:assertions}
\end{figure}

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

\subsection{Loop annotations}
\label{sec:loop_annot}

\except{loop invariants lose their inductive nature}

Figure~\ref{fig:gram:loops} shows grammar for loop annotations. There is no
syntactic difference with \acsl. 
\begin{figure}[htbp]
  \begin{cadre}
    \input{loops_modern.bnf}
  \end{cadre}
  \caption{Grammar for loop annotations}
  \label{fig:gram:loops}
\end{figure}

\difficultwhy{\notimplemented{\lstinline|loop assigns|}}{the implementation of a
  memory model}

\subsubsection{Loop invariants}

\index{invariant} The semantics of loop invariants is the same than the one
defined in \acsl, except that they are not inductive. More precisely, if one
does not take care of side effects (semantics of specifications about side
effects in loop is the same in \eacsl than the one in \acsl), a loop invariant
$I$ is valid in \acsl if and only if:
\begin{itemize}
\item $I$ holds before entering the loop; and
\item if $I$ is assumed true in some state where the loop condition $c$ is also
  true, and if execution of the loop body in that state ends normally at the end
  of the body or with a "continue" statement, $I$ is true in the resulting
  state.
\end{itemize}

In \eacsl, the same loop invariant $I$ is valid if and only if:
\begin{itemize}
\item $I$ holds before entering the loop; and
\item if execution of the loop body in that state ends normally at the end of
  the body or with a "continue" statement, $I$ is true in the resulting state. 
\end{itemize}

Thus the only difference with \acsl is that \eacsl does not assume that the
invariant previously holds when one checks that it holds at the end of the loop
body. In other words a loop invariant \lstinline|I| is equivalent to put an
assertion \lstinline|I| just before entering the loop and at the very end of the
loop body.

\begin{example}
In the following, \lstinline|bsearch(t,n,v)| searches for element \lstinline|v|
in array \lstinline|t| between indices \lstinline|0| and \lstinline|n-1|.

\cinput{bsearch.c}

In \eacsl, this annotated function is equivalent to the following one since
loop invariants are not inductive.

\cinput{bsearch2.c}

\end{example}

\subsubsection{General inductive invariant}

Syntax of these kinds of invariant is shown Figure~\ref{fig:advancedinvariants}
\begin{figure}[t]
  \begin{cadre}
    \input{generalinvariants_modern.bnf}
  \end{cadre}
  \caption{Grammar for general inductive invariants}
  \label{fig:advancedinvariants}
\end{figure}

In \eacsl, these kinds of invariants put everywhere in a loop body is exactly
equivalent to an assertion.

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

\subsection{Built-in construct \texorpdfstring{\at}{\textbackslash{}at}}
\label{sec:at}\indexttbs{at}

\except{no forward references}

The construct \verb|\at(t,id)| (where \verb|id| is a regular C label, a label
added within a ghost statement or a default logic label)
follows the same rule than its \acsl counterpart, except that a more restrictive
scoping rule must be respected in addition to the standard \acsl scoping rule:
when evaluating \verb|\at(t,id)| at a propram point $p$, the program point $p'$
denoted by \verb|id| must be executed after $p$ the program execution flow.

\begin{example}
In the following example, both assertions are accepted and valid in \acsl, but
only the first one is accepted and valid in \eacsl since evaluating the term
\verb|\at(*(p+\at(*q,Here)),L1)| at \verb|L2| requires to evaluate the term
 \verb|\at(*q,Here)| at \verb|L1|: that is forbidden since \verb|L1| is executed
 before \verb|L2|.
\cinput{at.c}

\end{example}

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

\subsection{Statement contracts}
\label{sec:statement_contract}
\index{statement contract}\index{contract}

\except{no \lstinline|abrupt| clauses}

Figure~\ref{fig:gram:contracts} shows grammar of statement contracts. Like
function contracts, this is a simplified version of \acsl with no
\lstinline|abrupt| clauses. All other constructs are unchanged.

\begin{figure}[htbp]
  \begin{cadre}
    \input{st_contracts_modern.bnf}
  \end{cadre}
  \caption{Grammar for statement contracts}
  \label{fig:gram:stcontracts}
\end{figure}

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

\section{Termination}
\label{sec:termination}
\index{termination}

\except{no \lstinline|terminates| clauses}

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

\subsection{\notimplemented{Integer measures}}
\label{sec:integermeasures}
\indexttbs{decreases}\indexttbs{variant}
\nodiff

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

\subsection{\notimplemented{General measures}}
\label{sec:generalmeasures}
\nodiff

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

\subsection{\notimplemented{Recursive function calls}}
\nodiff

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

\subsection{Non-terminating functions}
\absentexperimental

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

\section{Logic specifications}
\label{sec:logicspec}
\index{logic specification}\index{specification}

\limited{stable and computable features}

Figure~\ref{fig:gram:logic} presents grammar of logic definitions. This is the
same than the one of \acsl without polymorphic definitions, lemmas, nor
axiomatics.

\begin{figure}[htbp]
  \fbox{\begin{minipage}{0.97\linewidth}\vfill \input{logic_modern.bnf}
    \vfill\end{minipage}}
  \caption{Grammar for global logic definitions}
\label{fig:gram:logic}
\end{figure}

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

\subsection{\notimplemented{Predicate and function definitions}}
\nodiff

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

\subsection{Lemmas}
\absentwhy{lemmas are user-given propositions. They are written usually to help
  theorem provers to establish validity of specifications. Thus they are mostly
  useful for verification activities based on deductive methods which are out of
  the scope of \eacsl. Furthermore, they often requires human help to be proven,
  although \eacsl targets are automatic tools}

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

\subsection{Inductive predicates}\label{sec:inductive}
\absentwhy{inductive predicates are not computable if they really use their
  inductive nature}

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

\subsection{Axiomatic definitions}
\absentwhy{by nature, an axiomatic is not computable}

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

\subsection{Polymorphic logic types}
\absentexperimental

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

\subsection{\notimplemented{Recursive logic definitions}}
\index{recursion}
\nodiff

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

\subsection{Higher-order logic constructions}
\absentexperimental

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

\subsection{Concrete logic types}\label{sec:concrete-logic-types}
\absentexperimental

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

\subsection{\notimplemented{Hybrid functions and predicates}}
\label{sec:logicalstates}
\index{hybrid!function}
\index{hybrid!predicate}
\nodiff

\difficultswhy{\notimplemented{Hybrid functions and predicates}}{the
  implementation of a memory model (or at least to support \lstinline|\\at|)}

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

\subsection{Memory footprint specification: \texorpdfstring{\lstinline|reads|}{reads} clause}
\absentexperimental

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

\subsection{\notimplemented{Specification Modules}}
\label{sec:specmodules}
\nodiff

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

\section{Pointers and physical adressing}
\label{sec:pointers}

\except{separation}

Figure~\ref{fig:gram:memory} shows the additional constructs for terms and
predicates which are related to memory location.
\begin{figure}[htbp]
  \fbox{\begin{minipage}{0.97\linewidth}
      \input{memory_modern.bnf}
    \end{minipage}}
  \caption{Grammar extension of terms and predicates about memory}
\label{fig:gram:memory}
\end{figure}

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

\subsection{Memory blocks and pointer dereferencing}
\label{subsec:memory}\label{sec:memory}
\nodiff

\difficultswhy{\lstinline|\\base\_addr|,
    \lstinline|\\block\_length|, \lstinline|\\valid|, 
    \lstinline|\\valid_read| and
    \lstinline|\\offset|}{the implementation of a memory model}

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

\subsection{Separation}\label{sec:separation}
\nodiff

\difficultswhy{\notimplemented{\lstinline|\\separated|}}{the implementation of a
  memory model}

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

\subsection{Allocation and deallocation}
\difficultswhy{All these constructs}{the implementation of a memory model}
\label{sec:alloc-dealloc}

\mywarning{this section is still almost experimental in \acsl. Thus it might still
evolve in the future.}

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

\section{Sets and lists}
\index{location}

\subsection{Finite sets}
\nodiff

\subsection{Finite lists}
\nodiff

Figure~\ref{fig:gram:list} shows the notations for built-in lists.
\begin{figure}[t]
  \begin{cadre}
      \input{list-gram.bnf}
    \end{cadre}
  \caption{Notations for built-in list datatype}
\label{fig:gram:list}
\end{figure}

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

\section{Abrupt termination}\label{sec:abrupt}
\absentexperimental

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

\section{Dependencies information}
\absentexperimental

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

\section{\notimplemented{Data invariants}}
\label{sec:invariants}
\index{data invariant}\index{global invariant}\index{type invariant}
\index{invariant!data}\index{invariant!global}\index{invariant!type}

\nodiff

Figure~\ref{fig:gram:datainvariants} summarizes grammar for declarations of data
invariants.
\begin{figure}[htbp]
  \fbox{\begin{minipage}{0.97\linewidth}
      \input{data_invariants_modern.bnf}
    \end{minipage}}
  \caption{Grammar for declarations of data invariants}
\label{fig:gram:datainvariants}
\end{figure}

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

\subsection{Semantics}
\nodiff

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

\subsection{\notimplemented{Model variables and model fields}}
\label{sec:model}
\index{model}

\nodiff

Figure~\ref{fig:gram:model} summarizes grammar for declarations of model
variables and fields.
\begin{figure}[htbp]
  \fbox{\begin{minipage}{0.97\linewidth}
      \input{model_modern.bnf}
    \end{minipage}}
  \caption{Grammar for declarations of model variables and fields}
\label{fig:gram:model}
\end{figure}

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

\section{Ghost variables and statements}
\label{sec:ghost}
\index{ghost}

\except{no specific construct for volatile variables}

Figure~\ref{fig:gram:ghost} summarizes grammar for ghost statements which is the
same than the one of \acsl.
\begin{figure}[htbp]
  \fbox{\begin{minipage}{0.98\linewidth}
      \input{ghost_modern.bnf}
    \end{minipage}}
  \caption{Grammar for ghost statements}
\label{fig:gram:ghost}
\end{figure}

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

\subsection{Volatile variables}
\absentexperimental

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

\section{Undefined values, dangling pointers}
\label{sec:dangling}
\nodiff

\difficultswhy{\lstinline|\\initialized| and
  \notimplemented{\lstinline|\\dangling|}}{the implementation of a memory
  model}

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

\section{Well-typed pointers}
\label{sec:typedpointers}
\absentexperimental