diff options
| author | Don Stewart <dons@galois.com> | 2007-09-27 23:44:01 +0200 |
|---|---|---|
| committer | Don Stewart <dons@galois.com> | 2007-09-27 23:44:01 +0200 |
| commit | f5d686a3cb3c7f36109e221969b80e7cc5a0aab8 (patch) | |
| tree | 453dd83469e0f326b66a3f100567d9834e2d87e3 /tests | |
| parent | c04b6f4b266ec9a5381f3db679885cc36176cac0 (diff) | |
| download | metatile-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.hs | 21 |
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) |