From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 9 Feb 2006 14:55:48 +0000 Subject: Initial import of compcert git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Floats.v | 55 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 lib/Floats.v (limited to 'lib/Floats.v') 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. -- cgit