Library JMLNumeric
This file is part of
A Formal Definition of JML in Coq
and its Application to Runtime Assertion Checking
Ph.D. Thesis by Hermann Lehner
Online available at jmlcoq.info
Authors:
- Hermann Lehner
- David Pichardie (Bicolano)
- Andreas Kaegi (Syntax Rewritings, Implementation of ADTs)
Common interface for numerics domains
Open Local Scope Z_scope.
Module Type NUMERIC.
Parameter t : Set.
Parameter toZ : t -> Z.
Parameter power : Z.
Definition half_base := 2^power.
Definition base := 2 * half_base.
Definition range (z : Z) : Prop := -half_base <= z < half_base.
Parameter range_prop : forall x:t , range (toZ x).
Parameter num_dec : forall t1 t2:t , {t1 = t2} + {t1 <> t2}.
Definition smod (x:Z) : Z :=
let z := x mod base in
match Zcompare z half_base with
| Lt => z
| _ => z - base
end.
Parameter add : t -> t -> t.
Parameter add_prop : forall i1 i2 ,
toZ (add i1 i2) = smod (toZ i1 + toZ i2).
Parameter sub : t -> t -> t.
Parameter sub_prop : forall i1 i2 ,
toZ (sub i1 i2) = smod (toZ i1 - toZ i2).
Parameter mul : t -> t -> t.
Parameter mul_prop : forall i1 i2 ,
toZ (mul i1 i2) = smod (toZ i1 * toZ i2).
Parameter div : t -> t -> t.
Parameter div_prop : forall i1 i2 ,
toZ (div i1 i2) = smod (toZ i1 / toZ i2).
Parameter rem : t -> t -> t.
Parameter rem_prop : forall i1 i2 ,
toZ (rem i1 i2) = smod (toZ i1 mod toZ i2).
Parameter shr : t -> t -> t.
Parameter shr_prop : forall i1 i2 ,
toZ (shr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
Parameter shl : t -> t -> t.
Parameter shl_prop : forall i1 i2 ,
toZ (shr i1 i2) = smod (toZ i1 * 2^(toZ i2 mod 32)).
Parameter ushr : t -> t -> t.
Parameter ushr_prop1 : forall i1 i2 ,
toZ i1 < 0 ->
toZ (ushr i1 i2) = smod ((toZ i1 + base) / 2^(toZ i2 mod 32)).
Parameter ushr_prop2 : forall i1 i2 ,
toZ i1 >= 0 ->
toZ (ushr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
Parameter and : t -> t -> t.
Parameter or : t -> t -> t.
Parameter xor : t -> t -> t.
Parameter not : t -> t.
Parameter neg : t -> t.
Parameter neg_prop : forall i ,
toZ (neg i) = smod (- toZ i).
Parameter const : Z -> t.
Parameter const_prop : forall z ,
range z -> toZ (const z) = z.
End NUMERIC.
Module Type NUMERIC.
Parameter t : Set.
Parameter toZ : t -> Z.
Parameter power : Z.
Definition half_base := 2^power.
Definition base := 2 * half_base.
Definition range (z : Z) : Prop := -half_base <= z < half_base.
Parameter range_prop : forall x:t , range (toZ x).
Parameter num_dec : forall t1 t2:t , {t1 = t2} + {t1 <> t2}.
Definition smod (x:Z) : Z :=
let z := x mod base in
match Zcompare z half_base with
| Lt => z
| _ => z - base
end.
Parameter add : t -> t -> t.
Parameter add_prop : forall i1 i2 ,
toZ (add i1 i2) = smod (toZ i1 + toZ i2).
Parameter sub : t -> t -> t.
Parameter sub_prop : forall i1 i2 ,
toZ (sub i1 i2) = smod (toZ i1 - toZ i2).
Parameter mul : t -> t -> t.
Parameter mul_prop : forall i1 i2 ,
toZ (mul i1 i2) = smod (toZ i1 * toZ i2).
Parameter div : t -> t -> t.
Parameter div_prop : forall i1 i2 ,
toZ (div i1 i2) = smod (toZ i1 / toZ i2).
Parameter rem : t -> t -> t.
Parameter rem_prop : forall i1 i2 ,
toZ (rem i1 i2) = smod (toZ i1 mod toZ i2).
Parameter shr : t -> t -> t.
Parameter shr_prop : forall i1 i2 ,
toZ (shr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
Parameter shl : t -> t -> t.
Parameter shl_prop : forall i1 i2 ,
toZ (shr i1 i2) = smod (toZ i1 * 2^(toZ i2 mod 32)).
Parameter ushr : t -> t -> t.
Parameter ushr_prop1 : forall i1 i2 ,
toZ i1 < 0 ->
toZ (ushr i1 i2) = smod ((toZ i1 + base) / 2^(toZ i2 mod 32)).
Parameter ushr_prop2 : forall i1 i2 ,
toZ i1 >= 0 ->
toZ (ushr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
Parameter and : t -> t -> t.
Parameter or : t -> t -> t.
Parameter xor : t -> t -> t.
Parameter not : t -> t.
Parameter neg : t -> t.
Parameter neg_prop : forall i ,
toZ (neg i) = smod (- toZ i).
Parameter const : Z -> t.
Parameter const_prop : forall z ,
range z -> toZ (const z) = z.
End NUMERIC.