Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
fd7e592c
Commit
fd7e592c
authored
Oct 26, 2011
by
MARCHE Claude
Browse files
updated roadmap
parent
5dc73a2e
Changes
3
Hide whitespace changes
Inline
Side-by-side
ROADMAP
View file @
fd7e592c
...
...
@@ -39,28 +39,25 @@
* system description (e.g. at CAD, TACAS)
* rapports recherche ?
* choose a logo -> done ?
* Coq plugin
* Coq realization of theories
* prover support
** avoid bug of CVC3, e.g in examples/my_cosine.why
** understand bug reports 12792-12794 and 12907
* IDE:
** edition, navigation (partially done)
** restore provers detection in the middle of a session.
+ todo: run detection immediately at start up if conf file absent or
outdated
** reimplement "hide proved goals" feature
+ suggested solution: replace model + filter_model by a custom model
(JC + ?)
** saving session
* DONE add a "cancel" choice in the "ask" window
* add "ctrl-S" to save the session explicitly
(partially done, but no shortcut)
=== Roadmap for next release ========================
* update the BTS
* API for programs
* reject global "val"s in typing environment for logic decls.
* move session.ml and its dependencies into the Why3 lib
* Coq plugin
* Coq realization of theories
* DOC:
** complete api.tex: explain how to build theories, apply
...
...
@@ -68,10 +65,18 @@
** complete manpages.tex: section "Drivers of external provers" (A+F)
** make the glossary available
* IDE:
** saving session
* add "ctrl-S" to save the session explicitly
(partially done, but no shortcut)
** restore provers detection in the middle of a session.
+ todo: run detection immediately at start up if conf file absent or
outdated
=== Roadmap for release 0.71 ========================
* Final preparation:
*
DONE
Final preparation:
** put on the web page
*** why3-0.71.tar.gz
*** manual in PDF: check that macro \todo is commented out
...
...
tests/test-claude.mlw
0 → 100644
View file @
fd7e592c
module M
use import module ref.Ref
val x : ref int
axiom A : !x = 0
axiom B : (old !x) = 0
let f (n:int) : unit =
{ }
x := n
{ !x = 1 /\ (old !x) = 2 }
end
\ No newline at end of file
tests/test-claude.why
View file @
fd7e592c
theory TestProp
goal Test0 : true
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment