Commit 414ef4ae authored by MARCHE Claude's avatar MARCHE Claude

Small fixes in standard library

parent 5f70e95e
......@@ -166,7 +166,7 @@ See CHANGES
* test distrib/why3-0.84.tar.gz
* install web page for why2 which includes an updated page for the
quick migration guide. (sources are in CVS repository
~filliatr/ARCHIVE/www/why). ADD a colon on new syntax for 0.84. Change Proval into Toccata
~filliatr/ARCHIVE/www/why).
* put on the web page
- why3-0.84.tar.gz
cp distrib/why3-0.84.tar.gz /users/www-perso/projets/why3/download
......
......@@ -13,7 +13,8 @@ module Int
use export int.ComputerDivision
let (/) (x: int) (y: int)
requires { y <> 0 } ensures { result = div x y }
requires { "expl:division by zero" y <> 0 }
ensures { result = div x y }
= div x y
end
......
......@@ -219,7 +219,7 @@ theory Occ
lemma occ_bounds:
forall v: 'a, m: map int 'a, l u: int.
l <= u -> 0 <= occ v m l u <= u - l
(* direct when l>=u, by induction on b when l <= u *)
(* direct when l>=u, by induction on u when l <= u *)
lemma occ_append:
forall v: 'a, m: map int 'a, l mid u: int.
......
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