DoubleFormat.pvs 534 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
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