LAWS.bend source
LAWS.bend on the hub · documented module
import Baseimport ./lib.bend as R# Bound and constructor semantics.law bound_inclusive: { R.Range.Bound.is_inclusive(R.Inclusive{}) == True{} : Bool }law bound_exclusive: { R.Range.Bound.is_inclusive(R.Exclusive{}) == False{} : Bool }law nat_make: { R.Range.make(2n, R.Inclusive{}, 5n, R.Exclusive{}) == R.NR{2n, R.Inclusive{}, 5n, R.Exclusive{}} : R.Range.NatRange }law nat_closed: { R.Range.Nat.closed(2n, 5n) == R.NR{2n, R.Inclusive{}, 5n, R.Inclusive{}} : R.Range.NatRange }law u32_make: { R.Range.make_u32(2, R.Inclusive{}, 5, R.Exclusive{}) == R.UR{2, R.Inclusive{}, 5, R.Exclusive{}} : R.Range.U32Range }# Nat endpoint semantics, emptiness, cardinality, and enumeration.law nat_closed_open: { R.Range.Nat.to_list(R.Range.Nat.closed_open(2n, 5n)) == 2n <> 3n <> 4n <> Nil{} : List<&2, Nat> }law nat_closed_open_length: { R.Range.Nat.length(R.Range.Nat.closed_open(2n, 5n)) == 3n : Nat }law nat_open_closed: { R.Range.Nat.to_list(R.Range.Nat.open_closed(2n, 5n)) == 3n <> 4n <> 5n <> Nil{} : List<&2, Nat> }law nat_open: { R.Range.Nat.to_list(R.Range.Nat.open(2n, 5n)) == 3n <> 4n <> Nil{} : List<&2, Nat> }law nat_singleton: { R.Range.Nat.length(R.Range.Nat.closed(4n, 4n)) == 1n : Nat }law nat_open_singleton_empty: { R.Range.Nat.is_empty(R.Range.Nat.open(4n, 4n)) == True{} : Bool }law nat_reversed_empty: { R.Range.Nat.to_list(R.Range.Nat.closed(5n, 2n)) == Nil{} : List<&2, Nat> }law nat_contains_inside: { R.Range.Nat.contains(R.Range.Nat.closed_open(2n, 5n), 4n) == True{} : Bool }law nat_contains_excluded_upper: { R.Range.Nat.contains(R.Range.Nat.closed_open(2n, 5n), 5n) == False{} : Bool }law nat_contains_excluded_lower: { R.Range.Nat.contains(R.Range.Nat.open_closed(2n, 5n), 2n) == False{} : Bool }law nat_overlap_touch_closed: { R.Range.Nat.overlap(R.Range.Nat.closed(1n, 3n), R.Range.Nat.closed(3n, 5n)) == True{} : Bool }law nat_overlap_touch_open: { R.Range.Nat.overlaps(R.Range.Nat.closed(1n, 3n), R.Range.Nat.open(3n, 5n)) == False{} : Bool }law nat_overlap_disjoint: { R.Range.Nat.overlap(R.Range.Nat.closed(1n, 2n), R.Range.Nat.closed(3n, 5n)) == False{} : Bool }law nat_clamp_low: { R.Range.Nat.clamp(R.Range.Nat.closed(2n, 5n), 0n) == 2n : Nat }law nat_clamp_mid: { R.Range.Nat.clamp(R.Range.Nat.closed(2n, 5n), 4n) == 4n : Nat }law nat_clamp_high: { R.Range.Nat.clamp(R.Range.Nat.closed(2n, 5n), 9n) == 5n : Nat }# U32 has the same endpoint semantics and uses Nat for its length.law u32_closed_open_length: { R.Range.U32.length(R.Range.U32.closed_open(2, 5)) == 3n : Nat }law u32_closed_open_list: { R.Range.U32.to_list(R.Range.U32.closed_open(2, 5)) == 2 <> 3 <> 4 <> Nil{} : List<&2, U32> }law u32_open_list: { R.Range.U32.to_list(R.Range.U32.open(2, 5)) == 3 <> 4 <> Nil{} : List<&2, U32> }law u32_singleton: { R.Range.U32.length(R.Range.U32.closed(7, 7)) == 1n : Nat }law u32_open_singleton_empty: { R.Range.U32.is_empty(R.Range.U32.open(7, 7)) == True{} : Bool }law u32_contains_inside: { R.Range.U32.contains(R.Range.U32.closed_open(2, 5), 4) == True{} : Bool }law u32_contains_excluded_upper: { R.Range.U32.contains(R.Range.U32.closed_open(2, 5), 5) == False{} : Bool }law u32_overlap_touch_open: { R.Range.U32.overlap(R.Range.U32.closed(1, 3), R.Range.U32.open(3, 5)) == False{} : Bool }law u32_overlap_disjoint: { R.Range.U32.overlaps(R.Range.U32.closed(1, 2), R.Range.U32.closed(3, 5)) == False{} : Bool }law u32_clamp_low: { R.Range.U32.clamp(R.Range.U32.closed(2, 5), 0) == 2 : U32 }law u32_clamp_high: { R.Range.U32.clamp(R.Range.U32.closed(2, 5), 9) == 5 : U32 }