Commit fc7ed701 authored by MARCHE Claude's avatar MARCHE Claude

roadmap

parent 05cbaedd
......@@ -3,31 +3,49 @@
============ Long-term Roadmap (see below for roadmaps to next release) ===========
== projects ==
== long-term projects ==
* modules, raffinement, these de Leon
* modules, raffinement (these de Leon)
*
* support for higher-order
* extraction, more generally how to turn Why3 into a real programming language (these de Martin)
* internal interpreter, test of specifications, quickcheck
* BWare project, support for rewrite rules, improved support for provers,
extensions of set theory and their Coq realizations.
* LABCOM avec Adacore
** calculs non-linéaires, calculs en virgule flottante
** production de contre-exemples de preuves solides et exprimés dans le langage d’origine
** support efficace des invariants de données
** développer des composants réutilisables prouvés.
== Papers to write ==
* paper on the module system, its semantics, realizations, avec en
particulier la solution avec les types classes qui reste a
implanter
particulier la solution avec les types classes
* DONE paper on the proof management system
* DONE Encodings and transformations (Andrei+Francois FroCos 11)
* DONE Why presentation at the IVL workshop of CADE:
(http://research.microsoft.com/en-us/um/people/moskal/boogie2011/)
deadline: May 1st
* Caml code ?
* logic language for talking to provers
- DONE (Boogie 11)
- DONE FOL + poly (FroCos 11)
- alg + ind + rec ? + theories
* VACID-0
* system description (e.g. at CADE, TACAS)
* system description (e.g. at CADE, TACAS) DONE at ESOP
* rapports recherche ?
== stages ==
......@@ -35,8 +53,11 @@
* M1. preuve d'un petit compilateur, pas de pb de lieur,
eventuellement outils pour les preuves par recurrence
a la Leino, + fct size automatique
* M2. Lieur en Why3, POPLmark challenge. vers
un theorie et/ou un module réutilisable de lieurs
DONE (Stage M2 de Martin)
* (M2?) Stage Airbus, "TIP" avec Frama-C/Jessie ou WP/Why/Coq
besoin de la tactique Coq?
......@@ -51,7 +72,7 @@
* A true Jessie3 front-end
* Why3ML
- Fast WP a la Leino
- Fast WP a la Leino (DONE ?)
- assert qui ne donne pas une hypothese dans la suite -> "check"
also: in a black box
......@@ -118,13 +139,11 @@ Scheduled for 31 october 2013
== New Features to announce ==
* lemma functions
* polymorphic recursion permitted
* input language
** lemma functions
** polymorphic recursion permitted
* why.el renamed into why3.el
* new provers:
* new provers:
** veriT 201310
** Metitarski 2.2
** Metis 2.3
......@@ -133,40 +152,34 @@ Scheduled for 31 october 2013
** Yices2 2.0.4
* new versions of provers:
** Alt-Ergo 0.95.2
** Alt-Ergo 0.95.2
** CVC4 1.1 (& 1.2 ?)
** Coq 8.4pl2
** Coq 8.4pl2
** gappa 1.0.0
** SPASS 3.8ds
** SPASS 3.8ds
* API: more examples of use in examples/use_api/
* API: more examples of use
* emacs support: why.el renamed into why3.el
* why3session
** --stats: changed (detailler, temps, distinction root et subgoals, CLAUDE)
** --hist: TODO documenter (voir Alain ou Mohamed sur les graphes SMT)
* bug fix: PVS configuration and installation
* bug fix: leading zeros in decimal literals
* bug fix: PVS output, types are nonempty
* improved shape mecanism for session updates (see VSTTE'13 paper).
* bug fixes:
** remove leading zeros in decimal literals when needed by a prover
** PVS output: types are always non-empty
** PVS: fixed configuration and installation process
** improved shape mecanism for session updates (see VSTTE'13 paper).
Compatibility with session files from version 0.81 and earlier is
assured.
* bug fix: Coq tactic now loads dynamic plug-ins
* bug fix: Coq output of poly rec types
* BTS 15493, 15053
* BTS 13736 fixed
https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
** syntax highlighting bugs ?
some keywords are not colored in the bottom-right window
(but they are in the top-right window)
FIXED: it was caused by the language file for alt-ergo superseding the one for why3
** Coq tactic: now loads dynamic plug-ins
** Coq output: fixed printing of polymorphic recursive datatypes
** bug #15493: ?
** bug #15053: ?
** bug #13736: ?
** syntax highlighting bugs: should be fixed by removing old language
files from alt-ergo
== Final preparation ==
......@@ -245,10 +258,20 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* discriminate, mettre les bons arguments par defaut (ANDREI)
* tester avant la release sur
** BWare
** Prouveur de Martin
** examples de Frama-C/Jessie et Krakatoa
* eliminate_match: (apres la release ?)
** faire un cas particulier pour "bool", le match pouvant se traduire
vers ite qui est supporté par pas mal de prouveurs
** introduire des symboles _match non polymorphes differents pour
chaque instance necessaires. plutot qu'un seul symbole _match
poymorphe.
* efficiency issues
** understand problems when large number of goals (cf D Mentré examples)
** prouveur de Martin
** tester avant la release sur
*** BWare
*** Prouveur de Martin
*** examples de Frama-C/Jessie et Krakatoa
* Coq detection (et PVS) (CLAUDE, champ supplementaire compile_support = yes dans le prover-detection-data)
** refuser de detecter Coq si on n'a pas compilé avec le support de Coq
......@@ -257,25 +280,21 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* Coq tactic (CLAUDE, GUILLAUME, JCF, ANDREI)
** bug Prod(_,_,_) -> traiter le cas
* efficiency issues
- understand problems when large number of goals (cf D Mentré examples)
- prouveur de Martin
* Smoke detector and absurd: on pourrait mettre un label particulier
sur le "false" genéré par absurd, pour indiquer que c'est
intentionel que l'on veuille prouver false. FAIT
intentionel que l'on veuille prouver false. FAIT
Un tel cas pourrait etre
traité de facon speciale par le smoke detector avec option "deep",
pour eviter une fausse alarme.
PAS FAIT
* faire le menage dans les transformations d'induction : _int _ty
_ty_lex, FAIT et DOCUMENTER PAS FAIT
_ty_lex, FAIT et documenter PAS FAIT
* Documentation
- (ANDREI) make the glossary available
- (CLAUDE) complete api.tex: explain how to build/apply
transformations, write new functions on terms
transformations, write new functions on terms
- LEON: add a section "further reading"
* bug fix: 16454 (ne pas envoyer des triggers arithmetiques) (GUILLAUME)
......@@ -284,7 +303,7 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* support for new provers
** Alt-Ergo 0.95.2 DONE
** CVC4 1.2 TODO: pb avec les booleens
** CVC4 1.2 TODO: pb avec les booleens
** Coq 8.4pl2 TODO: probleme tactique Why3 ???
** Metitarski TODO: improve it (CLAUDE, GUILLAUME)
** others ?
......
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