Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit e5dc233b authored by MARCHE Claude's avatar MARCHE Claude

fix examples on floats

parent b7787a01
...@@ -69,7 +69,7 @@ module M121_039_nonlinear ...@@ -69,7 +69,7 @@ module M121_039_nonlinear
predicate axiom_mult (a b y : t) = predicate axiom_mult (a b y : t) =
if a .<= b /\ y .<= zeroF then a .* y .>= b .* y else false if a .<= b /\ y .<= zeroF then a .* y .>= b .* y else false
let test (a x y:t) let ghost test (a x y:t)
requires { zeroF .<= a .<= one } requires { zeroF .<= a .<= one }
requires { .- one .<= x .<= one } requires { .- one .<= x .<= one }
requires { .- one .<= y .<= one } requires { .- one .<= y .<= one }
...@@ -77,7 +77,6 @@ module M121_039_nonlinear ...@@ -77,7 +77,6 @@ module M121_039_nonlinear
ensures { result .>= zeroF /\ result .<= (2.0:t) } ensures { result .>= zeroF /\ result .<= (2.0:t) }
= =
assert { axiom_mult a one y }; assert { axiom_mult a one y };
assert { a .>= zeroF }; assert { a .>= zeroF };
assert { a .<= one }; assert { a .<= one };
assert { x .> zeroF }; assert { x .> zeroF };
...@@ -87,7 +86,6 @@ module M121_039_nonlinear ...@@ -87,7 +86,6 @@ module M121_039_nonlinear
assert { x .+ y .* a .>= x .+ y }; assert { x .+ y .* a .>= x .+ y };
assert { x .+ y .>= zeroF }; assert { x .+ y .>= zeroF };
assert { x .+ y .* a .>= zeroF }; assert { x .+ y .* a .>= zeroF };
x .+ y .* a x .+ y .* a
end end
...@@ -97,7 +95,7 @@ module LB09_025_conversion ...@@ -97,7 +95,7 @@ module LB09_025_conversion
use import ieee_float.Float32 use import ieee_float.Float32
use import int.Int use import int.Int
let fti x let ghost fti x
requires { x .>= of_int RNE (-2147483648) /\ x .+ (of_int RNE 1) .<= of_int RNE 2147483647 } requires { x .>= of_int RNE (-2147483648) /\ x .+ (of_int RNE 1) .<= of_int RNE 2147483647 }
ensures { of_int RNE result .>= x .- (of_int RNE 1) } ensures { of_int RNE result .>= x .- (of_int RNE 1) }
ensures { of_int RNE result .<= x .+ (of_int RNE 1) } ensures { of_int RNE result .<= x .+ (of_int RNE 1) }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment