LAWS.bend source

LAWS.bend on the hub · documented module

import Baseimport ./lib.bend as R# Construction and empty-state laws.law empty_is_new:  for c: Nat  { R.RingBuf.empty(c) == R.RingBuf.new(c) : R.RingBuf }law capacity_new:  for c: Nat  { R.RingBuf.capacity(R.RingBuf.new(c)) == c : Nat }law length_new:  for c: Nat  { R.RingBuf.length(R.RingBuf.new(c)) == 0n : Nat }law empty_new:  for c: Nat  { R.RingBuf.is_empty(R.RingBuf.new(c)) == True{} : Bool }law new_zero:  { R.RingBuf.new(0n) == R.RB{0n, 0n, 0n, Nil{}} : R.RingBuf }law new_one:  { R.RingBuf.new(1n) == R.RB{1n, 0n, 0n, 0 <> Nil{}} : R.RingBuf }# Empty observations and zero-capacity behavior.law pop_empty:  for c: Nat  { R.RingBuf.pop(R.RingBuf.new(c)) == None{} : Maybe<&2, R.RingBuf.Pop> }law peek_empty:  for c: Nat  { R.RingBuf.peek(R.RingBuf.new(c)) == None{} : Maybe<&2, U32> }law to_list_empty:  { R.RingBuf.to_list(R.RingBuf.new(0n)) == Nil{} : List<&2, U32> }law zero_push_fails:  for x: U32  { R.RingBuf.push(R.RingBuf.new(0n), x) == None{} : Maybe<&2, R.RingBuf.Push> }law zero_is_full:  { R.RingBuf.is_full(R.RingBuf.new(0n)) == True{} : Bool }# Singleton push/pop/peek behavior.law push_one:  for x: U32  {    R.RingBuf.push(R.RingBuf.new(1n), x)      == Some{R.PushResult{R.RB{1n, 0n, 1n, x <> Nil{}}}}    : Maybe<&2, R.RingBuf.Push>  }law one_is_full_after_push:  for x: U32  {    R.RingBuf.is_full(R.RB{1n, 0n, 1n, x <> Nil{}}) == True{} : Bool  }law push_full_fails:  for x: U32  for y: U32  {    R.RingBuf.push(R.RB{1n, 0n, 1n, x <> Nil{}}, y)      == None{}    : Maybe<&2, R.RingBuf.Push>  }law peek_one:  for x: U32  {    R.RingBuf.peek(R.RB{1n, 0n, 1n, x <> Nil{}})      == Some{x}    : Maybe<&2, U32>  }law pop_one:  for x: U32  {    R.RingBuf.pop(R.RB{1n, 0n, 1n, x <> Nil{}})      == Some{R.PopResult{x, R.RB{1n, 0n, 0n, x <> Nil{}}}}    : Maybe<&2, R.RingBuf.Pop>  }law to_list_one:  for x: U32  {    R.RingBuf.to_list(R.RB{1n, 0n, 1n, x <> Nil{}})      == x <> Nil{}    : List<&2, U32>  }# A two-slot buffer demonstrates FIFO order and physical wrap-around.law to_list_two:  for x: U32  for y: U32  {    R.RingBuf.to_list(R.RB{2n, 0n, 2n, x <> y <> Nil{}})      == x <> y <> Nil{}    : List<&2, U32>  }law pop_two:  for x: U32  for y: U32  {    R.RingBuf.pop(R.RB{2n, 0n, 2n, x <> y <> Nil{}})      == Some{R.PopResult{x, R.RB{2n, 1n, 1n, x <> y <> Nil{}}}}    : Maybe<&2, R.RingBuf.Pop>  }law wrapped_push:  for x: U32  for y: U32  for z: U32  {    R.RingBuf.push(R.RB{2n, 1n, 1n, x <> y <> Nil{}}, z)      == Some{R.PushResult{R.RB{2n, 1n, 2n, z <> y <> Nil{}}}}    : Maybe<&2, R.RingBuf.Push>  }law wrapped_to_list:  for x: U32  for y: U32  {    R.RingBuf.to_list(R.RB{2n, 1n, 2n, x <> y <> Nil{}})      == y <> x <> Nil{}    : List<&2, U32>  }law length_full:  for x: U32  for y: U32  {    R.RingBuf.length(R.RB{2n, 1n, 2n, x <> y <> Nil{}}) == 2n : Nat  }