LAWS.bend source
LAWS.bend on the hub 路 documented module
import Baseimport ./main.bend as Bimport ./model.bend as M# Auxiliary string/list algebra, universal.law string_right: for +s: String {String.append(s, "") == s : String}law string_assoc: for +a: String for +b: String for +c: String {String.append(String.append(a,b),c) == String.append(a,String.append(b,c)) : String}law flatten_join: for +a: List<&2,String> for +b: List<&2,String> {M.flatten(M.join(a,b)) == String.append(M.flatten(a),M.flatten(b)) : String}# Universal refinement, including an arbitrary suffix.law emit_model: for +t: B.Builder for +suffix: String {B.emit(t,suffix) == String.append(M.flatten(M.chunks(t)),suffix) : String}law finish_model: for +t: B.Builder {B.finish(t) == M.flatten(M.chunks(t)) : String}law empty: {B.finish(B.empty()) == "" : String}law fragment: for +s: String {B.finish(B.fragment(s)) == s : String}law compose: for +a: B.Builder for +b: B.Builder {B.finish(B.compose(a,b)) == String.append(B.finish(a),B.finish(b)) : String}law append: for +a: B.Builder for +s: String {B.finish(B.append(a,s)) == String.append(B.finish(a),s) : String}law character: for +a: B.Builder for +c: Char {B.finish(B.character(a,c)) == String.append(B.finish(a),SCon{c,SNil{}}) : String}law left_identity: for +a: B.Builder {B.finish(B.compose(B.empty(),a)) == B.finish(a) : String}law right_identity: for +a: B.Builder {B.finish(B.compose(a,B.empty())) == B.finish(a) : String}law associativity: for +a: B.Builder for +b: B.Builder for +c: B.Builder {B.finish(B.compose(B.compose(a,b),c)) == B.finish(B.compose(a,B.compose(b,c))) : String}law empty_fragment: for +a: B.Builder {B.finish(B.append(a,"")) == B.finish(a) : String}# Both old and new observations, not merely old == old.law snapshot: for +a: B.Builder for +s: String {(B.finish(a),B.finish(B.append(a,s))) == (M.flatten(M.chunks(a)),String.append(M.flatten(M.chunks(a)),s)) : String & String}# Inhabited normalization witness: empty, nonempty, Unicode, LF, CR, NUL.law witness: {B.finish(B.character(B.compose(B.append(B.fragment("位"),""),B.fragment("馃檪\r\n")),Chr{0})) == "位馃檪\r\n\0" : String}