~/bend-docscommunity

proofs/containers/lru/new.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/new.bend as New

6 imports
import Base
import ../../lib/array.bend as AR
import ../../../spec/containers/lru.bend as SP
import ../../../src/containers/lru.bend as LR
import ./state.bend as ST
import ../../lib/words32.bend as W32

Templates

template empty source · line 10 · raw

@-V:Data -> @+cap:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.Sh<V>

template MadeOK source · line 13 · raw

@-V:Data -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.Made<&2, V> -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Made<V> -> Type

template good_empty source · line 24 · raw

@-V:Data -> @+cap:U32 -> @+hz:{U32.is_eq(cap, 0) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.good(V, empty(V, cap)) == True{} : Bool}

template new_c source · line 34 · raw

@-V:Data -> @+cap:U32 -> @+z:Bool -> @+hz:{U32.is_eq(cap, 0) == z : Bool} -> @+r:Bool -> MadeOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.new_checked(&2, V, cap, z, r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.new_c(V, cap, z, r))

template new_ok source · line 45 · raw

@-V:Data -> @+cap:U32 -> MadeOK(V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.new(&2, V, cap), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.new(V, cap))

THEOREM: new rejects what the specification rejects, with its reason, and otherwise builds the specification's empty cache.