From 028b948d7075d7ebd057892156dd0c9a52e46901 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 7 Oct 2021 12:42:36 +0200
Subject: [PATCH] [e-acsl:doc] update wrt \sum, \prod, and \numof
---
.../e-acsl/doc/refman/changes_modern.tex | 42 +++++++++++--------
src/plugins/e-acsl/doc/refman/higherorder.tex | 8 ++--
.../e-acsl/doc/refman/intro_modern.tex | 3 +-
.../e-acsl/doc/refman/speclang_modern.tex | 5 ++-
4 files changed, 34 insertions(+), 24 deletions(-)
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index b37bb6f30da..770c70c1af1 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/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}
diff --git a/src/plugins/e-acsl/doc/refman/higherorder.tex b/src/plugins/e-acsl/doc/refman/higherorder.tex
index cc4d91104bc..838bef143f9 100644
--- a/src/plugins/e-acsl/doc/refman/higherorder.tex
+++ b/src/plugins/e-acsl/doc/refman/higherorder.tex
@@ -1,8 +1,8 @@
\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}
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index 328721a32e7..e6b55954335 100644
--- a/src/plugins/e-acsl/doc/refman/intro_modern.tex
+++ b/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 \\
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 95b64e165d0..8adb8844f77 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/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}}
--
GitLab