Commit 6e9ded77 authored by MARCHE Claude's avatar MARCHE Claude

Stdlib: int.ComputerDivision should provide separate "function" and "val"

for div and mod since we need to check division by zero
parent 7f0cc13a
......@@ -91,8 +91,8 @@ theory EuclideanDivision
use import Int
use import Abs
val function div (x y: int) : int
val function mod (x y: int) : int
function div (x y: int) : int
function mod (x y: int) : int
axiom Div_mod:
forall x y:int. y <> 0 -> x = y * div x y + mod x y
......@@ -162,8 +162,8 @@ theory ComputerDivision
use import Int
use import Abs
val function div (x y: int) : int
val function mod (x y: int) : int
function div (x y: int) : int
function mod (x y: int) : int
axiom Div_mod:
forall x y:int. y <> 0 -> x = y * div x y + mod x y
......@@ -205,6 +205,14 @@ theory ComputerDivision
x > 0 /\ y >= 0 /\ z >= 0 ->
mod (x * y + z) x = mod z x
val div (x y:int) : int
requires { y <> 0 }
ensures { result = div x y }
val mod (x y:int) : int
requires { y <> 0 }
ensures { result = mod x y }
end
(** {2 Generic Exponentiation of something to an integer exponent} *)
......
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