From 2fb92231d082210ed639a3f942ca3817aa51f978 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Mon, 11 Dec 2017 15:56:14 +0100
Subject: Assignment 12 up to 4

---
 assignment-12/cashModel.icl | 52 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

(limited to 'assignment-12/cashModel.icl')

diff --git a/assignment-12/cashModel.icl b/assignment-12/cashModel.icl
index ed0174a..5c11b31 100644
--- a/assignment-12/cashModel.icl
+++ b/assignment-12/cashModel.icl
@@ -8,6 +8,9 @@ implementation module cashModel
 */
 
 import StdEnv, GenEq
+import gastje
+from Data.Func import mapSt
+import Data.Tuple
 
 class euro a :: a -> Euro
 instance euro Product
@@ -46,3 +49,52 @@ model list (Rem p)
 | isMember p list = (removeMember p list,[~ (euro p)])
 | otherwise       = (list,[])
 model list Pay = ([],[euro list])
+
+derive gen Euro
+derive string Euro
+derive bimap []
+
+/**
+ * plus_zero_is_identity:          Fail for: {Euro|euro=0, cent=1} ; {Euro|euro=0, cent=1} <> {Euro|euro=0, cent=0}
+ * plus_is_commutative:            Passed
+ * minus_zero_is_identity:         Fail for: {Euro|euro=0, cent=1} ; {Euro|euro=0, cent=1} <> {Euro|euro=0, cent=0}
+ * prop_double_neg_is_identity:    Passed
+ * prop_neg_is_not_identity:       Fail for: {Euro|euro=0, cent=1}
+ * prop_minus_is_plus_after_neg:   Fail for: {Euro|euro=1, cent=0} {Euro|euro=-9223372036854775808, cent=1} ; {Euro|euro=0, cent=99} <> {Euro|euro=1, cent=1}
+ * prop_neg_distributes_over_plus: Fail for: {Euro|euro=1, cent=0} {Euro|euro=-9223372036854775808, cent=1} ; {Euro|euro=-1, cent=1} <> {Euro|euro=0, cent=99}
+ * prop_plus_minus_is_identity:    Fail for: {Euro|euro=0, cent=1} {Euro|euro=0, cent=0} ; {Euro|euro=0, cent=0} <> {Euro|euro=0, cent=1}
+ */
+Start =
+	[ ["plus_zero_is_identity:          ": test prop_plus_zero_is_identity]
+	, ["plus_is_commutative:            ": test prop_plus_is_commutative]
+	, ["minus_zero_is_identity:         ": test prop_minus_zero_is_identity]
+	, ["prop_double_neg_is_identity:    ": test prop_double_neg_is_identity]
+	, ["prop_neg_is_not_identity:       ": test prop_neg_is_not_identity]
+	, ["prop_minus_is_plus_after_neg:   ": test prop_minus_is_plus_after_neg]
+	, ["prop_neg_distributes_over_plus: ": test prop_neg_distributes_over_plus]
+	, ["prop_plus_minus_is_identity:    ": test prop_plus_minus_is_identity]
+	]
+where
+	prop_plus_zero_is_identity :: Euro -> Equals Euro
+	prop_plus_zero_is_identity e = e + zero =.= e
+
+	prop_plus_is_commutative :: Euro Euro -> Equals Euro
+	prop_plus_is_commutative a b = a + b =.= b + a
+
+	prop_minus_zero_is_identity :: Euro -> Equals Euro
+	prop_minus_zero_is_identity e = e - zero =.= e
+
+	prop_plus_minus_is_identity :: Euro Euro -> Equals Euro
+	prop_plus_minus_is_identity a b = a =.= a - b + b
+
+	prop_double_neg_is_identity :: Euro -> Equals Euro
+	prop_double_neg_is_identity e = ~(~e) =.= e
+
+	prop_neg_is_not_identity :: Euro -> Implies
+	prop_neg_is_not_identity e = e <> zero ==> e <> ~e
+
+	prop_minus_is_plus_after_neg :: Euro Euro -> Equals Euro
+	prop_minus_is_plus_after_neg a b = a - b =.= a + ~b
+
+	prop_neg_distributes_over_plus :: Euro Euro -> Equals Euro
+	prop_neg_distributes_over_plus a b = ~(a + b) =.= ~a + ~b
-- 
cgit v1.2.3