Skip to content
Snippets Groups Projects
Commit 8c497fbf authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl:doc] Update reference manual to add support of complete and disjoint behavior

parent dfdaaf67
No related branches found
No related tags found
No related merge requests found
......@@ -137,6 +137,8 @@ in \lstinline|\\at|}
\item \changeinsection{reals}{support of 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|
and \lstinline|disjoint behaviors|}
\item \changeinsection{statement_contract}{remove abrupt clauses from the list
of exceptions}
\item \changeinsection{abrupt}{add grammar for abrupt termination}
......
\begin{syntax}
[ function-contract ] ::= requires-clause*
{ decreases-clause? } simple-clause*
named-behavior* { completeness-clause* }
named-behavior* completeness-clause*
\
requires-clause ::= "requires" pred ";"
\
......@@ -24,6 +24,6 @@
\
assumes-clause ::= "assumes" pred ";"
\
{ completeness-clause } ::= { "complete" "behaviors" (id (","id)*)? ";" } ;
| { "disjoint" "behaviors" (id (","id)*)? ";" }
completeness-clause ::= "complete" "behaviors" (id (","id)*)? ";"
| "disjoint" "behaviors" (id (","id)*)? ";"
\end{syntax}
......@@ -70,8 +70,7 @@ currently implemented into the \framac's \eacsl plug-in.
& assigns \\
& allocates \\
& decreases \\
& abrupt termination \\
& complete and disjoint behaviors
& abrupt termination
\\
\hline
\end{tabular}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment