Commit e48f9e16 authored by MARCHE Claude's avatar MARCHE Claude

roadmap: a few features suggested by AstraVer people

parent 0799cf0d
......@@ -155,6 +155,10 @@ Release Notes (details in file CHANGES):
== TODO ==
* fix (<>) not allowed as prefix form
* support for tuple types in detect_polymorphism ?
* integrate server feature done by Johannes
* Coq realization of bitvector theory
......@@ -167,6 +171,28 @@ Release Notes (details in file CHANGES):
* take some time to fix some bugs of the BTS: 18029 at least
* use the file generated by altgr-ergo to replay proofs edited by altgr-ergo
alt-ergo -replay <file>.agr
* make the strategy feature public and documented. Possibly generate
default stratregies dynamically at the time of why3 config --detect,
using the provers detected : for that, we can annotated the provers in
prover-detection-data.conf to tell if they should be used in the strategies,
with which priority
2 possible default strategies
. favor use of many prover before splitting or increading timeout
. or, on the contrary, favor splitting
. or, favor timelimt increase...
==================== Roadmap for release 0.86 ========================
DATE : fin avril / début mai
......
......@@ -12,12 +12,13 @@ module M
val y "model" "model_projected" "model_trace:y" :ref int
let incr ( x "model" "model_trace:x" : ref int ): unit
ensures { !x = old !x + 2 + !y }
=
y := !y + 1;
x := !x + 1;
x := !x + 1
let incr ( x23 "model" "model_trace:my_x" : ref int ): unit
ensures { !x23 = old !x23 + 2 + !y }
=
#"/home/cmarche/recherche/why/tests/c/binary_search.c" 62 27 32#
y := !y + 1;
x23 := !x23 + 1;
x23 := !x23 + 1
let test_loop ( x "model" "model_trace:x" : ref int ): unit
ensures { !x < old !x }
......
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