[e-acsl:doc] update wrt \sum, \prod, and \numof

src/plugins/e-acsl/doc/refman/changes_modern.tex

@@ -176,26 +176,32 @@ in \lstinline|\\at|}
 
 \subsection*{Version \eacslplugincodename-\eacslpluginversion}
 \begin{itemize}
+\item \changeinsection{higherorder}{support for \lstinline|\\sum|,
+  \lstinline|\\prod|, and \lstinline|\\numof|}
+\end{itemize}
+ 
+\subsection*{Version Vanadium-23}
+\begin{itemize}
 \item \changeinsection{expressions}{mark logic function and predicate
   applications as implemented}
-\item \changeinsection{fn-behavior}{mark admit and check clauses as implemented}
-\item \changeinsection{loop_annot}{mark loop variants as implemented}
+\item \changeinsection{fn-behavior}{support for admit and check clauses}
+\item \changeinsection{loop_annot}{support for loop variants}
 \end{itemize}
 
 \subsection*{Version Titanium-22}
 
 \begin{itemize}
-\item \changeinsection{expressions}{support of bitwise operations}
-\item \changeinsection{aggregates}{support of logic arrays}
+\item \changeinsection{expressions}{support for bitwise operations}
+\item \changeinsection{aggregates}{support for logic arrays}
 \end{itemize}
 
 \subsection*{Version Scandium-21}
 
 \begin{itemize}
-\item \changeinsection{reals}{support of rational numbers and operations}
+\item \changeinsection{reals}{support for rational numbers and operations}
 \item \changeinsection{fn-behavior}{remove abrupt clauses from the list of
   exceptions}
-\item \changeinsection{fn-behavior}{support of \lstinline|complete behaviors|
+\item \changeinsection{fn-behavior}{support for \lstinline|complete behaviors|
   and \lstinline|disjoint behaviors|}
 \item \changeinsection{statement_contract}{remove abrupt clauses from the list
   of exceptions}
@@ -205,45 +211,45 @@ in \lstinline|\\at|}
 \subsection*{Version Potassium-19}
 
 \begin{itemize}
-\item \changeinsection{logicspec}{support of logic functions and predicates}
+\item \changeinsection{logicspec}{support for logic functions and predicates}
 \end{itemize}
 
 \subsection*{Version Argon-18}
 
 \begin{itemize}
-\item \changeinsection{at}{support of \lstinline|\\at| on purely
+\item \changeinsection{at}{support for \lstinline|\\at| on purely
 logic variables}
-\item \changeinsection{locations}{support of ranges in memory built-ins
+\item \changeinsection{locations}{support for ranges in memory built-ins
   (e.g. \lstinline|\\valid| or \lstinline|\\initialized|)}
 \end{itemize}
 
 \subsection*{Version Chlorine-20180501}
 
 \begin{itemize}
-\item \changeinsection{expressions}{support of \lstinline|\\let| binding}
+\item \changeinsection{expressions}{support for \lstinline|\\let| binding}
 \end{itemize}
 
 \subsection*{Version 0.5}
 
 \begin{itemize}
-\item \changeinsection{alloc-dealloc}{support of \lstinline|\\freeable|}
+\item \changeinsection{alloc-dealloc}{support for \lstinline|\\freeable|}
 \end{itemize}
 
 \subsection*{Version 0.3}
 
 \begin{itemize}
-\item \changeinsection{loop_annot}{support of loop invariant}
+\item \changeinsection{loop_annot}{support for loop invariant}
 \end{itemize}
 
 \subsection*{Version 0.2}
 
 \begin{itemize}
-\item \changeinsection{expressions}{support of bitwise complementation}
-\item \changeinsection{memory}{support of \lstinline|\\valid|}
-\item \changeinsection{memory}{support of \lstinline|\\block_length|}
-\item \changeinsection{memory}{support of \lstinline|\\base_addr|}
-\item \changeinsection{memory}{support of \lstinline|\\offset|}
-\item \changeinsection{dangling}{support of \lstinline|\\initialized|}
+\item \changeinsection{expressions}{support for bitwise complementation}
+\item \changeinsection{memory}{support for \lstinline|\\valid|}
+\item \changeinsection{memory}{support for \lstinline|\\block_length|}
+\item \changeinsection{memory}{support for \lstinline|\\base_addr|}
+\item \changeinsection{memory}{support for \lstinline|\\offset|}
+\item \changeinsection{dangling}{support for \lstinline|\\initialized|}
 \end{itemize}
 
 \subsection*{Version 0.1}

src/plugins/e-acsl/doc/refman/higherorder.tex

 \begin{syntax}
-term ::= { "\lambda" binders ";" term } ; abstraction
-| { ext-quantifier "(" term "," term "," term ")" };
+term ::= "\lambda" binders ";" term ; abstraction
+| ext-quantifier "(" term "," term "," term ")" ;
 | { "{" term "\with" "[" range "]" "=" term "}" } ;
 \
-{ ext-quantifier } ::= { "\max" } | { "\min" } | { "\sum" };
-                       | { "\product" } | { "\numof" }
+ext-quantifier ::= { "\max" } | { "\min" } | "\sum" ;
+                 | "\product" | "\numof"
 \end{syntax}

src/plugins/e-acsl/doc/refman/intro_modern.tex

@@ -52,7 +52,8 @@ currently implemented into the \framac's \eacsl plug-in.
       & built-in function \lstinline|\\length| over arrays \\
       & conversions of structure to structure \\
       & t-sets \\
-      & higher-order logic constructs \\
+      & abstractions \\
+      & \lstinline|\\max| and \lstinline|\\min| \\
       & hybrid functions \\
       & labeled memory-related built-in functions \\
       & finite sets \\

src/plugins/e-acsl/doc/refman/speclang_modern.tex

@@ -736,7 +736,7 @@ through semantic criteria.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{\notimplemented{Higher-order logic constructions}}
+\subsection{Higher-order logic constructions}
 \label{sec:higherorder}
 
 \experimental
@@ -754,6 +754,9 @@ higher-order logic.
 \label{fig:gram:higherorder}
 \end{figure}
 
+{\highlightnotimplemented Abstractions are only implemented for extended
+  quantifiers, such as the term \lstinline|\sum(1, 10, \lambda integer k; k)|.}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{\notimplemented{Concrete logic types}}