Why3 Standard Library index

# 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 nuilt-in support for floating-point numbers.

## 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:floating-point overflow]
add_pre_ieee x y \/ add_pre_real x y }
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:floating-point overflow]
sub_pre_ieee x y \/ sub_pre_real x y }
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:floating-point overflow]
mul_pre_ieee x y \/ mul_pre_real x y }
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:floating-point overflow]
div_pre_ieee x y \/ div_pre_real x y }
ensures  { div_post_ieee x y result /\ div_post_real x y result }

end

```

## 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:floating-point overflow]
add_pre_ieee x y \/ add_pre_real x y }
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:floating-point overflow]
sub_pre_ieee x y \/ sub_pre_real x y }
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:floating-point overflow]
mul_pre_ieee x y \/ mul_pre_real x y }
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:floating-point overflow]
div_pre_ieee x y \/ div_pre_real x y }
ensures  { div_post_ieee x y result /\ div_post_real x y result }

end
```

Generated by why3doc 1.4.0