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