Commit 50d1b914 authored by MARCHE Claude's avatar MARCHE Claude

pb avec Real

parent 3d5022d0
......@@ -163,11 +163,11 @@ bin/top: $(CMO)
test: bin/why.byte
mkdir -p output_why3
ocamlrun -bt bin/why.byte -I theories/ --driver drivers/why3.drv \
--output-dir output_why3 --all-goals src/test.why
--output-dir output_why3 --all-goals src/test.why
bin/why.byte --driver drivers/alt_ergo.drv -I theories/ \
--output-file - --goal Test.G src/test.why --timeout 3
--output-file - --goal Test.G src/test.why --timeout 3
bin/why.byte --driver drivers/alt_ergo.drv -I theories/ \
--call --goal Test.G src/test.why --timeout 3
--call --goal Test.G src/test.why --timeout 3
testl: bin/whyl.byte
ocamlrun -bt bin/whyl.byte -I theories/ src/programs/test.mlw
......
......@@ -58,10 +58,24 @@ exception CommandError
exception NoCommandlineProvided
(* this should be changeable by an option
(otherwise: The program 'timeout' is currently not installed) *)
let cpulimit = ref "timeout" (*"why-cpulimit"*)
(* this should be replaced by a proper use of fork/waitpid() *)
let cpulimit_commands = ["why-cpulimit"; "timeout"]
let cpulimit = ref (
let tmp = ref "" in
try
List.iter
(fun s ->
let r = Sys.command (s^" 1 echo") in
if r=0 then (tmp:=s; raise Exit))
cpulimit_commands;
failwith
(List.fold_left
(fun acc s -> acc^" "^s^",")
"need shell command among:"
cpulimit_commands)
with Exit -> !tmp)
(* Utils *)
......
......@@ -71,6 +71,6 @@ end
theory Field
clone export UnitaryCommutativeRing
logic inv(t) : t
axiom Inverse : forall x:t. x * inv(x) = one
axiom Inverse : forall x:t. x <> zero -> x * inv(x) = one
logic (/) (x:t, y:t) : t = x * inv(y)
end
theory Rounding
type mode = Near | Zero | Up | Down | NearTiesToAway
(** nearest ties to even, to zero, upward, downward, nearest ties to away *)
end
theory GenFloat
use import Rounding
use import real.Real
use import real.Abs
type t
logic round(mode,real) : real
logic round_logic(mode,real) : t
logic value(t) : real
logic exact(t) : real
logic model(t) : real
logic round_error(x:t) : real = abs(value(x) - exact(x))
logic total_error(x:t) : real = abs(value(x) - model(x))
logic max : real
logic no_overflow(m:mode,x:real) = abs(round(m,x)) <= max
axiom Bounded_real_no_overflow :
forall m:mode, x:real. abs(x) <= max -> no_overflow(m,x)
axiom Round_monotonic :
forall m:mode,x,y:real. x <= y -> round(m,x) <= round(m,y)
logic max_representable_integer : int
axiom Exact_rounding_for_integers:
forall m:mode,i:int.
- max_representable_integer <= i <= max_representable_integer ->
round(m,from_int(i)) = from_int(i)
(* rounding up and down *)
axiom Round_down_le:
forall x:real. round(Down,x) <= x
axiom Round_up_ge:
forall x:real. round(Up,x) >= x
axiom Round_down_neg:
forall x:real. round(Down,-x) = - round(Up,x)
axiom Round_up_neg:
forall x:real. round(Up,-x) = - round(Down,x)
end
theory Single
type single
logic max_single : real = 0x1.FFFFFEp127
logic max_int : int = 16777216 (* 2^24 *)
clone export GenFloat with
type t = single,
logic max = max_single,
logic max_representable_integer = max_int
end
theory Double
type double
logic max_double : real = 0x1.FFFFFFFFFFFFFp1023
logic max_int = 9007199254740992 (* 2^23 *)
clone export GenFloat with
type t = double,
logic max = max_double,
logic max_representable_integer = max_int
end
theory Real
logic (< ) (real, real)
logic (< )(real, real)
logic (<=)(real, real)
logic (> ) (real, real)
logic (> )(real, real)
logic (>=)(real, real)
(* TODO : < is a total order relation *)
(* TODO : they are total order relations *)
logic zero : real = 0.0
logic one : real = 1.0
......@@ -67,18 +67,75 @@ theory Truncate
end
theory Sqrt
theory Square
use import Real
logic sqr(x:real):real = x * x
logic sqrt(real):real
axiom Sqrt_positive:
forall x:real. x >= 0.0 -> sqrt(x) >= 0.0
axiom Sqrt_square:
forall x:real. x >= 0.0 -> sqr(sqrt(x)) = x
axiom Square_sqrt:
forall x:real. x >= 0.0 -> sqrt(x*x) = x
end
theory ExpLog
(* exp, log *)
use import Real
logic exp(real) : real
axiom Exp_zero : exp(0.0) = 1.0
axiom Exp_sum : forall x,y:real. exp(x+y) = exp(x)*exp(y)
logic log(real) : real
axiom Log_one : log(1.0) = 0.0
axiom Log_mul :
forall x,y:real. x > 0.0 and y > 0.0 -> log(x*y) = log(x)+log(y)
axiom Log_exp: forall x:real. log(exp(x)) = x
axiom Exp_log: forall x:real. x > 0.0 -> exp(log(x)) = x
logic log10(x:real) : real = log(x)/log(10.0)
end
theory Power
use import Real
use import Square
use import ExpLog
logic pow(real,real) : real
axiom Pow_zero_y:
forall y:real. y <> 0.0 -> pow(0.0,y) = 0.0
axiom Pow_x_zero:
forall x:real. x <> 0.0 -> pow(x,0.0) = 1.0
axiom Pow_x_one:
forall x:real. pow(x,1.0) = x
axiom Pow_one_y:
forall y:real. pow(1.0,y) = 1.0
axiom Pow_x_two:
forall x:real. pow(x,2.0) = sqr(x)
axiom Pow_half:
forall x:real. x > 0.0 -> pow(x,0.5) = sqrt(x)
axiom Pow_exp_log:
forall x:real. x > 0.0 -> pow(x,y) = exp(y*log(x))
end
theory Trigonometry
......
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