diff --git a/src/libraries/OS-Independent/Data/Set.dcl b/src/libraries/OS-Independent/Data/Set.dcl index e3373eaeaab576eb0633ba0554186a00aa162f46..70a3a85146b136e80b5edb298088d066ad1b5248 100644 --- a/src/libraries/OS-Independent/Data/Set.dcl +++ b/src/libraries/OS-Independent/Data/Set.dcl @@ -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 diff --git a/src/libraries/OS-Independent/Data/Set.icl b/src/libraries/OS-Independent/Data/Set.icl index c70917e8972bfa2197546f59a31d464d81006dc4..6a692fc4306884ddc15ada19be150cd144a008bc 100644 --- a/src/libraries/OS-Independent/Data/Set.icl +++ b/src/libraries/OS-Independent/Data/Set.icl @@ -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.