Commit 80d4b42c authored by MARCHE Claude's avatar MARCHE Claude

bug 13375 fixed

parent 6546c95d
......@@ -130,20 +130,28 @@ scheduled on Sep 2012
== New Features to announce ==
New features:
o new API for programs
o type invariants ?
o Support for Coq 8.4
o dropped support for Coq 8.2
o new scheme for Coq realizations using type classes
o new API for programs
o Support for PVS 6.0
o Support for PVS 6.0, including realizations
Bug fixes:
o
o fixed bug on merging config files which prevented the use
of Why3 back-end of the Frama-C/Jessie plugin when Coq is
not installed. (Bug 14672 of the Bug Tracking System)
o fixed bugs 13503 and 13375 of the Bug Tracking System
== Final preparation ==
* faire une passe sur le BTS
* do "make update-coq" and "make", fix Coq realizations if needed
* check that nightly bench is OK
* check that "make xml-validate" is OK
(see below : copy the dtd on the web)
* put 0.74 in file Version
* check headers
* check the file CHANGES, add the release date
......@@ -157,6 +165,7 @@ Bug fixes:
* put on the web page
- why3-0.74.tar.gz
- why3session.dtd
- standard library online, using why3doc, to http://why3.lri.fr/stdlib/
(make stdlibdoc ;
cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.74;
......
theory Signed
use import int.Int
type signed_type
function first : int
function last : int
predicate in_range (x : int) =
(first <= x <= last)
function to_int (n : signed_type) : int
function from_int (n : int) : signed_type
predicate eq (left : signed_type) (right : signed_type) =
(to_int left) = (to_int right)
axiom range :
forall x : signed_type.
in_range (to_int x)
axiom coerce :
forall x : int [(in_range x), (from_int x)].
(in_range x) -> ((to_int (from_int x)) = x)
axiom unicity :
forall x y : signed_type.
(to_int x) = (to_int y) -> x = y
end
module Spec
use import int.Int
type my_type
clone Signed as My_Type_T
with type signed_type = my_type
axiom axiom_first :
My_Type_T.first = 1
axiom axiom_last :
My_Type_T.last = 100
val my_type_t_from___int_ :
n : int ->
{ (My_Type_T.in_range n) }
my_type
{ (My_Type_T.to_int result) = n }
let to_int_ (x : my_type) =
{ true }
(My_Type_T.to_int x)
{ true }
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="13375/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<file
name="../13375.mlw"
verified="true"
expanded="true">
<theory
name="Signed"
locfile="13375/../13375.mlw"
loclnum="1" loccnumb="7" loccnume="13"
verified="true"
expanded="true">
</theory>
<theory
name="Spec"
locfile="13375/../13375.mlw"
loclnum="34" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="WP_parameter to_int_"
locfile="13375/../13375.mlw"
loclnum="53" loccnumb="5" loccnume="12"
expl="normal postcondition"
sum="4077c128df716cfc503b0898c655443c"
proved="true"
expanded="true"
shape="t">
<label
name="expl:parameter to_int_"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
</file>
</why3session>
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