1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
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
|
