more tests

Makefile.in

@@ -178,6 +178,10 @@ test: bin/why.byte  $(TOOLS)
 	echo bin/why.byte --call --timeout 1 --driver drivers/alt_ergo.drv -I theories/ \
 		--all-goals theories/real.why 
 	mkdir -p theories/coq
+	bin/why.byte --driver drivers/coq.drv -I theories/ \
+		--output-dir theories/coq --goals-of int.Abs 
+	bin/why.byte --driver drivers/coq.drv -I theories/ \
+		--output-dir theories/coq --goals-of int.EuclideanDivision --goals-of int.ComputerDivision 
 	bin/why.byte --driver drivers/coq.drv -I theories/ \
 		--output-dir theories/coq --goals-of real.Abs 
 	bin/why.byte --driver drivers/coq.drv -I theories/ \
@@ -186,6 +190,8 @@ test: bin/why.byte  $(TOOLS)
 		--output-dir theories/coq --goals-of real.ExpLog
 	bin/why.byte --driver drivers/coq.drv -I theories/ \
 		--output-dir theories/coq --goals-of real.Trigonometric
+	bin/why.byte --driver drivers/coq.drv -I theories/ \
+		--output-dir theories/coq --goals-of floating_point.Test
 	for i in theories/coq/*.v; do echo coq $$i; (coqc $$i || true) done
 
 testl: bin/whyl.byte

theories/floating_point.why

@@ -115,4 +115,12 @@ theory Double
 
 end
 
+theory Test
+
+  use import Rounding
+  use import Single
+
+  lemma Round_01: round(Near,0.1) = 0x0.199999Ap0
+
+end
 

theories/int.why

@@ -45,10 +45,42 @@ end
 
 
 theory EuclideanDivision
-  (* TODO *)
+
+  use import Int
+  use import Abs
+
+  logic div(int,int) : int
+  logic mod(int,int) : int
+
+  axiom Div_mod: 
+    forall x,y:int. y <> 0 -> x = y * div(x,y) + mod(x,y)
+
+  axiom Mod_bound: 
+    forall x,y:int. y <> 0 -> 0 <= mod(x,y) and mod(x,y) < abs(y)
+
+  lemma Mod_1: forall x:int. mod(x,1) = 0
+
+  lemma Div_1: forall x:int. div(x,1) = x
+
 end
 
 theory ComputerDivision
-  (* TODO *)
+
+  use import Int
+  use import Abs
+
+  logic div(int,int) : int
+  logic mod(int,int) : int
+
+  axiom Div_mod: 
+    forall x,y:int. y <> 0 -> x = y * div(x,y) + mod(x,y)
+
+  axiom Mod_bound: 
+    forall x,y:int. y <> 0 -> -abs(y) < mod(x,y) and mod(x,y) < abs(y)
+
+  lemma Mod_1: forall x:int. mod(x,1) = 0
+
+  lemma Div_1: forall x:int. div(x,1) = x
+
 end