summaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
authorDon Stewart <dons@galois.com>2007-09-27 23:44:01 +0200
committerDon Stewart <dons@galois.com>2007-09-27 23:44:01 +0200
commitf5d686a3cb3c7f36109e221969b80e7cc5a0aab8 (patch)
tree453dd83469e0f326b66a3f100567d9834e2d87e3 /tests
parentc04b6f4b266ec9a5381f3db679885cc36176cac0 (diff)
downloadmetatile-f5d686a3cb3c7f36109e221969b80e7cc5a0aab8.tar
metatile-f5d686a3cb3c7f36109e221969b80e7cc5a0aab8.zip
Add 3 QC properties for focusMaster: local, idempotent, preserves invariant
darcs-hash:20070927214401-cba2c-4d5e8646bcc9d21b844f56e7cea13b9af26de7c1
Diffstat (limited to 'tests')
-rw-r--r--tests/Properties.hs21
1 files changed, 19 insertions, 2 deletions
diff --git a/tests/Properties.hs b/tests/Properties.hs
index 3207f95..b42f463 100644
--- a/tests/Properties.hs
+++ b/tests/Properties.hs
@@ -141,6 +141,8 @@ prop_greedyView_I (n :: NonNegative Int) (x :: T) =
prop_focusUp_I (n :: NonNegative Int) (x :: T) =
invariant $ foldr (const focusUp) x [1..n]
+prop_focusMaster_I (n :: NonNegative Int) (x :: T) =
+ invariant $ foldr (const focusMaster) x [1..n]
prop_focusDown_I (n :: NonNegative Int) (x :: T) =
invariant $ foldr (const focusDown) x [1..n]
@@ -297,6 +299,9 @@ prop_focus_left_master (n :: NonNegative Int) (x::T) =
index (foldr (const focusUp) x [1..n]) == index x
prop_focus_right_master (n :: NonNegative Int) (x::T) =
index (foldr (const focusDown) x [1..n]) == index x
+prop_focus_master_master (n :: NonNegative Int) (x::T) =
+ index (foldr (const focusMaster) x [1..n]) == index x
+
prop_focusWindow_master (n :: NonNegative Int) (x :: T) =
case peek x of
Nothing -> True
@@ -308,6 +313,9 @@ prop_focusWindow_master (n :: NonNegative Int) (x :: T) =
prop_focus_left (x :: T) = (focusUp (focusDown x)) == x
prop_focus_right (x :: T) = (focusDown (focusUp x)) == x
+-- focus master is idempotent
+prop_focusMaster_idem (x :: T) = focusMaster x == focusMaster (focusMaster x)
+
-- focusWindow actually leaves the window focused...
prop_focusWindow_works (n :: NonNegative Int) (x :: T) =
case peek x of
@@ -326,7 +334,10 @@ prop_focus_all_r (x :: T) = (foldr (const focusDown) x [1..n]) == x
-- f x' = foldr (\_ y -> rotate GT y) x' [1..n]
-- focus is local to the current workspace
-prop_focus_local (x :: T) = hidden_spaces (focusDown x) == hidden_spaces x
+prop_focus_down_local (x :: T) = hidden_spaces (focusDown x) == hidden_spaces x
+prop_focus_up_local (x :: T) = hidden_spaces (focusUp x) == hidden_spaces x
+
+prop_focus_master_local (x :: T) = hidden_spaces (focusMaster x) == hidden_spaces x
prop_focusWindow_local (n :: NonNegative Int) (x::T ) =
case peek x of
@@ -581,16 +592,22 @@ main = do
,("index/length" , mytest prop_index_length)
,("focus left : invariant", mytest prop_focusUp_I)
+ ,("focus master : invariant", mytest prop_focusMaster_I)
,("focus right: invariant", mytest prop_focusDown_I)
,("focusWindow: invariant", mytest prop_focus_I)
,("focus left/master" , mytest prop_focus_left_master)
,("focus right/master" , mytest prop_focus_right_master)
+ ,("focus master/master" , mytest prop_focus_master_master)
,("focusWindow master" , mytest prop_focusWindow_master)
,("focus left/right" , mytest prop_focus_left)
,("focus right/left" , mytest prop_focus_right)
,("focus all left " , mytest prop_focus_all_l)
,("focus all right " , mytest prop_focus_all_r)
- ,("focus is local" , mytest prop_focus_local)
+ ,("focus down is local" , mytest prop_focus_down_local)
+ ,("focus up is local" , mytest prop_focus_up_local)
+ ,("focus master is local" , mytest prop_focus_master_local)
+ ,("focus master idemp" , mytest prop_focusMaster_idem)
+
,("focusWindow is local", mytest prop_focusWindow_local)
,("focusWindow works" , mytest prop_focusWindow_works)