Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
clean-and-itasks
clean-platform
Commits
8116b1cf
Verified
Commit
8116b1cf
authored
Jun 22, 2020
by
Camil Staps
🚀
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fix tests for Data.Set; use balanced invariant instead of log_size (which was always True)
parent
2ab3f602
Pipeline
#43816
failed with stage
in 2 minutes and 12 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
5 additions
and
5 deletions
+5
-5
src/libraries/OS-Independent/Data/Set.dcl
src/libraries/OS-Independent/Data/Set.dcl
+5
-5
No files found.
src/libraries/OS-Independent/Data/Set.dcl
View file @
8116b1cf
...
...
@@ -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
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment