Commit d8902fc0 authored by Julien Signoles's avatar Julien Signoles
Browse files

[doc] update reference manual wrt support of rationals

parent eb10aa7b
19.0
\ No newline at end of file
19.0+dev
......@@ -9,7 +9,7 @@
logic-type-expr ::= built-in-logic-type ;
| id ; type identifier
\
built-in-logic-type ::= "boolean" | "integer" | { "real" }
built-in-logic-type ::= "boolean" | "integer" | "real"
\
variable-ident ::= id
| "*" variable-ident ;
......
......@@ -125,6 +125,13 @@ in \lstinline|\\at|}
\section{Changes in \eacsl Implementation}
\subsection*{Version \eacslversion}
\begin{itemize}
\item \changeinsection{reals}{support of rational numbers and operations}
\end{itemize}
\subsection*{Version Potassium-19}
\begin{itemize}
\item \changeinsection{logicspec}{support of logic functions and predicates}
\end{itemize}
......
\chapter{Libraries}
\label{chap:lib}
\emph{Disclaimer:} this chapter is yet empty. It is left here to give an idea of
what the final document will look and to be consistent with the \acsl reference
manual~\cite{acsl}.
\emph{Disclaimer:} this chapter is empty on purpose. It is left here to be
consistent with the \acsl reference manual~\cite{acsl}.
......@@ -45,12 +45,6 @@ only difference between \eacsl and \acsl predicates are quantifications.
\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.
......@@ -260,10 +254,17 @@ It is not possible to define logic types introduced by the specification writer
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{\notimplemented{Real numbers} and floating point numbers}
\subsection{Real numbers and floating point numbers}
\label{sec:reals}
\nodiff
\difficults{\notimplemented{Exact real numbers} and even floating point numbers}
\difficults{Exact real numbers and even floating point numbers}
\begin{notimplementedenv}
Real numbers beyond rationals are currently not supported by the \eacsl
plug-in. Only rationals (in $\mathbb{Q}$) and floating point numbers are
supported.
\end{notimplementedenv}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment