Commit 5839c12a authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

updated roadmap

parent f222029e
......@@ -23,6 +23,9 @@
commande why3 et why3bench + le path
* Add more examples in the regression tests and in the proval gallery
** add all examples from the VSTTE 2012 competition (JCF, ANDREI)
* A literate programming tool for Why3 (JCF)
* Papers to write
......@@ -65,7 +68,7 @@ NON PRIORITAIRE ?
** logic symbols used in programs
* extraction vers Caml
** PRIORITAIRE, JCF, ANDREI, besoin pour cours aux JFLA en janvier 2012
* FRANCOIS new tools
** merge why3html and why3stats into a new executable why3report
......@@ -83,6 +86,9 @@ NON PRIORITAIRE ?
meaning like twice the value of %t ?), because we cannot be sure they always
honor their own -timeout option.
** fix CVC3 printer: prints predicate def using LAMBDA
** better use of Alt-Ergo's builtin theories: records, enumeration types
(Alt-Ergo >= 0.94) => at least two drivers for Alt-Ergo, depending on its
version number
* FRANCOIS CLAUDE, move Session module and its dependencies into the Why3 library
** but avoid duplication with session_ro
Supports Markdown
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