peano.mlw 1.94 KB
 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 `````` (** {2 Peano arithmetic} *) module Peano use import int.Int type t model { v: int } val to_int (x: t) : int ensures { result = x.v } val zero (): t ensures { result.v = 0 } (* FIXME: should be a constant val function zero : t ensures { result.v = 0 } *) val succ (x: t) : t ensures { result.v = x.v + 1 } val pred (x: t) : t ensures { result.v = x.v - 1 } val lt (x y: t) : bool ensures { result <-> x.v < y.v } val le (x y: t) : bool ensures { result <-> x.v <= y.v } val gt (x y: t) : bool ensures { result <-> x.v > y.v } val ge (x y: t) : bool ensures { result <-> x.v >= y.v } val eq (x y: t) : bool ensures { result <-> x.v = y.v } val ne (x y: t) : bool ensures { result <-> x.v <> y.v } val neg (x: t) : t ensures { result.v = - x.v } val abs (x: t) : t ensures { result.v = if x.v >= 0 then x.v else - x.v } val add (x y: t) (low high: t) : t requires { low.v <= x.v + y.v <= high.v } ensures { result.v = x.v + y.v } val sub (x y: t) (low high: t) : t requires { low.v <= x.v - y.v <= high.v } ensures { result.v = x.v - y.v } val mul (x y: t) (low high: t) : t requires { low.v <= x.v * y.v <= high.v } ensures { result.v = x.v * y.v } val of_int (x: int) (low high: t) : t requires { low.v <= x <= high.v } ensures { result.v = x } (* FIXME could replace low.v by - max (abs low) (abs high) high.v by max (abs low) (abs high) avoid the computation of the bounds e.g. addition of two values of different signs *) use import int.ComputerDivision val div (x y: t) : t requires { y.v <> 0 } ensures { result.v = div x.v y.v } val mod (x y: t) : t requires { y.v <> 0 } ensures { result.v = mod x.v y.v } use import int.MinMax val max (x y: t) : t ensures { result.v = max x.v y.v } val min (x y: t) : t ensures { result.v = min x.v y.v } end ``````