Commit 7431a795 authored by Jean-Christophe's avatar Jean-Christophe

PVS: fixed output; improved realizations

parent ad6bcf3e
......@@ -977,13 +977,13 @@ PVSLIBS_REAL_FILES = Abs FromInt MinMax Real # ExpLog Square RealInfix
PVSLIBS_REAL = $(addprefix lib/pvs/real/, $(PVSLIBS_REAL_FILES))
PVSLIBS_LIST_FILES =
# List Length
# Nth
PVSLIBS_LIST = $(addprefix lib/pvs/int/, $(PVSLIBS_LIST_FILES))
PVSLIBS_NUMBER_FILES = # Divisibility Gcd Parity Prime
PVSLIBS_NUMBER = $(addprefix lib/pvs/number/, $(PVSLIBS_NUMBER_FILES))
ifeq (@enable_pvs_fp_libs@,yes)
ifeq (@enable_pvs_nasa_libs@,yes)
PVSLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
PVSLIBS_FP_ALL_FILES = GenFloat $(PVSLIBS_FP_FILES)
PVSLIBS_FP = $(addprefix lib/pvs/floating_point/, $(PVSLIBS_FP_ALL_FILES))
......@@ -1016,7 +1016,7 @@ install_no_local::
cp $(PVSLIBS_LIST) $(LIBDIR)/why3/pvs/list/
mkdir -p $(LIBDIR)/why3/pvs/number
cp $(PVSLIBS_NUMBER) $(LIBDIR)/why3/pvs/number/
ifeq (@enable_pvs_fp_libs@,yes)
ifeq (@enable_pvs_nasa_libs@,yes)
mkdir -p $(LIBDIR)/why3/pvs/floating_point/
cp $(PVSLIBS_FP) $(LIBDIR)/why3/pvs/
endif
......
......@@ -122,8 +122,10 @@ theory real.Real
syntax function ( - ) "(%1 - %2)"
syntax function (-_) "(-%1)"
syntax function ( * ) "(%1 * %2)"
(*
syntax function ( / ) "(%1 / %2)"
syntax function inv "(1 / %1)"
*)
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
......@@ -169,7 +171,7 @@ theory real.RealInfix
syntax function (-.) "(%1 - %2)"
syntax function (-._) "(-%1)"
syntax function ( *.) "(%1 * %2)"
syntax function (/.) "(%1 / %2)"
(* syntax function (/.) "(%1 / %2)" *)
syntax predicate (<=.) "(%1 <= %2)"
syntax predicate (<.) "(%1 < %2)"
......
Double: THEORY
BEGIN
IMPORTING int@Int
IMPORTING real@Real
IMPORTING real@Abs
IMPORTING real@FromInt
IMPORTING Rounding
IMPORTING DoubleFormat
% do not edit above this line
% Why3 round
round(x:Rounding.mode, x1:real): real
% Why3 round_logic
round_logic(x:Rounding.mode, x1:real): DoubleFormat.double
% Why3 value
value(x:DoubleFormat.double): real
% Why3 exact
exact(x:DoubleFormat.double): real
% Why3 model
model(x:DoubleFormat.double): real
% Why3 round_error
round_error(x:DoubleFormat.double): real = abs((value(x) - exact(x)))
% Why3 total_error
total_error(x:DoubleFormat.double): real = abs((value(x) - model(x)))
% Why3 no_overflow
no_overflow(m:Rounding.mode, x:real): bool = (abs(round(m,
x)) <= DoubleFormat.max_double)
% Why3 bounded_real_no_overflow
bounded_real_no_overflow: LEMMA FORALL (m:Rounding.mode, x:real):
(abs(x) <= DoubleFormat.max_double) => no_overflow(m, x)
% Why3 round_monotonic
round_monotonic: LEMMA FORALL (m:Rounding.mode, x:real, y:real):
(x <= y) => (round(m, x) <= round(m, y))
% Why3 round_idempotent
round_idempotent: LEMMA FORALL (m1:Rounding.mode, m2:Rounding.mode,
x:real): (round(m1, round(m2, x)) = round(m2, x))
% Why3 round_value
round_value: LEMMA FORALL (m:Rounding.mode, x:DoubleFormat.double):
(round(m, value(x)) = value(x))
% Why3 bounded_value
bounded_value: LEMMA FORALL (x:DoubleFormat.double):
(abs(value(x)) <= DoubleFormat.max_double)
% Why3 exact_rounding_for_integers
exact_rounding_for_integers: LEMMA FORALL (m:Rounding.mode, i:int):
(((-DoubleFormat.max_int) <= i) AND (i <= DoubleFormat.max_int)) =>
(round(m, (i :: real)) = (i :: real))
% Why3 round_down_le
round_down_le: LEMMA FORALL (x:real): (round(Rounding.down, x) <= x)
% Why3 round_up_ge
round_up_ge: LEMMA FORALL (x:real): (round(Rounding.up, x) >= x)
% Why3 round_down_neg
round_down_neg: LEMMA FORALL (x:real): (round(Rounding.down,
(-x)) = (-round(Rounding.up, x)))
% Why3 round_up_neg
round_up_neg: LEMMA FORALL (x:real): (round(Rounding.up,
(-x)) = (-round(Rounding.down, x)))
% Why3 of_real_post
of_real_post(m:Rounding.mode, x:real, res:DoubleFormat.double): bool =
(value(res) = round(m, x)) AND ((exact(res) = x) AND (model(res) = x))
% Why3 add_post
add_post(m:Rounding.mode, x:DoubleFormat.double, y:DoubleFormat.double,
res:DoubleFormat.double): bool = (value(res) = round(m,
(value(x) + value(y)))) AND ((exact(res) = (exact(x) + exact(y))) AND
(model(res) = (model(x) + model(y))))
% Why3 sub_post
sub_post(m:Rounding.mode, x:DoubleFormat.double, y:DoubleFormat.double,
res:DoubleFormat.double): bool = (value(res) = round(m,
(value(x) - value(y)))) AND ((exact(res) = (exact(x) - exact(y))) AND
(model(res) = (model(x) - model(y))))
% Why3 mul_post
mul_post(m:Rounding.mode, x:DoubleFormat.double, y:DoubleFormat.double,
res:DoubleFormat.double): bool = (value(res) = round(m,
(value(x) * value(y)))) AND ((exact(res) = (exact(x) * exact(y))) AND
(model(res) = (model(x) * model(y))))
% Why3 div_post
div_post(m:Rounding.mode, x:DoubleFormat.double, y:DoubleFormat.double,
res:DoubleFormat.double): bool = (value(res) = round(m,
real@Real.infix_sl(value(x), value(y)))) AND
((exact(res) = real@Real.infix_sl(exact(x), exact(y))) AND
(model(res) = real@Real.infix_sl(model(x), model(y))))
% Why3 neg_post
neg_post(x:DoubleFormat.double, res:DoubleFormat.double): bool =
(value(res) = (-value(x))) AND ((exact(res) = (-exact(x))) AND
(model(res) = (-model(x))))
% Why3 lt
lt(x:DoubleFormat.double, y:DoubleFormat.double): bool =
(value(x) < value(y))
% Why3 gt
gt(x:DoubleFormat.double, y:DoubleFormat.double): bool =
(value(x) > value(y))
END Double
\ No newline at end of file
DoubleFormat: THEORY
BEGIN
% do not edit above this line
% Why3 double
double: TYPE+
% Why3 max_double
max_double: real =
(9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)
% Why3 max_int
max_int: int = 9007199254740992
END DoubleFormat
\ No newline at end of file
Rounding: THEORY
BEGIN
% do not edit above this line
% Why3 mode
mode: DATATYPE
BEGIN
nearesttiestoeven: nearesttiestoeven?
tozero: tozero?
up: up?
down: down?
nearesttiestoaway: nearesttiestoaway?
END mode
END Rounding
\ No newline at end of file
Single: THEORY
BEGIN
IMPORTING int@Int
IMPORTING real@Real
IMPORTING real@Abs
IMPORTING real@FromInt
IMPORTING Rounding
IMPORTING SingleFormat
% do not edit above this line
% Why3 round
round(x:Rounding.mode, x1:real): real
% Why3 round_logic
round_logic(x:Rounding.mode, x1:real): SingleFormat.single
% Why3 value
value(x:SingleFormat.single): real
% Why3 exact
exact(x:SingleFormat.single): real
% Why3 model
model(x:SingleFormat.single): real
% Why3 round_error
round_error(x:SingleFormat.single): real = abs((value(x) - exact(x)))
% Why3 total_error
total_error(x:SingleFormat.single): real = abs((value(x) - model(x)))
% Why3 no_overflow
no_overflow(m:Rounding.mode, x:real): bool = (abs(round(m,
x)) <= SingleFormat.max_single)
% Why3 bounded_real_no_overflow
bounded_real_no_overflow: LEMMA FORALL (m:Rounding.mode, x:real):
(abs(x) <= SingleFormat.max_single) => no_overflow(m, x)
% Why3 round_monotonic
round_monotonic: LEMMA FORALL (m:Rounding.mode, x:real, y:real):
(x <= y) => (round(m, x) <= round(m, y))
% Why3 round_idempotent
round_idempotent: LEMMA FORALL (m1:Rounding.mode, m2:Rounding.mode,
x:real): (round(m1, round(m2, x)) = round(m2, x))
% Why3 round_value
round_value: LEMMA FORALL (m:Rounding.mode, x:SingleFormat.single):
(round(m, value(x)) = value(x))
% Why3 bounded_value
bounded_value: LEMMA FORALL (x:SingleFormat.single):
(abs(value(x)) <= SingleFormat.max_single)
% Why3 exact_rounding_for_integers
exact_rounding_for_integers: LEMMA FORALL (m:Rounding.mode, i:int):
(((-SingleFormat.max_int) <= i) AND (i <= SingleFormat.max_int)) =>
(round(m, (i :: real)) = (i :: real))
% Why3 round_down_le
round_down_le: LEMMA FORALL (x:real): (round(Rounding.down, x) <= x)
% Why3 round_up_ge
round_up_ge: LEMMA FORALL (x:real): (round(Rounding.up, x) >= x)
% Why3 round_down_neg
round_down_neg: LEMMA FORALL (x:real): (round(Rounding.down,
(-x)) = (-round(Rounding.up, x)))
% Why3 round_up_neg
round_up_neg: LEMMA FORALL (x:real): (round(Rounding.up,
(-x)) = (-round(Rounding.down, x)))
% Why3 of_real_post
of_real_post(m:Rounding.mode, x:real, res:SingleFormat.single): bool =
(value(res) = round(m, x)) AND ((exact(res) = x) AND (model(res) = x))
% Why3 add_post
add_post(m:Rounding.mode, x:SingleFormat.single, y:SingleFormat.single,
res:SingleFormat.single): bool = (value(res) = round(m,
(value(x) + value(y)))) AND ((exact(res) = (exact(x) + exact(y))) AND
(model(res) = (model(x) + model(y))))
% Why3 sub_post
sub_post(m:Rounding.mode, x:SingleFormat.single, y:SingleFormat.single,
res:SingleFormat.single): bool = (value(res) = round(m,
(value(x) - value(y)))) AND ((exact(res) = (exact(x) - exact(y))) AND
(model(res) = (model(x) - model(y))))
% Why3 mul_post
mul_post(m:Rounding.mode, x:SingleFormat.single, y:SingleFormat.single,
res:SingleFormat.single): bool = (value(res) = round(m,
(value(x) * value(y)))) AND ((exact(res) = (exact(x) * exact(y))) AND
(model(res) = (model(x) * model(y))))
% Why3 div_post
div_post(m:Rounding.mode, x:SingleFormat.single, y:SingleFormat.single,
res:SingleFormat.single): bool = (value(res) = round(m,
real@Real.infix_sl(value(x), value(y)))) AND
((exact(res) = real@Real.infix_sl(exact(x), exact(y))) AND
(model(res) = real@Real.infix_sl(model(x), model(y))))
% Why3 neg_post
neg_post(x:SingleFormat.single, res:SingleFormat.single): bool =
(value(res) = (-value(x))) AND ((exact(res) = (-exact(x))) AND
(model(res) = (-model(x))))
% Why3 lt
lt(x:SingleFormat.single, y:SingleFormat.single): bool =
(value(x) < value(y))
% Why3 gt
gt(x:SingleFormat.single, y:SingleFormat.single): bool =
(value(x) > value(y))
END Single
\ No newline at end of file
SingleFormat: THEORY
BEGIN
% do not edit above this line
% Why3 single
single: TYPE+
% Why3 max_single
max_single: real = (33554430 * 10141204801825835211973625643008)
% Why3 max_int
max_int: int = 16777216
END SingleFormat
\ No newline at end of file
......@@ -3,19 +3,15 @@ Abs: THEORY
IMPORTING Int
% do not edit above this line
% Why3 tuple0
tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
% Why3 abs
abs(x:int): int = IF (x >= 0) THEN x ELSE (-x) ENDIF
% Why3 abs1
abs1(x:int): int = IF (x >= 0) THEN x ELSE (-x) ENDIF
% Why3 abs_le
abs_le: LEMMA FORALL (x:int, y:int): (abs(x) <= y) <=> (((-y) <= x) AND
abs_le: LEMMA FORALL (x:int, y:int): (abs1(x) <= y) <=> (((-y) <= x) AND
(x <= y))
% Why3 abs_pos
abs_pos: LEMMA FORALL (x:int): (abs(x) >= 0)
abs_pos: LEMMA FORALL (x:int): (abs1(x) >= 0)
END Abs
\ No newline at end of file
......@@ -4,9 +4,6 @@ ComputerDivision: THEORY
IMPORTING Abs
% do not edit above this line
% Why3 tuple0
tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
IMPORTING ints@div, ints@rem
div_total(x: int): int
......@@ -15,15 +12,14 @@ ComputerDivision: THEORY
div(x:int,
x1:int): MACRO int = IF x1 /= 0 THEN div(x, x1) ELSE div_total(x) ENDIF
mod_total(x: int): int
% Why3 mod1
mod1(x:int, x1:int): int
% Why3 mod
mod(x:int,
x1:int): MACRO int = IF x1 /= 0 THEN rem(x, x1) ELSE mod_total(x) ENDIF
mod_total(x: int): int
% Why3 div_mod
div_mod: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) => (x = ((y * div(x,
y)) + mod(x, y)))
y)) + mod1(x, y)))
% Why3 div_bound
div_bound: LEMMA FORALL (x:int, y:int): ((x >= 0) AND (y > 0)) =>
......@@ -31,7 +27,7 @@ ComputerDivision: THEORY
% Why3 mod_bound
mod_bound: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) =>
(((-abs(y)) < mod(x, y)) AND (mod(x, y) < abs(y)))
(((-abs(y)) < mod1(x, y)) AND (mod1(x, y) < abs(y)))
% Why3 div_sign_pos
div_sign_pos: LEMMA FORALL (x:int, y:int): ((x >= 0) AND (y > 0)) =>
......@@ -43,11 +39,11 @@ ComputerDivision: THEORY
% Why3 mod_sign_pos
mod_sign_pos: LEMMA FORALL (x:int, y:int): ((x >= 0) AND NOT (y = 0)) =>
(mod(x, y) >= 0)
(mod1(x, y) >= 0)
% Why3 mod_sign_neg
mod_sign_neg: LEMMA FORALL (x:int, y:int): ((x <= 0) AND NOT (y = 0)) =>
(mod(x, y) <= 0)
(mod1(x, y) <= 0)
% Why3 rounds_toward_zero
rounds_toward_zero: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) =>
......@@ -57,14 +53,14 @@ ComputerDivision: THEORY
div_1: LEMMA FORALL (x:int): (div(x, 1) = x)
% Why3 mod_1
mod_1: LEMMA FORALL (x:int): (mod(x, 1) = 0)
mod_1: LEMMA FORALL (x:int): (mod1(x, 1) = 0)
% Why3 div_inf
div_inf: LEMMA FORALL (x:int, y:int): ((0 <= x) AND (x < y)) => (div(x,
y) = 0)
% Why3 mod_inf
mod_inf: LEMMA FORALL (x:int, y:int): ((0 <= x) AND (x < y)) => (mod(x,
mod_inf: LEMMA FORALL (x:int, y:int): ((0 <= x) AND (x < y)) => (mod1(x,
y) = x)
% Why3 div_mult
......@@ -73,8 +69,7 @@ ComputerDivision: THEORY
% Why3 mod_mult
mod_mult: LEMMA FORALL (x:int, y:int, z:int): ((x > 0) AND ((y >= 0) AND
(z >= 0))) => (mod(((x * y) + z), x) = mod(z, x))
(z >= 0))) => (mod1(((x * y) + z), x) = mod1(z, x))
END ComputerDivision
\ No newline at end of file
......@@ -4,9 +4,6 @@ EuclideanDivision: THEORY
IMPORTING Abs
% do not edit above this line
% Why3 tuple0
tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
IMPORTING ints@tdiv, ints@tmod
div_total(x: int): int
......@@ -15,26 +12,25 @@ EuclideanDivision: THEORY
div(x:int,
x1:int): MACRO int = IF x1 /= 0 THEN tdiv(x, x1) ELSE div_total(x) ENDIF
mod_total(x: int): int
% Why3 mod1
mod1(x:int, x1:int): int
% Why3 mod
mod(x:int,
x1:int): MACRO int = IF x1 /= 0 THEN mod(x, x1) ELSE mod_total(x) ENDIF
mod_total(x: int): int
% Why3 div_mod
div_mod: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) => (x = ((y * div(x,
y)) + mod(x, y)))
y)) + mod1(x, y)))
% Why3 div_bound
div_bound: LEMMA FORALL (x:int, y:int): ((x >= 0) AND (y > 0)) =>
((0 <= div(x, y)) AND (div(x, y) <= x))
% Why3 mod_bound
mod_bound: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) => ((0 <= mod(x,
y)) AND (mod(x, y) < abs(y)))
mod_bound: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) => ((0 <= mod1(x,
y)) AND (mod1(x, y) < abs(y)))
% Why3 mod_1
mod_1: LEMMA FORALL (x:int): (mod(x, 1) = 0)
mod_1: LEMMA FORALL (x:int): (mod1(x, 1) = 0)
% Why3 div_1
div_1: LEMMA FORALL (x:int): (div(x, 1) = x)
......@@ -48,7 +44,7 @@ EuclideanDivision: THEORY
(div((-x), y) = (-1))
% Why3 mod_0
mod_0: LEMMA FORALL (y:int): (NOT (y = 0)) => (mod(0, y) = 0)
mod_0: LEMMA FORALL (y:int): (NOT (y = 0)) => (mod1(0, y) = 0)
% Why3 div_1_left
div_1_left: LEMMA FORALL (y:int): (y > 1) => (div(1, y) = 0)
......@@ -57,11 +53,11 @@ EuclideanDivision: THEORY
div_minus1_left: LEMMA FORALL (y:int): (y > 1) => (div((-1), y) = (-1))
% Why3 mod_1_left
mod_1_left: LEMMA FORALL (y:int): (y > 1) => (mod(1, y) = 1)
mod_1_left: LEMMA FORALL (y:int): (y > 1) => (mod1(1, y) = 1)
% Why3 mod_minus1_left
mod_minus1_left: LEMMA FORALL (y:int): (y > 1) => (mod((-1), y) = (y - 1))
mod_minus1_left: LEMMA FORALL (y:int): (y > 1) => (mod1((-1),
y) = (y - 1))
END EuclideanDivision
\ No newline at end of file
......@@ -2,9 +2,6 @@ Int: THEORY
BEGIN
% do not edit above this line
% Why3 tuple0
tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
% Why3 zero
zero: int = 0
......@@ -90,6 +87,5 @@ Int: THEORY
compatordermult: LEMMA FORALL (x:int, y:int, z:int): infix_lseq(x, y) =>
(infix_lseq(zero, z) => infix_lseq(infix_as(x, z), infix_as(y, z)))
END Int
\ No newline at end of file
......@@ -3,49 +3,45 @@ MinMax: THEORY
IMPORTING Int
% do not edit above this line
% Why3 tuple0
tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
% Why3 min1
min1(x:int, x1:int): int
% Why3 min
min(x:int, x1:int): MACRO int = min(x, x1)
% Why3 max
max(x:int, x1:int): MACRO int = max(x, x1)
% Why3 max1
max1(x:int, x1:int): int
% Why3 max_is_ge
max_is_ge: LEMMA FORALL (x:int, y:int): (max(x, y) >= x) AND (max(x,
max_is_ge: LEMMA FORALL (x:int, y:int): (max1(x, y) >= x) AND (max1(x,
y) >= y)
% Why3 max_is_some
max_is_some: LEMMA FORALL (x:int, y:int): (max(x, y) = x) OR (max(x,
max_is_some: LEMMA FORALL (x:int, y:int): (max1(x, y) = x) OR (max1(x,
y) = y)
% Why3 min_is_le
min_is_le: LEMMA FORALL (x:int, y:int): (x >= min(x, y)) AND (y >= min(x,
min_is_le: LEMMA FORALL (x:int, y:int): (x >= min1(x, y)) AND (y >= min1(x,
y))
% Why3 min_is_some
min_is_some: LEMMA FORALL (x:int, y:int): (min(x, y) = x) OR (min(x,
min_is_some: LEMMA FORALL (x:int, y:int): (min1(x, y) = x) OR (min1(x,
y) = y)
% Why3 max_x
max_x: LEMMA FORALL (x:int, y:int): (x >= y) => (max(x, y) = x)
max_x: LEMMA FORALL (x:int, y:int): (x >= y) => (max1(x, y) = x)
% Why3 max_y
max_y: LEMMA FORALL (x:int, y:int): (y >= x) => (max(x, y) = y)
max_y: LEMMA FORALL (x:int, y:int): (y >= x) => (max1(x, y) = y)
% Why3 min_x
min_x: LEMMA FORALL (x:int, y:int): (y >= x) => (min(x, y) = x)
min_x: LEMMA FORALL (x:int, y:int): (y >= x) => (min1(x, y) = x)
% Why3 min_y
min_y: LEMMA FORALL (x:int, y:int): (x >= y) => (min(x, y) = y)
min_y: LEMMA FORALL (x:int, y:int): (x >= y) => (min1(x, y) = y)
% Why3 max_sym
max_sym: LEMMA FORALL (x:int, y:int): (x >= y) => (max(x, y) = max(y, x))
max_sym: LEMMA FORALL (x:int, y:int): (x >= y) => (max1(x, y) = max1(y, x))
% Why3 min_sym
min_sym: LEMMA FORALL (x:int, y:int): (x >= y) => (min(x, y) = min(y, x))
min_sym: LEMMA FORALL (x:int, y:int): (x >= y) => (min1(x, y) = min1(y, x))
END MinMax
\ No newline at end of file
......@@ -3,29 +3,27 @@ Abs: THEORY
IMPORTING Real
% do not edit above this line
% Why3 tuple0
tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
% Why3 abs
abs(x:real): real = IF (x >= 0) THEN x ELSE (-x) ENDIF
% Why3 abs1
abs1(x:real): real = IF (x >= 0) THEN x ELSE (-x) ENDIF
% Why3 abs_le
abs_le: LEMMA FORALL (x:real, y:real): (abs(x) <= y) <=> (((-y) <= x) AND
abs_le: LEMMA FORALL (x:real, y:real): (abs1(x) <= y) <=> (((-y) <= x) AND
(x <= y))
% Why3 abs_pos
abs_pos: LEMMA FORALL (x:real): (abs(x) >= 0)
abs_pos: LEMMA FORALL (x:real): (abs1(x) >= 0)
% Why3 abs_sum
abs_sum: LEMMA FORALL (x:real, y:real): (abs((x + y)) <= (abs(x) + abs(y)))
abs_sum: LEMMA FORALL (x:real, y:real):
(abs1((x + y)) <= (abs1(x) + abs1(y)))
% Why3 abs_prod
abs_prod: LEMMA FORALL (x:real, y:real): (abs((x * y)) = (abs(x) * abs(y)))
abs_prod: LEMMA FORALL (x:real, y:real):
(abs1((x * y)) = (abs1(x) * abs1(y)))
% Why3 triangular_inequality
triangular_inequality: LEMMA FORALL (x:real, y:real, z:real):
(abs((x - z)) <= (abs((x - y)) + abs((y - z))))
(abs1((x - z)) <= (abs1((x - y)) + abs1((y - z))))
END Abs
\ No newline at end of file
......@@ -4,9 +4,6 @@ FromInt: THEORY
IMPORTING Real
% do not edit above this line
% Why3 tuple0
tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
% Why3 from_int
from_int(x:int): MACRO real = x
......@@ -16,8 +13,8 @@ FromInt: THEORY
% Why3 one
one: LEMMA (from_int(1) = 1)
% Why3 add
add: LEMMA FORALL (x:int, y:int):
% Why3 add1
add1: LEMMA FORALL (x:int, y:int):
(from_int((x + y)) = (from_int(x) + from_int(y)))
% Why3 sub
......@@ -31,6 +28,5 @@ FromInt: THEORY
% Why3 neg
neg: LEMMA FORALL (x:int): (from_int((-x)) = (-from_int(x)))
END FromInt
\ No newline at end of file
......@@ -3,31 +3,27 @@ MinMax: THEORY
IMPORTING Real
% do not edit above this line
% Why3 tuple0
tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
% Why3 min1
min1(x:real, x1:real): real
% Why3 min
min(x:real, x1:real): MACRO real = min(x,x1)
% Why3 max
max(x:real, x1:real): MACRO real = max(x,x1)
% Why3 max1
max1(x:real, x1:real): real
% Why3 max_is_ge
max_is_ge: LEMMA FORALL (x:real, y:real): (max(x, y) >= x) AND (max(x,
max_is_ge: LEMMA FORALL (x:real, y:real): (max1(x, y) >= x) AND (max1(x,
y) >= y)
% Why3 max_is_some
max_is_some: LEMMA FORALL (x:real, y:real): (max(x, y) = x) OR (max(x,
max_is_some: LEMMA FORALL (x:real, y:real): (max1(x, y) = x) OR (max1(x,
y) = y)
% Why3 min_is_le
min_is_le: LEMMA FORALL (x:real, y:real): (min(x, y) <= x) AND (min(x,
min_is_le: LEMMA FORALL (x:real, y:real): (min1(x, y) <= x) AND (min1(x,
y) <= y)
% Why3 min_is_some
min_is_some: LEMMA FORALL (x:real, y:real): (min(x, y) = x) OR (min(x,
min_is_some: LEMMA FORALL (x:real, y:real): (min1(x, y) = x) OR (min1(x,
y) = y)
END MinMax
\ No newline at end of file
......@@ -2,9 +2,6 @@ Real: THEORY
BEGIN
% do not edit above this line
% Why3 tuple0
tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
% Why3 zero
zero: real = 0
......@@ -126,6 +123,5 @@ Real: THEORY
compatordermult: LEMMA FORALL (x:real, y:real, z:real): infix_lseq(x, y) =>
(infix_lseq(zero, z) => infix_lseq(infix_as(x, z), infix_as(y, z)))
END Real
\ No newline at end of file
......@@ -285,6 +285,7 @@ name = "PVS"
exec = "pvs"
version_switch = "-version"
version_regexp = "PVS Version \\([^ \n]+\\)"
version_ok = "6.0"
version_ok = "5.0"
version_old = "^[0-4]\..+$"
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-check-pvs %l %f"
......
......@@ -84,7 +84,7 @@ let black_list =
(* PVS prelude *)
"boolean"; "bool";
"pred"; "setof"; "exists1";
"list"; "member"; "append"; "reverse";
"list"; "length"; "member"; "nth"; "append"; "reverse";
"domain"; "range"; "graph"; "preserves"; "inverts"; "transpose";
"restrict"; "extend"; "identity"; "eq";
"epsilon";
......@@ -107,11 +107,10 @@ let black_list =
"mod"; "divides"; "rem"; "ndiv";
"upfrom"; "above";
"even";
(* introduced by Why3 *)
"tuple0"; ]
]
let fresh_printer () =
let isanitize = sanitizer char_to_alpha char_to_alnumus in
let isanitize = sanitizer char_to_lalpha char_to_lalnumus in
create_ident_printer black_list ~sanitizer:isanitize
let iprinter =
......@@ -176,12 +175,14 @@ let print_path = print_list (constant_string ".") string
let print_id fmt id = string fmt (id_unique iprinter id)
let print_id_real info fmt id =
try let path,th,ipr = Mid.find id info.symbol_printers in
fprintf fmt "%s.%s.%s"
path
th.Theory.th_name.id_string
(id_unique ipr id)
with Not_found -> print_id fmt id
try
let path, th, ipr = Mid.find id info.symbol_printers in
let th = th.Theory.th_name.id_string in
let id = id_unique ipr id in
if path = "" then fprintf fmt "%s.%s" th id
else fprintf fmt "%s@@%s.%s" path th id
with Not_found ->
print_id fmt id
let print_ls_real info fmt ls = print_id_real info fmt ls.ls_name
let print_ts_real info fmt ts = print_id_real info fmt ts.ts_name
......@@ -193,7 +194,7 @@ let rec print_ty info fmt ty = match ty.ty_node with
| Tyvar v -> print_tv fmt v
| Tyapp (ts, tl) when is_ts_tuple ts ->
begin match tl with
| [] -> fprintf fmt "tuple0"
| [] -> fprintf fmt "[]"
| [ty] -> print_ty info fmt ty
| _ -> fprintf fmt "[%a]" (print_list comma (print_ty info)) tl
end
......@@ -338,7 +339,7 @@ and print_tnode opl opr info fmt t = match t.t_node with
(print_vsty_nopar info) v (print_opl_fmla info) f;
forget_var v
| Tapp (fs, []) when is_fs_tuple fs ->
fprintf fmt "Tuple0"
fprintf fmt "()"
| Tapp (fs, pl) when is_fs_tuple fs ->