Commit 3e801acb authored by Steffen Michels's avatar Steffen Michels

Merge branch '96-balanced-set' into 'master'

Fix tests for Data.Set; use balanced invariant instead of log_size (which was always True)

Closes #96

See merge request !340
parents a74e11fe c9e198a8
Pipeline #44131 failed with stage
in 1 minute and 18 seconds
......@@ -82,17 +82,17 @@ from Data.Foldable import class Foldable
* @invariant integrity: A.s :: Set a | Eq, genShow{|*|}, gPrint{|*|} a:
* // Check that the data structure is still correct.
* name "no_duplicates" (no_duplicates s) /\
* name "log_size" (log_size s) /\
* name "balanced" (balanced s) /\
* name "sizes_correct" (sizes_correct s)
*
* @invariant no_duplicates: A.s :: Set a | Eq, genShow{|*|}, gPrint{|*|} a:
* xs =.= removeDup xs where xs = toList s
*
* @invariant log_size: A.s :: Set a:
* check (<) nelem (2 ^ depth s)
* @invariant balanced: A.s :: Set a:
* case s of
* Tip -> prop True
* Bin _ _ l r -> abs (depth l - depth r) < 2 /\ balanced l /\ balanced r
* where
* nelem = size s
*
* depth :: (Set a) -> Int
* depth Tip = 0
* depth (Bin _ _ l r) = 1 + (max `on` depth) l r
......
......@@ -454,7 +454,7 @@ maxView x = Just (deleteFindMax x)
However (since we use quickcheck :-) we will stick to strictly balanced
trees.
--------------------------------------------------------------------*/
delta :== 4
delta :== 3
ratio :== 2
// Functions balanceL and balanceR are specialised versions of balance.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment