Commit 0497d13d authored by MARCHE Claude's avatar MARCHE Claude

preparation for release 0.73. PVS features commented out

parent 00ba3ec8
......@@ -64,11 +64,6 @@
* replayer
** deplacer option -bench dans une commande de why3session
* Sortie PVS
** avec mecanisme de realization
* Yices 2 ? interesserait Cesar
* Projets interessant Cesar ?
** Preuve de prog flottants avec Frama-C+WP+Why3+PVS
** Generation d'annotations
......@@ -76,17 +71,6 @@
interval_arith.c. Completer la galerie
** preuve sur l'assembleur
* PRIORITAIRE, JCF et ANDREI, clone de module
- demarche: ecrire une API avec smart constructors garantissant
le bon typage, et clone sera en premier lieu un de ces constructors
- cas d'utilisation: range d'entiers de Jessie, Flottants -> double ou single
containeurs pour Adacore et Claire
- NON PRIORITAIRE ?
+ regions : strong update
+ ghost code
+ logic symbols used in programs
* extraction vers Caml
- PRIORITAIRE, JCF, ANDREI
......@@ -104,13 +88,6 @@
* Coq tactic
** ajout de bases de hint
* PRIORITAIRE Coq output
- corriger l'incoherence, comprendre si on veut vraiment accepter
function x : 'a
(cf: en caml cela ne marche pas)
Solution proposee: utiliser des types classes, en particulier Inhabited
* efficiency issues
- understand problems when large number of goals (cf D Mentré examples)
- also: BTS 13736
......@@ -122,16 +99,6 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
traité de facon speciale par le smoke detector avec option "deep",
pour eviter une fausse alarme.
* Documentation
- (ANDREI) make the glossary available
- (CLAUDE) complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
* Contre-exemples de Alt-Ergo
* detect editors
*** check if coqide and also emacs/proof-general is installed
* IDE
** todo: run detection immediately at start up if conf file absent or
outdated. should become doable with the new Session module
......@@ -143,10 +110,51 @@ 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.
==================== Roadmap for release 0.74 ========================
scheduled on Sep 2012
* Sortie PVS
** avec mecanisme de realization
* Yices 2 ? interesserait Cesar
* mettre au propre les loc des fichiers de sessions, en particulier
les noms de fichiers doivent etre relatifs au fichier de session
lui-meme. Utiliser Sysutil.relativize_filename a bon escient.
* Contre-exemples de Alt-Ergo
* detect editors
*** check if coqide and also emacs/proof-general is installed
* Documentation
- (ANDREI) make the glossary available
- (CLAUDE) complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
* PRIORITAIRE Coq output
- corriger l'incoherence, comprendre si on veut vraiment accepter
function x : 'a
(cf: en caml cela ne marche pas)
Solution proposee: utiliser des types classes, en particulier Inhabited
* PRIORITAIRE, JCF et ANDREI, clone de module
- demarche: ecrire une API avec smart constructors garantissant
le bon typage, et clone sera en premier lieu un de ces constructors
- cas d'utilisation: range d'entiers de Jessie, Flottants -> double ou single
containeurs pour Adacore et Claire
- NON PRIORITAIRE ?
+ regions : strong update
+ ghost code
+ logic symbols used in programs
==================== Roadmap for release 0.73 ========================
== New Features to announce ==
......
\subsection{PVS}
When a PVS file is regenerated, the old version is split into chunks,
according to blank lines. Chunks corresponding to \why declarations
are identified with a comment starting with \verb+% Why3+, \eg
\begin{verbatim}
% Why3 f
f(x: int) : int
\end{verbatim}
Other chunks are considered to be user PVS declarations.
Thus a comment such as \verb+% Why3 f+ must not be removed;
otherwise, there will be two
declarations for \texttt{f} in the next version of the file (one being
regenerated and another one considered to be a user-edited chunk).
The user is allowed to perform the following actions on a PVS
realization:
\begin{itemize}
\item give a definition to an uninterpreted symbol (type, function, or
predicate symbol), by adding an equal sign (\texttt{=}) and a
right-hand side to the definition. When the declaration is
regenerated, the left-hand side is updated and the right-hand side
is reprinted as is. In particular, the names of a function or
predicate arguments should not be modified. In addition, the
\texttt{MACRO} keyword may be inserted and it will be kept in
further generations.
\item turn an axiom into a lemma, that is to replace the PVS keyword
\texttt{AXIOM} with either \texttt{LEMMA} or \texttt{THEOREM}.
\item insert anything between generated declarations, such as a lemma,
an extra definition for the purpose of a proof, etc.
\end{itemize}
\why makes some effort to merge the new declarations with the old ones
and with the user chunks. If it happens that some chunks could not be
merged, they are appended at the end of the file, in comments.
......@@ -7,7 +7,8 @@ some of its uninterpreted symbols and proofs for some of its
axioms. This way, one can show the consistency of an axiomatized
theory and/or make a connection to an existing library (of the proof
assistant) to ease some proofs.
Currently, realizations are supported for the proof assistants Coq and PVS.
Currently, realizations are supported only for the proof assistant Coq.
% Currently, realizations are supported for the proof assistants Coq and PVS.
\section{Generating a realization}
......@@ -87,42 +88,7 @@ much about comments. For instance, \why can easily be confused by
some terminating directive like \verb+Qed+ that would be present in a
comment.
\subsection{PVS}
When a PVS file is regenerated, the old version is split into chunks,
according to blank lines. Chunks corresponding to \why declarations
are identified with a comment starting with \verb+% Why3+, \eg
\begin{verbatim}
% Why3 f
f(x: int) : int
\end{verbatim}
Other chunks are considered to be user PVS declarations.
Thus a comment such as \verb+% Why3 f+ must not be removed;
otherwise, there will be two
declarations for \texttt{f} in the next version of the file (one being
regenerated and another one considered to be a user-edited chunk).
The user is allowed to perform the following actions on a PVS
realization:
\begin{itemize}
\item give a definition to an uninterpreted symbol (type, function, or
predicate symbol), by adding an equal sign (\texttt{=}) and a
right-hand side to the definition. When the declaration is
regenerated, the left-hand side is updated and the right-hand side
is reprinted as is. In particular, the names of a function or
predicate arguments should not be modified. In addition, the
\texttt{MACRO} keyword may be inserted and it will be kept in
further generations.
\item turn an axiom into a lemma, that is to replace the PVS keyword
\texttt{AXIOM} with either \texttt{LEMMA} or \texttt{THEOREM}.
\item insert anything between generated declarations, such as a lemma,
an extra definition for the purpose of a proof, etc.
\end{itemize}
\why makes some effort to merge the new declarations with the old ones
and with the user chunks. If it happens that some chunks could not be
merged, they are appended at the end of the file, in comments.
% \input{./pvs.tex}
\section{Shipping libraries of realizations}
......@@ -141,3 +107,10 @@ driver="path/to/extra_coq.drv"
This file can be passed to \why thanks to the \verb+--extra-config+
option.
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
......@@ -346,19 +346,19 @@ command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3
driver = "drivers/coq.drv"
editor = "coqide"
[ITP pvs]
name = "PVS"
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
version_ok = "5.0"
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-check-pvs %l %f"
driver = "drivers/pvs.drv"
editor = "pvs"
# [ITP pvs]
# name = "PVS"
# exec = "pvs"
# version_switch = "-version"
# version_regexp = "PVS Version \\([^ \n]+\\)"
# version_ok = "5.0"
# command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-check-pvs %l %f"
# driver = "drivers/pvs.drv"
# editor = "pvs"
[editor pvs]
name = "PVS"
command = "@LOCALBIN@why3-call-pvs %l %f"
# [editor pvs]
# name = "PVS"
# command = "@LOCALBIN@why3-call-pvs %l %f"
[editor coqide]
name = "CoqIDE"
......
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