cleaning up

parent 9bc74453
......@@ -12,31 +12,12 @@ module Int
use export int.Int
use export int.ComputerDivision
let (/) (x: int) (y:int)
let (/) (x: int) (y: int)
requires { y <> 0 } ensures { result = div x y }
= div x y
end
(** {2 Division on real numbers}
See also {h <a href="floating_point.why.html">Floating-Point theories</a>.}
*)
module Real
use import real.Real
use export real.RealInfix
use export real.FromInt
let (/.) (x: real) (y: real)
requires { y <> 0. } ensures { result = x / y }
= x / y
end
(** {2 Machine integers}
Bounded integers, typically n-bit signed and unsigned integers, go
......@@ -80,28 +61,28 @@ module Bounded_int
ensures { to_int result = to_int a * to_int b }
val (-_) (a:t) : t
requires { "expl:integer overflow" in_bounds (- (to_int a)) }
ensures { to_int result = - (to_int a) }
requires { "expl:integer overflow" in_bounds (- to_int a) }
ensures { to_int result = - to_int a }
val eq (a:t) (b:t) : bool
ensures { result = True <-> to_int a = to_int b }
ensures { result <-> to_int a = to_int b }
val ne (a:t) (b:t) : bool
ensures { result = True <-> to_int a <> to_int b }
ensures { result <-> to_int a <> to_int b }
axiom extensionality: forall x y: t. to_int x = to_int y -> x = y
val (<=) (a:t) (b:t) : bool
ensures { result = True <-> to_int a <= to_int b }
ensures { result <-> to_int a <= to_int b }
val (<) (a:t) (b:t) : bool
ensures { result = True <-> to_int a < to_int b }
ensures { result <-> to_int a < to_int b }
val (>=) (a:t) (b:t) : bool
ensures { result = True <-> to_int a >= to_int b }
ensures { result <-> to_int a >= to_int b }
val (>) (a:t) (b:t) : bool
ensures { result = True <-> to_int a > to_int b }
ensures { result <-> to_int a > to_int b }
use import int.ComputerDivision
......
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