Commit 5f92d65f authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update the roadmap. Make sure the TODO don't go unnoticed.

parent ecfa4816
......@@ -114,9 +114,6 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* (JCF) reject global "val"s in typing environment for logic decls.
* documentation
** avoir une version html et la mettre sur le web
* sessions
** mettre la dtd sur le web et changer l'entête des sessions pour qu'elles
pointent dessus
......@@ -166,6 +163,7 @@ Bug fixes:
* check the file CHANGES, add the release date
* manual in PDF: check that macro \todo is commented out
in ./macros.tex, and then "make doc"
* manual in HTML: "make doc/html/index.html"
* do "make distrib"
* test the distrib why3-0.74.tar.gz
* make a last commit:
......@@ -174,6 +172,7 @@ Bug fixes:
* put on the web page
- why3-0.74.tar.gz
- the HTML version of the manual (content of doc/html)
- why3session.dtd
- standard library online, using why3doc, to http://why3.lri.fr/stdlib/
(make stdlibdoc ;
......
......@@ -22,7 +22,7 @@ extended with
%\item Hilbert's epsilon construct
\end{itemize}
TODO: continue
\todo{continue}
\section{Organization of this document}
......
% \newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
\newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
\newcommand{\why}{\textsf{Why3}\xspace}
\newcommand{\whyml}{\textsf{WhyML}\xspace}
......
......@@ -82,7 +82,7 @@
\vfill
% \todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
\todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
%BEGIN LATEX
\begin{LARGE}
......
......@@ -198,39 +198,39 @@ In the following we describe the informal semantics of each constructs, and prov
\subsubsection{Constant expressions}
Integer and real constants are as in the logic language
TODO
\todo{Integer and real constants are as in the logic language}
\subsubsection{Unary and Binary Operators}
\todo{}
\subsubsection{Array accesses and updates, fields access and updates}
TODO
\todo{}
\subsubsection{Let binding, sequences}
TODO
\todo{}
\subsubsection{Function definition}
TODO: fun, let rec
\todo{fun, let rec}
\subsubsection{Function call}
TODO
\todo{}
\subsubsection{Exception throwing and catching}
TODO: raise, try with end
\todo{raise, try with end}
\subsubsection{Conditional expression, pattern matching}
if then else. Discuss standard WP versus fast WP
\todo{if then else. Discuss standard WP versus fast WP}
\subsubsection{Loops}
while, loop, for
\todo{while, loop, for}
\subsubsection{Assertions, Code Contracts}
......@@ -289,7 +289,7 @@ The corresponding rules for computing WP are as follows:
\end{array}
\]
TODO ? sandbox:
\todo{? sandbox:}
\[
WP(\texttt{sandbox}~e, Q) = WP(e,true) \land Q
\]
......@@ -297,7 +297,7 @@ WP(\texttt{sandbox}~e, Q) = WP(e,true) \land Q
\subsubsection{Labels, old, at}
TODO
\todo{}
\subsection{Modules}
......
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