Verified Commit 5560d110 authored by Camil Staps's avatar Camil Staps 🚀

Use four spaces for indentation in properties

parent 0e731357
Pipeline #29625 passed with stage
in 2 minutes and 48 seconds
......@@ -96,6 +96,18 @@ With [clean-test-properties][]' `testproperties` tool, [Gast][] test programs
can be generated with properties from docblocks. For this, several additional
fields can be used, which are further documented by [clean-test-properties][].
Our [standards](STANDARDS.md) require the use of tabs for indentation and spaces
for outlining. Because with properties code is included in documentation blocks,
using tabs for indentation would lead to tabs after spaces. To avoid this, we
use four spaces in this context instead. For example:
```clean
/**
* @property correctness: A.xs :: Set a:
* minList (toList xs) == findMin xs
*/
```
[clean-test-properties]: https://gitlab.science.ru.nl/clean-and-itasks/clean-test-properties
[Gast]: https://gitlab.science.ru.nl/clean-and-itasks/gast
......
......@@ -6,63 +6,63 @@ definition module Data.Map
* such that lookup, insert and delete operations can be performed in O(log n).
*
* @property-bootstrap
* import StdBool, StdChar, StdInt, StdTuple
* from StdList import all, isMember, removeDup, reverse, instance length []
* from Data.Func import on, `on`
* import Data.GenDefault
* from Data.List import nubBy
* import StdBool, StdChar, StdInt, StdTuple
* from StdList import all, isMember, removeDup, reverse, instance length []
* from Data.Func import on, `on`
* import Data.GenDefault
* from Data.List import nubBy
*
* :: Predicate a = ConstTrue | IsMember [a]
* :: Predicate a = ConstTrue | IsMember [a]
*
* pred :: (Predicate a) a -> Bool | Eq a
* pred ConstTrue _ = True
* pred (IsMember cs) c = isMember c cs
* pred :: (Predicate a) a -> Bool | Eq a
* pred ConstTrue _ = True
* pred (IsMember cs) c = isMember c cs
*
* :: GMap k v =
* { gma :: !v
* , gmb :: !v
* , gmc :: !v
* , gmd :: !v
* , gme :: !v
* , gmf :: !v
* , rest :: ![(k,v)]
* }
* :: GMap k v =
* { gma :: !v
* , gmb :: !v
* , gmc :: !v
* , gmd :: !v
* , gme :: !v
* , gmf :: !v
* , rest :: ![(k,v)]
* }
*
* class Key k
* where keya :: k; keyb :: k; keyc :: k; keyd :: k; keye :: k; keyf :: k
* class Key k
* where keya :: k; keyb :: k; keyc :: k; keyd :: k; keye :: k; keyf :: k
*
* instance Key Char
* where keya = 'a'; keyb = 'b'; keyc = 'c'; keyd = 'd'; keye = 'e'; keyf = 'f'
* instance Key Char
* where keya = 'a'; keyb = 'b'; keyc = 'c'; keyd = 'd'; keye = 'e'; keyf = 'f'
*
* derive class Gast GMap, Predicate
* derive genShow Map, Maybe
* derive gPrint Map, Maybe
* derive class Gast GMap, Predicate
* derive genShow Map, Maybe
* derive gPrint Map, Maybe
*
* kvs :: (GMap k v) -> [(k,v)] | Key k
* kvs gm =
* [ (keya,gm.gma)
* , (keyb,gm.gmb)
* , (keyc,gm.gmc)
* , (keyd,gm.gmd)
* , (keye,gm.gme)
* , (keyf,gm.gmf)
* : gm.rest
* ]
* kvs :: (GMap k v) -> [(k,v)] | Key k
* kvs gm =
* [ (keya,gm.gma)
* , (keyb,gm.gmb)
* , (keyc,gm.gmc)
* , (keyd,gm.gmd)
* , (keye,gm.gme)
* , (keyf,gm.gmf)
* : gm.rest
* ]
*
* all_present :: [(k,v)] (Map k v) -> Bool | <, == k & == v
* all_present kvs m = all (\(k,v) -> get k m == Just v) kvs`
* where
* kvs` = nubBy ((==) `on` fst) (reverse kvs) // Remove duplicate keys, assuming the last takes precedence
* all_present :: [(k,v)] (Map k v) -> Bool | <, == k & == v
* all_present kvs m = all (\(k,v) -> get k m == Just v) kvs`
* where
* kvs` = nubBy ((==) `on` fst) (reverse kvs) // Remove duplicate keys, assuming the last takes precedence
*
* all_from :: (Map k v) [(k,v)] -> Bool | Eq k & Eq v
* all_from Tip _ = True
* all_from (Bin _ k v l r) kvs = isMember (k,v) kvs && all_from l kvs && all_from r kvs
* all_from :: (Map k v) [(k,v)] -> Bool | Eq k & Eq v
* all_from Tip _ = True
* all_from (Bin _ k v l r) kvs = isMember (k,v) kvs && all_from l kvs && all_from r kvs
*
* @property-test-with k = Char
* @property-test-with v = Char
*
* @property-test-generator (GMap k v) -> Map k v | Key, <, == k
* gen gm = fromList (kvs gm)
* gen gm = fromList (kvs gm)
*/
from Data.Maybe import :: Maybe (..)
......@@ -86,25 +86,25 @@ import StdClass
* @var The type of the values stored in the mapping.
*
* @invariant integrity: A.m :: Map k v:
* log_size m /\
* sizes_correct m
* log_size m /\
* sizes_correct m
*
* @invariant log_size: A.m :: Map k v:
* check (<) nelem (2 ^ depth m)
* where
* nelem = mapSize m
* check (<) nelem (2 ^ depth m)
* where
* nelem = mapSize m
*
* depth :: (Map a b) -> Int
* depth Tip = 0
* depth (Bin _ _ _ l r) = 1 + (max `on` depth) l r
* depth :: (Map a b) -> Int
* depth Tip = 0
* depth (Bin _ _ _ l r) = 1 + (max `on` depth) l r
*
* @invariant sizes_correct: A.m :: Map k v:
* case m of
* Tip -> prop True
* b=:(Bin _ _ _ l r) ->
* mapSize b =.= 1 + mapSize l + mapSize r /\
* sizes_correct l /\
* sizes_correct r
* case m of
* Tip -> prop True
* b=:(Bin _ _ _ l r) ->
* mapSize b =.= 1 + mapSize l + mapSize r /\
* sizes_correct l /\
* sizes_correct r
*/
:: Map k v
= Bin !Int !k !v !(Map k v) !(Map k v)
......@@ -123,9 +123,9 @@ instance < (Map k v) | Ord k & Ord v
* Check if a Map is empty.
* @type (Map k a) -> Bool
* @property equivalence with size 0: A.m :: Map k v:
* mapSize m == 0 <==> null m
* mapSize m == 0 <==> null m
* @property equivalence with newMap: A.m :: Map k v:
* m == newMap <==> null m
* m == newMap <==> null m
* @complexity O(1)
*/
null mp :== case mp of
......@@ -136,7 +136,7 @@ null mp :== case mp of
* Create an empty Map.
* @result An empty map
* @property is null:
* null newMap
* null newMap
* @complexity O(1)
*/
newMap :: w:(Map k u:v), [ w <= u]
......@@ -150,7 +150,7 @@ singleton :: !k !v -> Map k v
/**
* The number of elements in a Map.
* @property correctness: A.m :: Map k v:
* mapSize m =.= length (removeDup (keys m))
* mapSize m =.= length (removeDup (keys m))
*/
mapSize :: !(Map k v) -> Int
......@@ -162,11 +162,11 @@ mapSize :: !(Map k v) -> Int
* @param The original mapping
* @result The modified mapping with the added value
* @property correctness: A.m :: Map k v; k :: k; v :: v:
* get k m` =.= Just v /\ // Correctly put
* check all_present [kv \\ kv=:(k`,_) <- toList m | k <> k`] m` /\ // Other elements untouched
* integrity m`
* where
* m` = put k v m
* get k m` =.= Just v /\ // Correctly put
* check all_present [kv \\ kv=:(k`,_) <- toList m | k <> k`] m` /\ // Other elements untouched
* integrity m`
* where
* m` = put k v m
* @complexity O(log n)
*/
put :: !k !a !(Map k a) -> Map k a | < k
......@@ -202,11 +202,11 @@ getU :: !k !w:(Map k v) -> x:(!Maybe v, !y:(Map k v)) | == k & < k, [ x <= y, w
* @param The original mapping
* @result The modified mapping with the value/key removed
* @property correctness: A.m :: Map k v; k :: k:
* get k m` =.= Nothing /\ // Correctly deleted
* check all_present [kv \\ kv=:(k`,_) <- toList m | k <> k`] m` /\ // Other elements untouched
* integrity m`
* where
* m` = del k m
* get k m` =.= Nothing /\ // Correctly deleted
* check all_present [kv \\ kv=:(k`,_) <- toList m | k <> k`] m` /\ // Other elements untouched
* integrity m`
* where
* m` = del k m
*/
del :: !k !(Map k a) -> Map k a | < k
......@@ -270,11 +270,11 @@ toAscList m :== foldrWithKey (\k x xs -> [(k,x):xs]) [] m
* @param A list of key/value tuples
* @result A mapping containing all the tuples in the list
* @property correctness: A.elems :: [(k,v)]:
* check all_present elems m /\ // All elements put
* check all_from m elems /\ // No other elements
* integrity m
* where
* m = fromList elems
* check all_present elems m /\ // All elements put
* check all_from m elems /\ // No other elements
* integrity m
* where
* m = fromList elems
* @complexity O(n*log n)
*/
fromList :: !u:[v:(a, b)] -> Map a b | == a & < a, [u <= v]
......@@ -297,7 +297,7 @@ derive gLexOrd Map
/**
* Check if a key exists in a Map.
* @property correctness: A.k :: k; m :: Map k v:
* member k m <==> isMember k (keys m)
* member k m <==> isMember k (keys m)
* @complexity O(log n)
*/
member :: !k !(Map k a) -> Bool | < k
......@@ -306,7 +306,7 @@ member :: !k !(Map k a) -> Bool | < k
* Checks if a key is not a member of a Map.
* @type k (Map k v) -> Bool | < k
* @property correctness: A.k :: k; m :: Map k v:
* notMember k m <==> not (isMember k (keys m))
* notMember k m <==> not (isMember k (keys m))
*/
notMember k m :== not (member k m)
......@@ -314,7 +314,7 @@ notMember k m :== not (member k m)
* Find an element in a Map.
* Aborts when the element is not found.
* @property correctness: A.k :: k; v :: v; m :: Map k v:
* find k (put k v m) =.= v
* find k (put k v m) =.= v
* @complexity O(log n)
*/
find :: !k !(Map k a) -> a | < k
......@@ -326,9 +326,9 @@ find :: !k !(Map k a) -> a | < k
* @param The default.
* @param The key to look up.
* @property correctness: A.k :: k; v :: v; m :: Map k v:
* findWithDefault default k (put k v m) =.= v /\
* findWithDefault default k (del k m) =.= default
* where default = gDefault{|*|}
* findWithDefault default k (put k v m) =.= v /\
* findWithDefault default k (del k m) =.= default
* where default = gDefault{|*|}
* @complexity O(log n)
*/
findWithDefault :: !a !k !(Map k a) -> a | < k
......@@ -340,9 +340,9 @@ findWithDefault :: !a !k !(Map k a) -> a | < k
*
* @param The element you're looking for.
* @property correctness: A.v :: v; m :: Map k v:
* case [k \\ (k,v`) <- toList m | v == v`] of
* [] -> findKey v m =.= Nothing
* [k:_] -> findKey v m =.= Just k
* case [k \\ (k,v`) <- toList m | v == v`] of
* [] -> findKey v m =.= Nothing
* [k:_] -> findKey v m =.= Just k
* @complexity O(n)
*/
findKey :: !a !(Map k a) -> Maybe k | == a
......@@ -353,9 +353,9 @@ findKey :: !a !(Map k a) -> Maybe k | == a
*
* @param The search function for checking values in the Map.
* @property correctness: A.p :: Predicate v; m :: Map k v:
* case [k \\ (k,v) <- toList m | pred p v] of
* [] -> findKeyWith (pred p) m =.= Nothing
* [k:_] -> findKeyWith (pred p) m =.= Just k
* case [k \\ (k,v) <- toList m | pred p v] of
* [] -> findKeyWith (pred p) m =.= Nothing
* [k:_] -> findKeyWith (pred p) m =.= Just k
* @complexity O(n)
*/
findKeyWith :: !(a -> Bool) !(Map k a) -> Maybe k
......@@ -367,10 +367,10 @@ findKeyWith :: !(a -> Bool) !(Map k a) -> Maybe k
* @param The result if the second parameter does not occur as a value in the Map.
* @param The element you're looking for.
* @property correctness: A.v :: v; m :: Map k v:
* case findKey v m of
* Nothing -> findKeyWithDefault default v m =.= default
* Just k -> findKeyWithDefault default v m =.= k
* where default = gDefault{|*|}
* case findKey v m of
* Nothing -> findKeyWithDefault default v m =.= default
* Just k -> findKeyWithDefault default v m =.= k
* where default = gDefault{|*|}
* @complexity O(n)
*/
findKeyWithDefault :: !k !a !(Map k a) -> k | == a
......@@ -382,10 +382,10 @@ findKeyWithDefault :: !k !a !(Map k a) -> k | == a
* @param The search function for checking values in the Map.
* @param The result when all values in the Map check as False.
* @property correctness: A.p :: Predicate v; m :: Map k v:
* case findKeyWith (pred p) m of
* Nothing -> findKeyWithDefaultWith (pred p) default m =.= default
* Just k -> findKeyWithDefaultWith (pred p) default m =.= k
* where default = gDefault{|*|}
* case findKeyWith (pred p) m of
* Nothing -> findKeyWithDefaultWith (pred p) default m =.= default
* Just k -> findKeyWithDefaultWith (pred p) default m =.= k
* where default = gDefault{|*|}
* @complexity O(n)
*/
findKeyWithDefaultWith :: !(a -> Bool) !k !(Map k a) -> k
......
......@@ -22,45 +22,45 @@ definition module Data.Set
* by Lszl Domoszlai, 2013.
*
* @property-bootstrap
* import StdBool, StdChar, StdInt, StdOrdList, StdTuple
* from StdList import ++, all, isMember, removeDup,
* instance == [a], instance length []
* import qualified StdList
* from Data.Func import on, `on`
* import Data.GenLexOrd
* import StdBool, StdChar, StdInt, StdOrdList, StdTuple
* from StdList import ++, all, isMember, removeDup,
* instance == [a], instance length []
* import qualified StdList
* from Data.Func import on, `on`
* import Data.GenLexOrd
*
* derive genShow Maybe
* genShow{|Set|} show sep p xs rest = ["Set{":showList (toList xs) ["}":rest]]
* where
* showList [x] rest = show sep False x rest
* showList [x:xs] rest = show sep False x [",":showList xs rest]
* showList [] rest = rest
* derive genShow Maybe
* genShow{|Set|} show sep p xs rest = ["Set{":showList (toList xs) ["}":rest]]
* where
* showList [x] rest = show sep False x rest
* showList [x:xs] rest = show sep False x [",":showList xs rest]
* showList [] rest = rest
*
* :: Predicate a = ConstTrue | IsMember [a]
* :: Predicate a = ConstTrue | IsMember [a]
*
* pred :: (Predicate a) a -> Bool | Eq a
* pred ConstTrue _ = True
* pred (IsMember cs) c = isMember c cs
* pred :: (Predicate a) a -> Bool | Eq a
* pred ConstTrue _ = True
* pred (IsMember cs) c = isMember c cs
*
* derive class Gast Predicate
* derive gPrint Maybe, Set
* derive class Gast Predicate
* derive gPrint Maybe, Set
*
* // Check that all elements from a list are in a set.
* contains :: (Set a) [a] -> Bool | < a
* contains d xs = all (\x -> member x d) xs
* // Check that all elements from a list are in a set.
* contains :: (Set a) [a] -> Bool | < a
* contains d xs = all (\x -> member x d) xs
*
* // Check that no elements from a list are in a set.
* does_not_contain :: (Set a) [a] -> Bool | < a
* does_not_contain d ys = all (\y -> notMember y d) ys
* // Check that no elements from a list are in a set.
* does_not_contain :: (Set a) [a] -> Bool | < a
* does_not_contain d ys = all (\y -> notMember y d) ys
*
* // Check that all elements from a set are in a list.
* all_in :: (Set a) [a] -> Bool | Eq a
* all_in s xs = all (\e -> isMember e xs) (toList s)
* // Check that all elements from a set are in a list.
* all_in :: (Set a) [a] -> Bool | Eq a
* all_in s xs = all (\e -> isMember e xs) (toList s)
*
* @property-test-with a = Char
*
* @property-test-generator [a] -> Set a | < a
* gen xs = fromList xs
* gen xs = fromList xs
*/
from StdOverloaded import class ==, class < (..)
......@@ -77,30 +77,30 @@ from Data.Foldable import class Foldable
* A `Set a` is an unordered, uncounted collection of values of type `a`.
*
* @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 "sizes_correct" (sizes_correct s)
* // Check that the data structure is still correct.
* name "no_duplicates" (no_duplicates s) /\
* name "log_size" (log_size 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
* xs =.= removeDup xs where xs = toList s
*
* @invariant log_size: A.s :: Set a:
* check (<) nelem (2 ^ depth s)
* where
* nelem = size s
* check (<) nelem (2 ^ depth s)
* where
* nelem = size s
*
* depth :: (Set a) -> Int
* depth Tip = 0
* depth (Bin _ _ l r) = 1 + (max `on` depth) l r
* depth :: (Set a) -> Int
* depth Tip = 0
* depth (Bin _ _ l r) = 1 + (max `on` depth) l r
*
* @invariant sizes_correct: A.s :: Set a:
* case s of
* Tip -> prop True
* b=:(Bin _ _ l r) ->
* size b =.= 1 + size l + size r /\
* sizes_correct l /\
* sizes_correct r
* case s of
* Tip -> prop True
* b=:(Bin _ _ l r) ->
* size b =.= 1 + size l + size r /\
* sizes_correct l /\
* sizes_correct r
*/
:: Set a = Tip
| Bin !Int !a !(Set a) !(Set a)
......@@ -115,9 +115,9 @@ instance Foldable Set
* True iff this is the empty set.
* @type (Set a) -> Bool
* @property equivalence with size 0: A.s :: Set a:
* size s == 0 <==> null s
* size s == 0 <==> null s
* @property equivalence with newSet: A.s :: Set a:
* s == newSet <==> null s
* s == newSet <==> null s
*/
null s :== case s of
Tip -> True
......@@ -127,7 +127,7 @@ null s :== case s of
* The number of elements in the set.
* @type (Set a) -> Int
* @property correctness: A.s :: Set a:
* size s =.= length (toList s)
* size s =.= length (toList s)
*/
size s :== case s of
Tip -> 0
......@@ -137,7 +137,7 @@ size s :== case s of
* Is the element in the set?
* @complexity O(log n)
* @property correctness: A.x :: a; s :: Set a:
* member x s <==> isMember x (toList s)
* member x s <==> isMember x (toList s)
*/
member :: !a !(Set a) -> Bool | < a
......@@ -153,7 +153,7 @@ notMember x t :== not (member x t)
* @type (Set a) (Set a) -> Bool | <, == a
* @complexity O(n+m)
* @property correctness: A.xs :: Set a; ys :: Set a:
* isSubsetOf xs ys <==> all (\x -> isMember x (toList ys)) (toList xs)
* isSubsetOf xs ys <==> all (\x -> isMember x (toList ys)) (toList xs)
*/
isSubsetOf t1 t2 :== (size t1 <= size t2) && (isSubsetOfX t1 t2)
......@@ -164,10 +164,10 @@ isSubsetOfX :: !(Set a) !(Set a) -> Bool | < a
* @type (Set a) (Set a) -> Bool | <, == a
* @complexity O(n+m)
* @property correctness: A.xs :: Set a; ys :: Set a:
* isProperSubsetOf xs ys
* <==> all (\x -> isMember x ys`) xs` && not (all (\y -> isMember y xs`) ys`)
* where
* (xs`,ys`) = (toList xs, toList ys)
* isProperSubsetOf xs ys
* <==> all (\x -> isMember x ys`) xs` && not (all (\y -> isMember y xs`) ys`)
* where
* (xs`,ys`) = (toList xs, toList ys)
*/
isProperSubsetOf s1 s2 :== (size s1 < size s2) && (isSubsetOf s1 s2)
......@@ -175,7 +175,7 @@ isProperSubsetOf s1 s2 :== (size s1 < size s2) && (isSubsetOf s1 s2)
* The empty set.
* @complexity O(1)
* @property is null:
* null newSet
* null newSet
*/
newSet :: Set a
......@@ -191,10 +191,10 @@ singleton :: !u:a -> w:(Set u:a), [w <= u]
*
* @complexity O(log n)
* @property correctness: A.x :: a; xs :: Set a:
* let xs` = insert x xs in
* check member x xs` /\ // Membership
* check contains xs` (toList xs) /\ // Rest untouched
* integrity xs` // Data structure integrity
* let xs` = insert x xs in
* check member x xs` /\ // Membership
* check contains xs` (toList xs) /\ // Rest untouched
* integrity xs` // Data structure integrity
*/
insert :: !a !.(Set a) -> Set a | < a
......@@ -203,10 +203,10 @@ insert :: !a !.(Set a) -> Set a | < a
*
* @complexity O(log n)
* @property correctness: A.x :: a; xs :: Set a:
* let xs` = delete x xs in
* check notMember x xs` /\ // Membership
* check contains xs` [x` \\ x` <- toList xs | x` <> x] /\ // Rest untouched
* integrity xs` // Data structure integrity
* let xs` = delete x xs in
* check notMember x xs` /\ // Membership
* check contains xs` [x` \\ x` <- toList xs | x` <> x] /\ // Rest untouched
* integrity xs` // Data structure integrity
*/
delete :: !a !.(Set a) -> Set a | < a
......@@ -214,7 +214,7 @@ delete :: !a !.(Set a) -> Set a | < a
* The minimal element of a set.
* @complexity O(log n)
* @property correctness: A.xs :: Set a:
* minList (toList xs) == findMin xs
* minList (toList xs) == findMin xs
* @precondition not (null xs)
*/
findMin :: !(Set a) -> a
......@@ -223,7 +223,7 @@ findMin :: !(Set a) -> a
* The maximal element of a set.
* @complexity O(log n)
* @property correctness: A.xs :: Set a:
* maxList (toList xs) == findMax xs
* maxList (toList xs) == findMax xs
* @precondition not (null xs)
*/
findMax :: !(Set a) -> a
......@@ -232,12 +232,12 @@ findMax :: !(Set a) -> a
* Delete the minimal element.
* @complexity O(log n)
* @property correctness: A.xs :: Set a:
* case xs of
* Tip -> prop (null (deleteMin newSet))
* xs -> let xs` = deleteMin xs in
* check notMember (minList (toList xs)) xs` /\
* size xs` =.= size xs - 1 /\
* integrity xs`
* case xs of
* Tip -> prop (null (deleteMin newSet))
* xs -> let xs` = deleteMin xs in
* check notMember (minList (toList xs)) xs` /\
* size xs` =.= size xs - 1 /\
* integrity xs`
*/
deleteMin :: !.(Set a) -> Set a
......@@ -245,12 +245,12 @@ deleteMin :: !.(Set a) -> Set a
* Delete the maximal element.
* @complexity O(log n)
* @property correctness: A.xs :: Set a:
* case xs of
* Tip -> prop (null (deleteMax newSet))
* xs -> let xs` = deleteMax xs in
* check notMember (maxList (toList xs)) xs` /\
* size xs` =.= size xs - 1 /\
* integrity xs`
* case xs of
* Tip -> prop (null (deleteMax newSet))
* xs -> let xs` = deleteMax xs in
* check notMember (maxList (toList xs)) xs` /\
* size xs` =.= size xs - 1 /\
* integrity xs`
*/
deleteMax :: !.(Set a) -> Set a
......@@ -258,9 +258,9 @@ deleteMax :: !.(Set a) -> Set a
* deleteFindMin set = (findMin set, deleteMin set)
* @complexity O(log n)
* @property correctness: A.xs :: Set a:
* let (m,xs`) = deleteFindMin xs in
* m =.= min /\ notMember min xs`
* where min = minList (toList xs)
* let (m,xs`) = deleteFindMin xs in
* m =.= min /\ notMember min xs`
* where min = minList (toList xs)
* @precondition not (null xs)
*/
deleteFindMin :: !.(Set a) -> (!a, !Set a)
......@@ -269,9 +269,9 @@ deleteFindMin :: !.(Set a) -> (!a, !Set a)
* deleteFindMax set = (findMax set, deleteMax set)
* @complexity O(log n)
* @property correctness: A.xs :: Set a:
* let (m,xs`) = deleteFindMax xs in
* m =.= max /\ notMember max xs`
* where max = maxList (toList xs)
* let (m,xs`) = deleteFindMax xs in
* m =.= max /\ notMember max xs`
* where max = maxList (toList xs)
* @precondition not (null xs)
*/
deleteFindMax :: !.(Set a) -> (!a, !Set a)
......@@ -281,9 +281,9 @@ deleteFindMax :: !.(Set a) -> (!a, !Set a)
* or 'Nothing' if passed an empty set.
* @complexity O(log n)
* @property correctness: A.xs :: Set a:
* if (null xs)
* (Nothing =.= minView xs)
* (Just (deleteFindMin xs) =.= minView xs)
* if (null xs)
* (Nothing =.= minView xs)
* (Just (deleteFindMin xs) =.= minView xs)
*/
minView :: !.(Set a) -> .(Maybe (!a, !Set a))
......@@ -292,9 +292,9 @@ minView :: !.(Set a) -> .(Maybe (!a, !Set a))
* or 'Nothing' if passed an empty set.
* @complexity O(log n)
* @property correctness: A.xs :: Set a:
* if (null xs)
* (Nothing =.= maxView xs)
* (Just (deleteFindMax xs) =.= maxView xs)
* if (null xs)
* (Nothing =.= maxView xs)
* (Just (deleteFindMax xs) =.= maxView xs)
*/
maxView :: !.(Set a) -> .(Maybe (!a, !Set a))
......@@ -303,12 +303,12 @@ maxView :: !.(Set a) -> .(Maybe (!a, !Set a))