mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
36 lines
775 B
Plaintext
36 lines
775 B
Plaintext
module AdditionSqrtSingle
|
|
use real.RealInfix
|
|
use real.Abs
|
|
use ufloat.USingle
|
|
use ufloat.USingleLemmas
|
|
use ieee_float.RoundingMode
|
|
use real.Square
|
|
|
|
val function usqrt (x:usingle) : usingle
|
|
|
|
let add_sqrt (a b : usingle)
|
|
ensures {
|
|
let exact = (to_real a +. to_real (usqrt b)) in
|
|
abs (to_real result -. exact) <=. eps *. abs exact
|
|
}
|
|
= a ++. usqrt b
|
|
end
|
|
|
|
module AdditionSqrtDouble
|
|
use real.RealInfix
|
|
use real.Abs
|
|
use ufloat.UDouble
|
|
use ufloat.UDoubleLemmas
|
|
use ieee_float.RoundingMode
|
|
use real.Square
|
|
|
|
val function usqrt (x:udouble) : udouble
|
|
|
|
let add_sqrt (a b : udouble)
|
|
ensures {
|
|
let exact = (to_real a +. to_real (usqrt b)) in
|
|
abs (to_real result -. exact) <=. eps *. abs exact
|
|
}
|
|
= a ++. usqrt b
|
|
end
|