Commit 9addf36e authored by MARCHE Claude's avatar MARCHE Claude

more theories

parent 1d0e668f
......@@ -19,3 +19,52 @@ theory Array
axiom Const : forall b:'b. forall a:'a. select(const(b),a) = b
end
theory BitVector
use export bool.Bool
use import int.Int
logic size : int
type bv
logic nth(bv,int): bool
logic bvzero : bv
axiom Nth_zero:
forall n:int. 0 <= n and n < size -> nth(bvzero,n) = False
logic bvone : bv
axiom Nth_one:
forall n:int. 0 <= n and n < size -> nth(bvone,n) = True
logic eq(v1:bv,v2:bv) =
forall n:int. 0 <= n and n < size -> nth(v1,n) = nth(v2,n)
logic bw_and(v1:bv,v2:bv) : bv
axiom Nth_bw_and:
forall v1,v2:bv,n:int. 0 <= n and n < size ->
nth(bw_and(v1,v2),n) = andb(nth(v1,n),nth(v2,n))
end
theory BV32
logic size : int = 32
clone export BitVector with logic size = size
end
theory TestBv32
use import BV32
lemma Test1:
let b = bw_and(bvzero,bvone) in nth(b,1) = False
end
(* definition of IEEE-754 rounding modes *)
theory Rounding
type mode = Near | Zero | Up | Down | NearTiesToAway
......@@ -7,6 +8,22 @@ theory Rounding
end
(* handling of IEEE-754 special values +\infty, -\infty, NaN, +0, -0 *)
theory SpecialValues
type class = Finite | Infinite | NaN
type sign = Neg | Pos
use import real.Real
inductive same_sign_real(sign,real) =
| Neg_case: forall x:real. x < 0.0 -> same_sign_real(Neg,x)
| Pos_case: forall x:real. x > 0.0 -> same_sign_real(Pos,x)
end
theory GenFloat
use import Rounding
......@@ -57,6 +74,17 @@ theory GenFloat
end
theory GenFloatFull
use import GenFloat
use import SpecialValues
(* special values *)
logic class(t) : class
logic sign(t) : sign
end
theory Single
type single
......@@ -71,6 +99,8 @@ theory Single
end
theory Double
type double
......
theory Equiv
type t
logic eq(t,t)
axiom Refl : forall x:t. eq(x,x)
axiom Symm : forall x,y:t. eq(x,y) -> eq(y,x)
axiom Trans : forall x,y,z:t. eq(x,y) and eq(y,z) -> eq(x,z)
end
theory Order
clone export Equiv
logic le(t,t)
axiom Le_refl : forall x:t. le(x,x)
axiom Le_trans : forall x,y,z:t. le(x,y) and le(y,z) -> le(x,z)
logic lt(x:t,y:t) = le(x,y) and not eq(x,y)
lemma Lt_antirefl: forall x:t. not lt(x,x)
lemma Lt_trans: forall x,y,z:t. lt(x,y) and lt(y,z) -> lt(x,z)
lemma Le_lt_trans: forall x,y,z:t. le(x,y) and lt(y,z) -> lt(x,z)
lemma Lt_le_trans: forall x,y,z:t. lt(x,y) and le(y,z) -> lt(x,z)
end
theory StrictOrder
clone export Equiv
logic lt(t,t)
axiom AntiRefl : forall x:t. not lt(x,x)
axiom Lt_trans : forall x,y,z:t. lt(x,y) and lt(y,z) -> lt(x,z)
logic le(x:t,y:t) = lt(x,y) or eq(x,y)
lemma Le_refl: forall x:t. le(x,x)
lemma Le_trans: forall x,y,z:t. le(x,y) and le(y,z) -> le(x,z)
lemma Le_lt_trans: forall x,y,z:t. le(x,y) and lt(y,z) -> lt(x,z)
lemma Lt_le_trans: forall x,y,z:t. lt(x,y) and le(y,z) -> lt(x,z)
end
(*
Local Variables:
compile-command: "../bin/why.opt --output-dir goals --driver ../drivers/alt_ergo.drv -I ../theories/ relations.why"
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