LAWS.bend source

LAWS.bend on the hub · documented module

import Baseimport ./lib.bend as Bs# Empty is represented by no words.law to_words_empty:  { Bs.BitSet.to_words(Bs.BitSet.empty()) == Nil{} : List<&2, U32> }law is_empty_empty:  { Bs.BitSet.is_empty(Bs.BitSet.empty()) == True{} : Bool }law size_empty:  { Bs.BitSet.size(Bs.BitSet.empty()) == 0n : Nat }law to_list_empty:  { Bs.BitSet.to_list(Bs.BitSet.empty()) == Nil{} : List<&2, Nat> }law contains_empty:  { Bs.BitSet.contains(Bs.BitSet.empty(), 0n) == False{} : Bool }# The lowest bit is the first singleton.law singleton_zero_words:  { Bs.BitSet.to_words(Bs.BitSet.singleton(0n)) == 1 <> Nil{} : List<&2, U32> }law singleton_zero_list:  { Bs.BitSet.to_list(Bs.BitSet.singleton(0n)) == 0n <> Nil{} : List<&2, Nat> }law singleton_zero_size:  { Bs.BitSet.size(Bs.BitSet.singleton(0n)) == 1n : Nat }law singleton_zero_contains:  { Bs.BitSet.contains(Bs.BitSet.singleton(0n), 0n) == True{} : Bool }law remove_singleton_zero:  { Bs.BitSet.remove(Bs.BitSet.singleton(0n), 0n) == Bs.BitSet.empty() : Bs.BitSet }law insert_singleton_idempotent:  { Bs.BitSet.insert(Bs.BitSet.singleton(0n), 0n)      == Bs.BitSet.singleton(0n) : Bs.BitSet }law union_empty_singleton:  { Bs.BitSet.union(Bs.BitSet.empty(), Bs.BitSet.singleton(0n))      == Bs.BitSet.singleton(0n) : Bs.BitSet }law intersect_empty_singleton:  { Bs.BitSet.intersect(Bs.BitSet.empty(), Bs.BitSet.singleton(0n))      == Bs.BitSet.empty() : Bs.BitSet }# Small boundary cases exercise the word layout.law singleton_one_words:  { Bs.BitSet.to_words(Bs.BitSet.singleton(1n)) == 2 <> Nil{} : List<&2, U32> }law singleton_one_list:  { Bs.BitSet.to_list(Bs.BitSet.singleton(1n)) == 1n <> Nil{} : List<&2, Nat> }law singleton_thirty_one:  { Bs.BitSet.to_list(Bs.BitSet.singleton(31n)) == 31n <> Nil{} : List<&2, Nat> }law singleton_thirty_two_words:  { Bs.BitSet.to_words(Bs.BitSet.singleton(32n)) == 0 <> 1 <> Nil{} : List<&2, U32> }law singleton_thirty_two_list:  { Bs.BitSet.to_list(Bs.BitSet.singleton(32n)) == 32n <> Nil{} : List<&2, Nat> }law contains_absent_singleton:  { Bs.BitSet.contains(Bs.BitSet.singleton(0n), 1n) == False{} : Bool }law insert_zero_empty:  { Bs.BitSet.insert(Bs.BitSet.empty(), 0n) == Bs.BitSet.singleton(0n) : Bs.BitSet }law insert_thirty_two_empty:  { Bs.BitSet.insert(Bs.BitSet.empty(), 32n)      == Bs.BitSet.singleton(32n) : Bs.BitSet }law remove_absent_empty:  { Bs.BitSet.remove(Bs.BitSet.empty(), 32n) == Bs.BitSet.empty() : Bs.BitSet }law remove_other_singleton:  { Bs.BitSet.remove(Bs.BitSet.singleton(0n), 1n)      == Bs.BitSet.singleton(0n) : Bs.BitSet }law remove_one_from_two:  { Bs.BitSet.remove(Bs.BitSet.insert(Bs.BitSet.singleton(0n), 1n), 0n)      == Bs.BitSet.singleton(1n) : Bs.BitSet }law union_two_bits:  { Bs.BitSet.to_list(Bs.BitSet.union(Bs.BitSet.singleton(0n), Bs.BitSet.singleton(1n)))      == 0n <> 1n <> Nil{} : List<&2, Nat> }law union_across_words:  { Bs.BitSet.to_words(Bs.BitSet.union(Bs.BitSet.singleton(0n), Bs.BitSet.singleton(32n)))      == 1 <> 1 <> Nil{} : List<&2, U32> }law intersect_disjoint:  { Bs.BitSet.intersect(Bs.BitSet.singleton(0n), Bs.BitSet.singleton(1n))      == Bs.BitSet.empty() : Bs.BitSet }law intersect_same:  { Bs.BitSet.intersect(Bs.BitSet.singleton(32n), Bs.BitSet.singleton(32n))      == Bs.BitSet.singleton(32n) : Bs.BitSet }law from_words_trims_zero_tail:  { Bs.BitSet.from_words(1 <> 0 <> Nil{})      == Bs.BitSet.from_words(1 <> Nil{}) : Bs.BitSet }law from_words_zero_is_empty:  { Bs.BitSet.from_words(0 <> 0 <> Nil{}) == Bs.BitSet.empty() : Bs.BitSet }law u32_singleton_wrapper:  { Bs.BitSet.singleton_u32(0) == Bs.BitSet.singleton(0n) : Bs.BitSet }law u32_insert_wrapper:  { Bs.BitSet.insert_u32(Bs.BitSet.empty(), 32)      == Bs.BitSet.singleton(32n) : Bs.BitSet }