update

[clean-tests.git] / afp / a12 / gastyStart.dcl

diff --git a/afp/a12/gastyStart.dcl b/afp/a12/gastyStart.dcl
new file mode 100644 (file)
index 0000000..053ac97
--- /dev/null
+++ b/afp/a12/gastyStart.dcl
@@ -0,0 +1,37 @@
+definition module gastyStart
+
+/*
+       Pieter Koopman, Radboud University, 2016 - 2018
+       pieter@cs.ru.nl
+       Advanced programming
+       A simplified MBT tool based on logical properties
+       
+       Use the iTask environment!
+       Execute with "Basic values only" option
+*/
+
+import StdEnv, StdGeneric, Data.GenEq
+
+test :: p -> [String] | prop p
+class prop a where holds :: a Prop -> [Prop]
+
+:: Prop
+
+instance prop Bool
+instance prop (a->b) | prop b & testArg a
+class testArg a | gen{|*|}, string{|*|}, gEq{|*|} a
+
+generic gen a :: [a]
+derive gen Int, Real, Bool, Char, UNIT, PAIR, EITHER, CONS, OBJECT, RECORD, FIELD
+
+generic string a :: a -> String
+derive string Int, Real, Bool, Char, UNIT, PAIR, EITHER, CONS of gcd, OBJECT, RECORD of grd, FIELD of gfd
+
+:: For = E.a b: (For) infix 0 (a -> b) [a] & prop b & string{|*|} a
+instance prop For
+
+:: Select = E.p: (==>) infixl 0 Bool p & prop p
+instance prop Select
+
+:: Equ = E.a: (=.=) infix 4 a a & testArg a
+instance prop Equ