Commit 8a6c1483 authored by MARCHE Claude's avatar MARCHE Claude

add a few things in roadmap

parent d5670dc8
...@@ -8,6 +8,8 @@ ...@@ -8,6 +8,8 @@
particulier la solution avec les types classes qui reste a particulier la solution avec les types classes qui reste a
implanter implanter
* paper on the proof management system
* DONE Encodings and transformations (Andrei+Francois FroCos 11) * DONE Encodings and transformations (Andrei+Francois FroCos 11)
* DONE Why presentation at the IVL workshop of CADE: * DONE Why presentation at the IVL workshop of CADE:
(http://research.microsoft.com/en-us/um/people/moskal/boogie2011/) (http://research.microsoft.com/en-us/um/people/moskal/boogie2011/)
...@@ -17,9 +19,8 @@ ...@@ -17,9 +19,8 @@
- DONE (Boogie 11) - DONE (Boogie 11)
- DONE FOL + poly (FroCos 11) - DONE FOL + poly (FroCos 11)
- alg + ind + rec ? + theories - alg + ind + rec ? + theories
* proof sessions
* VACID-0 * VACID-0
* system description (e.g. at CAD, TACAS) * system description (e.g. at CADE, TACAS)
* rapports recherche ? * rapports recherche ?
== stages == == stages ==
...@@ -155,7 +156,8 @@ Bug fix: ...@@ -155,7 +156,8 @@ Bug fix:
/users/www-perso/projets/why3/api ) /users/www-perso/projets/why3/api )
- update the main HTML page (sources are in why3-papers/www) - update the main HTML page (sources are in why3-papers/www)
* produce the Why3 part of ProVal gallery ? * produce the Why3 part of ProVal gallery
-> add also a ZIP file of it
* Announce the distrib * Announce the distrib
- What to put in the announcement: see New Features above - What to put in the announcement: see New Features above
* The next commit : add +git to the version in file Version * The next commit : add +git to the version in file Version
......
...@@ -564,7 +564,7 @@ let () = Exn_printer.register ...@@ -564,7 +564,7 @@ let () = Exn_printer.register
print_pr pr print_pr pr
| Decl.NonPositiveIndDecl (_ls, pr, ls1) -> | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
fprintf fmt "Inductive clause %a contains \ fprintf fmt "Inductive clause %a contains \
a negative occurrence of symbol %a" a non strictly positive occurrence of symbol %a"
print_pr pr print_ls ls1 print_pr pr print_ls ls1
| Decl.BadLogicDecl (ls1,ls2) -> | Decl.BadLogicDecl (ls1,ls2) ->
fprintf fmt "Ill-formed definition: symbols %a and %a are different" fprintf fmt "Ill-formed definition: symbols %a and %a are different"
......
...@@ -197,3 +197,19 @@ theory TestInline ...@@ -197,3 +197,19 @@ theory TestInline
goal G : p 4 4 goal G : p 4 4
end end
theory TestInductive
use import int.Int
inductive p (x:int) =
| C0 : forall x:int. p x -> p x
(* NonPositiveIndDecl
| C1 : forall x:int.
(if p x then true else false) -> p x
*)
| C2 : let x=0 in p x
end
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