mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
198 lines
6.1 KiB
Plaintext
198 lines
6.1 KiB
Plaintext
(** {1 Floating-Point Computations with overflow check}
|
|
|
|
The following functions could be used to encode floating-point
|
|
operations in programs, in the case where one wants to forbids
|
|
overflows.
|
|
|
|
Each function comes with two pre-conditions and two post-conditions,
|
|
one using interpretation in real numbers, one using the predicate
|
|
`t'isFinite` from the `ieee_float` library. The second form should be
|
|
better with a prover that has built-in support for floating-point
|
|
numbers.
|
|
|
|
*)
|
|
|
|
(** {2 Single-precision floats} *)
|
|
|
|
module Single
|
|
|
|
use real.RealInfix
|
|
use export ieee_float.Float32
|
|
|
|
predicate add_pre_ieee (x:t) (y:t) =
|
|
t'isFinite (x .+ y)
|
|
|
|
predicate add_post_ieee (x:t) (y:t) (r:t) =
|
|
r = x .+ y
|
|
|
|
predicate add_pre_real (x:t) (y:t) =
|
|
no_overflow RNE (t'real x +. t'real y)
|
|
|
|
predicate add_post_real (x:t) (y:t) (r:t) =
|
|
t'real r = round RNE (t'real x +. t'real y)
|
|
|
|
val safe_add (x y: t) : t
|
|
requires { [@expl:finite floating-point number] t'isFinite x }
|
|
requires { [@expl:finite floating-point number] t'isFinite y }
|
|
requires { [@expl:floating-point overflow]
|
|
add_pre_ieee x y \/ add_pre_real x y }
|
|
ensures { t'isFinite result }
|
|
ensures { add_post_ieee x y result /\ add_post_real x y result }
|
|
|
|
predicate sub_pre_ieee (x:t) (y:t) =
|
|
t'isFinite (x .- y)
|
|
|
|
predicate sub_post_ieee (x:t) (y:t) (r:t) =
|
|
r = x .- y
|
|
|
|
predicate sub_pre_real (x:t) (y:t) =
|
|
no_overflow RNE (t'real x -. t'real y)
|
|
|
|
predicate sub_post_real (x:t) (y:t) (r:t) =
|
|
t'real r = round RNE (t'real x -. t'real y)
|
|
|
|
val safe_sub (x y: t) : t
|
|
requires { [@expl:finite floating-point number] t'isFinite x }
|
|
requires { [@expl:finite floating-point number] t'isFinite y }
|
|
requires { [@expl:floating-point overflow]
|
|
sub_pre_ieee x y \/ sub_pre_real x y }
|
|
ensures { t'isFinite result }
|
|
ensures { sub_post_ieee x y result /\ sub_post_real x y result }
|
|
|
|
predicate mul_pre_ieee (x:t) (y:t) =
|
|
t'isFinite (x .* y)
|
|
|
|
predicate mul_post_ieee (x:t) (y:t) (r:t) =
|
|
r = x .* y
|
|
|
|
predicate mul_pre_real (x:t) (y:t) =
|
|
no_overflow RNE (t'real x *. t'real y)
|
|
|
|
predicate mul_post_real (x:t) (y:t) (r:t) =
|
|
t'real r = round RNE (t'real x *. t'real y)
|
|
|
|
val safe_mul (x y: t) : t
|
|
requires { [@expl:finite floating-point number] t'isFinite x }
|
|
requires { [@expl:finite floating-point number] t'isFinite y }
|
|
requires { [@expl:floating-point overflow]
|
|
mul_pre_ieee x y \/ mul_pre_real x y }
|
|
ensures { t'isFinite result }
|
|
ensures { mul_post_ieee x y result /\ mul_post_real x y result }
|
|
|
|
predicate div_pre_ieee (x:t) (y:t) =
|
|
t'isFinite (x ./ y)
|
|
|
|
predicate div_post_ieee (x:t) (y:t) (r:t) =
|
|
r = x ./ y
|
|
|
|
predicate div_pre_real (x:t) (y:t) =
|
|
no_overflow RNE (t'real x /. t'real y)
|
|
|
|
predicate div_post_real (x:t) (y:t) (r:t) =
|
|
t'real r = round RNE (t'real x /. t'real y)
|
|
|
|
val safe_div (x y: t) : t
|
|
requires { [@expl:finite floating-point number] t'isFinite x }
|
|
requires { [@expl:finite floating-point number] t'isFinite y }
|
|
requires { [@expl:non-zero floating-point number] not (is_zero y) }
|
|
requires { [@expl:floating-point overflow]
|
|
div_pre_ieee x y \/ div_pre_real x y }
|
|
ensures { t'isFinite result }
|
|
ensures { div_post_ieee x y result /\ div_post_real x y result }
|
|
|
|
|
|
end
|
|
|
|
|
|
|
|
(** {2 Double-precision floats} *)
|
|
|
|
module Double
|
|
|
|
use real.RealInfix
|
|
use export ieee_float.Float64
|
|
|
|
predicate add_pre_ieee (x:t) (y:t) =
|
|
t'isFinite (x .+ y)
|
|
|
|
predicate add_post_ieee (x:t) (y:t) (r:t) =
|
|
r = x .+ y
|
|
|
|
predicate add_pre_real (x:t) (y:t) =
|
|
no_overflow RNE (t'real x +. t'real y)
|
|
|
|
predicate add_post_real (x:t) (y:t) (r:t) =
|
|
t'real r = round RNE (t'real x +. t'real y)
|
|
|
|
val safe_add (x y: t) : t
|
|
requires { [@expl:finite floating-point number] t'isFinite x }
|
|
requires { [@expl:finite floating-point number] t'isFinite y }
|
|
requires { [@expl:floating-point overflow]
|
|
add_pre_ieee x y \/ add_pre_real x y }
|
|
ensures { t'isFinite result }
|
|
ensures { add_post_ieee x y result /\ add_post_real x y result }
|
|
|
|
predicate sub_pre_ieee (x:t) (y:t) =
|
|
t'isFinite (x .- y)
|
|
|
|
predicate sub_post_ieee (x:t) (y:t) (r:t) =
|
|
r = x .- y
|
|
|
|
predicate sub_pre_real (x:t) (y:t) =
|
|
no_overflow RNE (t'real x -. t'real y)
|
|
|
|
predicate sub_post_real (x:t) (y:t) (r:t) =
|
|
t'real r = round RNE (t'real x -. t'real y)
|
|
|
|
val safe_sub (x y: t) : t
|
|
requires { [@expl:finite floating-point number] t'isFinite x }
|
|
requires { [@expl:finite floating-point number] t'isFinite y }
|
|
requires { [@expl:floating-point overflow]
|
|
sub_pre_ieee x y \/ sub_pre_real x y }
|
|
ensures { t'isFinite result }
|
|
ensures { sub_post_ieee x y result /\ sub_post_real x y result }
|
|
|
|
predicate mul_pre_ieee (x:t) (y:t) =
|
|
t'isFinite (x .* y)
|
|
|
|
predicate mul_post_ieee (x:t) (y:t) (r:t) =
|
|
r = x .* y
|
|
|
|
predicate mul_pre_real (x:t) (y:t) =
|
|
no_overflow RNE (t'real x *. t'real y)
|
|
|
|
predicate mul_post_real (x:t) (y:t) (r:t) =
|
|
t'real r = round RNE (t'real x *. t'real y)
|
|
|
|
val safe_mul (x y: t) : t
|
|
requires { [@expl:finite floating-point number] t'isFinite x }
|
|
requires { [@expl:finite floating-point number] t'isFinite y }
|
|
requires { [@expl:floating-point overflow]
|
|
mul_pre_ieee x y \/ mul_pre_real x y }
|
|
ensures { t'isFinite result }
|
|
ensures { mul_post_ieee x y result /\ mul_post_real x y result }
|
|
|
|
predicate div_pre_ieee (x:t) (y:t) =
|
|
t'isFinite (x ./ y)
|
|
|
|
predicate div_post_ieee (x:t) (y:t) (r:t) =
|
|
r = x ./ y
|
|
|
|
predicate div_pre_real (x:t) (y:t) =
|
|
no_overflow RNE (t'real x /. t'real y)
|
|
|
|
predicate div_post_real (x:t) (y:t) (r:t) =
|
|
t'real r = round RNE (t'real x /. t'real y)
|
|
|
|
val safe_div (x y: t) : t
|
|
requires { [@expl:finite floating-point number] t'isFinite x }
|
|
requires { [@expl:finite floating-point number] t'isFinite y }
|
|
requires { [@expl:non-zero floating-point number] not (is_zero y) }
|
|
requires { [@expl:floating-point overflow]
|
|
div_pre_ieee x y \/ div_pre_real x y }
|
|
ensures { t'isFinite result }
|
|
ensures { div_post_ieee x y result /\ div_post_real x y result }
|
|
|
|
|
|
end
|