From 975e611d3ae2cd7d8a38328205564fbf97e0b3a4 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Sat, 17 Sep 2011 14:16:50 +0200 Subject: [PATCH] more support for full floats --- examples/check-builtin/floats/why3session.xml | 18 ++--- theories/floating_point.why | 81 ++++++++++++++----- 2 files changed, 71 insertions(+), 28 deletions(-) diff --git a/examples/check-builtin/floats/why3session.xml b/examples/check-builtin/floats/why3session.xml index 5d8d4459f..193b3af5d 100644 --- a/examples/check-builtin/floats/why3session.xml +++ b/examples/check-builtin/floats/why3session.xml @@ -36,7 +36,7 @@ expanded="true"> @@ -50,7 +50,7 @@ @@ -64,7 +64,7 @@ @@ -73,21 +73,21 @@ timelimit="5" edited="" obsolete="false"> - + - + - + @@ -113,7 +113,7 @@ @@ -127,7 +127,7 @@ diff --git a/theories/floating_point.why b/theories/floating_point.why index c9795ad10..f1db90f9b 100644 --- a/theories/floating_point.why +++ b/theories/floating_point.why @@ -81,7 +81,47 @@ theory GenFloat axiom Round_up_neg: forall x:real. round Up (-x) = - round Down x +end + +theory Single + + type single + + function max_single : real = 0x1.FFFFFEp127 + function max_int : int = 16777216 (* 2^24 *) + + clone export GenFloat with + type t = single, + function max = max_single, + function max_representable_integer = max_int + +end + + + +theory Double + + type double + + function max_double : real = 0x1.FFFFFFFFFFFFFp1023 + function max_int : int = 9007199254740992 (* 2^23 *) + + clone export GenFloat with + type t = double, + function max = max_double, + function max_representable_integer = max_int + +end + + + +theory GenFloatFull + use import SpecialValues + use import Rounding + use import real.Real + + clone export GenFloat (* special values *) function class t : class @@ -103,50 +143,55 @@ theory GenFloat predicate is_gen_zero_plus (x:t) = is_gen_zero x /\ sign x = Pos predicate is_gen_zero_minus (x:t) = is_gen_zero x /\ sign x = Neg - predicate le (x:t) (y:t) = + predicate le_full (x:t) (y:t) = (is_finite x /\ is_finite y /\ value x <= value y) \/ (is_minus_infinity x /\ is_not_NaN y) \/ (is_not_NaN x /\ is_plus_infinity y) - predicate lt (x:t) (y:t) = + predicate lt_full (x:t) (y:t) = (is_finite x /\ is_finite y /\ value x < value y) \/ (is_minus_infinity x /\ is_not_NaN y /\ not (is_minus_infinity y)) \/ (is_not_NaN x /\ not (is_plus_infinity x) /\ is_plus_infinity y) - predicate ge (x:t) (y:t) = le y x + predicate ge_full (x:t) (y:t) = le_full y x - predicate gt (x:t) (y:t) = lt y x + predicate gt_full (x:t) (y:t) = lt_full y x - predicate eq (x:t) (y:t) = + predicate eq_full (x:t) (y:t) = is_not_NaN x /\ is_not_NaN y /\ ((is_finite x /\ is_finite y /\ value x = value y) \/ (is_infinite x /\ is_infinite y /\ same_sign x y)) - predicate ne (x:t) (y:t) = not (eq x y) + predicate ne_full (x:t) (y:t) = not (eq_full x y) - lemma le_lt_trans: forall x y z:t. le x y /\ lt y z -> lt x z + lemma le_lt_full_trans: + forall x y z:t. le_full x y /\ lt_full y z -> lt_full x z - lemma lt_le_trans: forall x y z:t. lt x y /\ le y z -> lt x z + lemma lt_le_full_trans: + forall x y z:t. lt_full x y /\ le_full y z -> lt_full x z - lemma le_ge_asym: forall x y:t. le x y /\ ge x y -> eq x y + lemma le_ge_full_asym: + forall x y:t. le_full x y /\ ge_full x y -> eq_full x y - lemma not_lt_ge: forall x y:t. - not (lt x y) /\ is_not_NaN x /\ is_not_NaN y -> ge x y + lemma not_lt_ge_full: forall x y:t. + not (lt_full x y) /\ is_not_NaN x /\ is_not_NaN y -> ge_full x y - lemma not_gt_le: forall x y:t. - not (gt x y) /\ is_not_NaN x /\ is_not_NaN y -> le x y + lemma not_gt_le_full: forall x y:t. + not (gt_full x y) /\ is_not_NaN x /\ is_not_NaN y -> le_full x y end -theory Single + + +theory SingleFull type single function max_single : real = 0x1.FFFFFEp127 function max_int : int = 16777216 (* 2^24 *) - clone export GenFloat with + clone export GenFloatFull with type t = single, function max = max_single, function max_representable_integer = max_int @@ -155,18 +200,16 @@ end -theory Double +theory DoubleFull type double function max_double : real = 0x1.FFFFFFFFFFFFFp1023 function max_int : int = 9007199254740992 (* 2^23 *) - clone export GenFloat with + clone export GenFloatFull with type t = double, function max = max_double, function max_representable_integer = max_int end - - -- 2.26.2