diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-02-09 14:55:48 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-02-09 14:55:48 +0000 |
commit | 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe (patch) | |
tree | bbb5e49ccbf7e3614966571acc317f8d318fecad /lib/Floats.v | |
download | compcert-kvx-2ae43be7b9d4118335c9d2cef6e098f9b9f807fe.tar.gz compcert-kvx-2ae43be7b9d4118335c9d2cef6e098f9b9f807fe.zip |
Initial import of compcert
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Floats.v')
-rw-r--r-- | lib/Floats.v | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/lib/Floats.v b/lib/Floats.v new file mode 100644 index 00000000..b95789e6 --- /dev/null +++ b/lib/Floats.v @@ -0,0 +1,55 @@ +(** Axiomatization of floating-point numbers. *) + +(** In contrast with what we do with machine integers, we do not bother + to formalize precisely IEEE floating-point arithmetic. Instead, we + simply axiomatize a type [float] for IEEE double-precision floats + and the associated operations. *) + +Require Import Bool. +Require Import AST. +Require Import Integers. + +Parameter float: Set. + +Module Float. + +Parameter zero: float. +Parameter one: float. + +Parameter neg: float -> float. +Parameter abs: float -> float. +Parameter singleoffloat: float -> float. +Parameter intoffloat: float -> int. +Parameter floatofint: int -> float. +Parameter floatofintu: int -> float. + +Parameter add: float -> float -> float. +Parameter sub: float -> float -> float. +Parameter mul: float -> float -> float. +Parameter div: float -> float -> float. + +Parameter cmp: comparison -> float -> float -> bool. + +Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}. + +(** Below are the only properties of floating-point arithmetic that we + rely on in the compiler proof. *) + +Axiom addf_commut: forall f1 f2, add f1 f2 = add f2 f1. + +Axiom subf_addf_opp: forall f1 f2, sub f1 f2 = add f1 (neg f2). + +Axiom singleoffloat_idem: + forall f, singleoffloat (singleoffloat f) = singleoffloat f. + +Axiom cmp_ne_eq: + forall f1 f2, cmp Cne f1 f2 = negb (cmp Ceq f1 f2). +Axiom cmp_le_lt_eq: + forall f1 f2, cmp Cle f1 f2 = cmp Clt f1 f2 || cmp Ceq f1 f2. +Axiom cmp_ge_gt_eq: + forall f1 f2, cmp Cge f1 f2 = cmp Cgt f1 f2 || cmp Ceq f1 f2. + +Axiom eq_zero_true: cmp Ceq zero zero = true. +Axiom eq_zero_false: forall f, f <> zero -> cmp Ceq f zero = false. + +End Float. |