From a7d7542dc646a5fd124ef71e71ce260889f1701b Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Tue, 2 Feb 2016 19:24:50 +0100
Subject: Moved to 1415 directory

---
 1415/files/practicum/StdSetTest.icl | 124 ++++++++++++++++++++++++++++++++++++
 1 file changed, 124 insertions(+)
 create mode 100644 1415/files/practicum/StdSetTest.icl

(limited to '1415/files/practicum/StdSetTest.icl')

diff --git a/1415/files/practicum/StdSetTest.icl b/1415/files/practicum/StdSetTest.icl
new file mode 100644
index 0000000..3b75c3e
--- /dev/null
+++ b/1415/files/practicum/StdSetTest.icl
@@ -0,0 +1,124 @@
+module StdSetTest
+
+/*	Test module StdSet
+	Voor werken met Gast: 
+		(*) gebruik Environment 'Gast'
+		(*) zet Project Options op 'Basic Values Only' en '8M' Maximum Heap Size.
+*/
+
+import gast
+import GenLexOrd
+import StdSet
+
+Start = testn 2000 
+        (\n` n2` m -> let n  = cast [A,B,C] n`
+                          n2 = cast [A,B,C] n2`
+                       in 
+							membership            m n  /\
+							conversion_invariant  n    /\
+							length_property       n    /\
+							subset_property       n n2 /\
+							strictsubset_property n n2 /\
+							empty_properties      m n  /\
+							disjoint_properties   n n2 /\
+							product_properties    n n2 /\
+							intersect_properties  n n2 /\
+							setminus_properties   n n2 /\
+							union_properties      n n2 /\
+							powset_properties     n    /\
+							True
+                   )
+
+:: Enum = A | B | C 
+
+derive bimap []
+derive ggen Enum
+derive genShow Enum
+derive gEq Enum
+derive gLexOrd Enum
+instance == Enum where (==) x y = gEq{|*|} x y
+instance <  Enum where  (<) x y = gEq{|*|} (gLexOrd{|*|} x y) LT
+
+// clean should have something like this!
+cast :: a a -> a
+cast _ x = x
+
+membership :: Enum [Enum] -> Property
+membership x xs
+ = name "membership"
+   ( memberOfSet x s <==> isMember x xs )
+  where s = toSet xs
+
+conversion_invariant :: [Enum] -> Property
+conversion_invariant xs
+ = name "conversion_invariant" 
+   ( toSet (fromSet xs`) == xs` )
+   where xs` = toSet xs
+
+length_property :: [Enum] -> Property
+length_property xs
+ = name "length_property"
+   ( nrOfElements s == length (removeDup xs) )
+ where s = toSet xs
+
+subset_property :: [Enum] [Enum] -> Property
+subset_property xs ys
+ = name "subset_property"
+   ( (isSubset u v) <==> all (flip isMember ys) xs)
+  where (u,v) = (toSet xs, toSet ys)
+
+strictsubset_property :: [Enum] [Enum] -> Property
+strictsubset_property xs ys
+ = name "strictsubset_property"
+   ( (isStrictSubset u v) <==> (all (flip isMember ys) xs && not (all (flip isMember xs) ys)) )
+  where (u,v) = (toSet xs, toSet ys)
+
+// everything you alwys wanted to know about the empty set...
+// ... but were afraid to ask
+empty_properties :: Enum [Enum] -> Property
+empty_properties x xs
+ = name "empty_properties"
+   ( isEmptySet (cast dummy zero) /\ isEmptySet (toSet (cast [A] [])) /\
+     ((nrOfElements s == 0) <==> isEmptySet s) /\ 
+           ((zero == s)     <==> isEmptySet s) )
+ where s = toSet xs
+       dummy :: Set Enum
+       dummy = undef
+
+product_properties :: [Enum] [Enum] -> Property
+product_properties xs ys
+ = name "product_properties"
+   ( product u v == toSet [(x,y) \\ x<-xs, y<-ys ] )
+ where (u,v) = (toSet xs, toSet ys)
+
+powset_properties :: [Enum] -> Property
+powset_properties xs
+ = name "powset_properties"
+   ( powerSet s == toSet (map toSet (subs xs)) )
+ where s = toSet xs
+       subs [] = [[]]
+       subs [x:xs] = subs xs ++ [ [x:xs`] \\ xs` <- subs xs ]
+
+union_properties :: [Enum] [Enum] -> Property
+union_properties xs ys
+ = name "union_properties"
+   ( union u v == toSet (xs++ys) )
+ where (u,v) = (toSet xs, toSet ys)
+
+intersect_properties :: [Enum] [Enum] -> Property
+intersect_properties xs ys
+ = name "intersect_properties"
+   ( intersection u v == toSet [ x \\ x<-xs | isMember x ys ] )
+ where (u,v) = (toSet xs, toSet ys)
+
+setminus_properties :: [Enum] [Enum] -> Property
+setminus_properties xs ys
+ = name "setminus_properties"
+   ( without u v == toSet [ x \\ x<-xs | not (isMember x ys) ])
+ where (u,v) = (toSet xs, toSet ys)
+
+disjoint_properties :: [Enum] [Enum] -> Property
+disjoint_properties xs ys
+ = name "disjoint_properties"
+   ( isDisjoint u v <==> (nrOfElements u + nrOfElements v == nrOfElements (union u v)) )
+ where (u,v) = (toSet xs, toSet ys)
-- 
cgit v1.2.3