Commit 3e43991f authored by MARCHE Claude's avatar MARCHE Claude

roadmap for next release

parent 5e795ba1
......@@ -46,9 +46,8 @@
+ suggested solution: replace model + filter_model by a custom model
(JC + ?)
=== Roadmap for next release ========================
== stages ==
* stages
** M1. preuve d'un petit compilateur, pas de pb de lieur,
eventuellement outils pour les preuves par recurrence
a la Leino, + fct size automatique
......@@ -57,8 +56,8 @@
** (M2?) Stage Airbus, "TIP" avec Frama-C/Jessie ou WP/Why/Coq
besoin du plugin Coq?
* INSTALLATION
** configure.in: detect dynlink.cmxa, and switch to bytecode if not found
=== release d'apres ==========================================
* PRIORITAIRE, JCF et ANDREI, clone de module
** demarche: ecrire une API avec smart constructors garantissant
......@@ -70,30 +69,69 @@ NON PRIORITAIRE ?
** ghost code
** logic symbols used in programs
* extraction vers Caml
** PRIORITAIRE, JCF, ANDREI
* FRANCOIS new tools
** merge why3html and why3stats into a new executable why3report
** move -latex from why3replayer to why3report
** document why3report
* Coq plugin
* Coq output
** corriger l'incoherence, comprendre si on veut vraiment accepter
function x : 'a
(cf: en caml cela ne marche pas)
* efficiency issues
** understand problems when large number of goals (cf D Mentré examples)
** also: BTS 13736
https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
=== Roadmap for next release ========================
== Nouveautés importantes ==
* Realisation Coq
* tool why3session avec -latex, -html, -stats, etc
* tool why3doc
* several versions of the same prover
* Improved IDE: left scrollbar, font enlargement, etc.
TODOS:
* Documentation
** GM Realisations Coq, comment fait l'utilisateur pour faire ses realisations
ne pas oublier de dire que les dependances avec le .why ou .mlw: ne sera pas vérifié
** ??? revoir documentation du smoke detector
** Documenter l'utilisation de plusieurs version du meme prouveur comme CVC3 et Z3
** CLAUDE Documenter les popups qui peuvent apparaitre dans why3ide quand les prouveurs ont changé
ET LES METTRE AU POINT
*** ANDREI ajouter option a why3config pour ajouter association ident-executable
*** CLAUDE meme ordre d'idee: ne pas ecraser "default editor" et "timelimit"
** complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
** complete manpages.tex: section "Drivers of external provers" (A+F)
** make the glossary available
* CM why3session
** passe sur la documentation ecrite par Francois reecrite par Guillaume
** option -latex et -html deplacé de why3replayer vers why3session
** reprendre une partie de src/ide/stats.ml, et virer executable why3stats
* FRANCOIS
** document smoke detector
* CLAUDE provers
** fix support for newer Z3, CVC3 and Alt-Ergo, allow several version
of them at the same time. Allow why3config --detect to find e.g z3
under names like z3-3.2 (how ? command-line option ? e.g. -p z3 /usr/local/bin/z3-3.2)
** Ensure that we kill a prover after some time (ressurect %T ? with a
* JCF renommer why3html en why3doc
** rajouter les liens
** mettre bibliotheque standard de Why3 en HTML, sur le site Web
* provers
** CLAUDE Ensure that we kill a prover after some time (ressurect %T ? with a
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
** ANDREI 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
* DONE, move Session module and its dependencies into the Why3 library
** but avoid duplication with session_ro
** avoid also duplication of type like prover_data record
** do not include task and transf in the data type, so that
......@@ -101,37 +139,16 @@ NON PRIORITAIRE ?
** session + session_ro -> session_data + session_dynamic
* efficiency issues
** understand problems when large number of goals (cf D Mentré examples)
** also: BTS 13736
https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* ALL fix bug and update the BTS
** reject global "val"s in typing environment for logic decls.
* DELAYED Coq plugin
* Coq realization of theories
** corriger l'incoherence, comprendre si on veut vraiment accepter
function x : 'a
(cf: en caml cela ne marche pas)
** make it really usable
** understand problems when trying to realize set.why.
Status of equality, relation with clone module feature
* DOC:
** document new tools why3stats and others if any
** complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
** complete manpages.tex: section "Drivers of external provers" (A+F)
** make the glossary available
* IDE:
** enlarge font (menu + shortcut Ctrl-+)
* CM IDE:
** DONE enlarge font (menu + shortcut Ctrl-+)
** Ctrl-A to select all rows
** commentaires dans les sessions, attachés a chaque ligne
** BTS: Refreshing the IDE pane for prover output
** Do not save if not needed
** ne pas ecrire saving sessions si on ne sauve pas la session
** saving session
* add "ctrl-S" to save the session explicitly
(partially done, but no shortcut)
......@@ -142,7 +159,7 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
** syntax highlighting
some keywords are not colored in the bottom-right window
(but they are in the top-right window)
** add a scrollbar for the left panel
** DONE add a scrollbar for the left panel
=== Roadmap for release 0.71 ========================
......
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
Parameter param : Type.
Parameter infix_ls: Z -> Z -> Prop.
Definition infix_lseq(x:Z) (y:Z): Prop := (infix_ls x y) \/ (x = y).
Parameter infix_pl: Z -> Z -> Z.
Parameter prefix_mn: Z -> Z.
Parameter infix_as: Z -> Z -> Z.
Axiom Unit_def : forall (x:Z), ((infix_pl x 0%Z) = x).
Axiom Assoc : forall (x:Z) (y:Z) (z:Z), ((infix_pl (infix_pl x y)
z) = (infix_pl x (infix_pl y z))).
Axiom Inv_def : forall (x:Z), ((infix_pl x (prefix_mn x)) = 0%Z).
Axiom Comm : forall (x:Z) (y:Z), ((infix_pl x y) = (infix_pl y x)).
Axiom Assoc1 : forall (x:Z) (y:Z) (z:Z), ((infix_as (infix_as x y)
z) = (infix_as x (infix_as y z))).
Axiom Mul_distr : forall (x:Z) (y:Z) (z:Z), ((infix_as x (infix_pl y
z)) = (infix_pl (infix_as x y) (infix_as x z))).
Definition infix_mn(x:Z) (y:Z): Z := (infix_pl x (prefix_mn y)).
Axiom Comm1 : forall (x:Z) (y:Z), ((infix_as x y) = (infix_as y x)).
Axiom Unitary : forall (x:Z), ((infix_as 1%Z x) = x).
Axiom NonTrivialRing : ~ (0%Z = 1%Z).
Axiom Refl : forall (x:Z), (infix_lseq x x).
Axiom Trans : forall (x:Z) (y:Z) (z:Z), (infix_lseq x y) -> ((infix_lseq y
z) -> (infix_lseq x z)).
Axiom Antisymm : forall (x:Z) (y:Z), (infix_lseq x y) -> ((infix_lseq y x) ->
(x = y)).
Axiom Total : forall (x:Z) (y:Z), (infix_lseq x y) \/ (infix_lseq y x).
Axiom CompatOrderAdd : forall (x:Z) (y:Z) (z:Z), (infix_lseq x y) ->
(infix_lseq (infix_pl x z) (infix_pl y z)).
Axiom CompatOrderMult : forall (x:Z) (y:Z) (z:Z), (infix_lseq x y) ->
((infix_lseq 0%Z z) -> (infix_lseq (infix_as x z) (infix_as y z))).
Parameter pr: param -> Z -> Prop.
Parameter num_of: param -> Z -> Z -> Z.
Axiom Num_of_empty : forall (p:param) (a:Z) (b:Z), (infix_lseq b a) ->
((num_of p a b) = 0%Z).
Axiom Num_of_right_no_add : forall (p:param) (a:Z) (b:Z), (infix_ls a b) ->
((~ (pr p (infix_mn b 1%Z))) -> ((num_of p a b) = (num_of p a (infix_mn b
1%Z)))).
Axiom Num_of_right_add : forall (p:param) (a:Z) (b:Z), (infix_ls a b) ->
((pr p (infix_mn b 1%Z)) -> ((num_of p a b) = (infix_pl 1%Z (num_of p a
(infix_mn b 1%Z))))).
Theorem Num_of_non_negative : forall (p:param) (a:Z) (b:Z), (infix_lseq 0%Z
(num_of p a b)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros p a b.
assert (h: (a > b \/ a <= b)%Z) by omega.
destruct h.
rewrite Num_of_empty; auto with zarith.
admit. admit.
generalize H; clear H.
generalize b; clear b.
apply Zlt_lower_bound_ind.
intros b Hind Hab.
assert (h: (a = b \/ a < b)%Z) by omega.
destruct h.
rewrite Num_of_empty; auto with zarith.
admit. admit.
assert (h: (pr p (b - 1) \/ ~ pr p (b - 1))%Z).
admit.
destruct h.
rewrite Num_of_right_add; auto with zarith.
admit. admit. admit.
rewrite Num_of_right_no_add; auto with zarith.
admit. admit. admit.
Qed.
(* DO NOT EDIT BELOW *)
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