~/bend-docscommunity

proofs/containers/queue/steps.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/steps.bend as Steps

9 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/queue.bend as S
import ../../../src/containers/queue.bend as Q
import ../../../src/containers/types/queue.bend as E
import ./state.bend as ST

Definitions

def is_nil source · line 22 · raw

@-T:Data -> @xs:List<&2, T> -> Bool

def rdy source · line 30 · raw

@-T:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> Bool

the front can be read: nonempty, or the queue is empty

def rdy_nil_back source · line 37 · raw

@-T:Data -> @+m:List<&2, T> -> {rdy(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Sh{m, []}) == True{} : Bool}

Templates

template StepOK source · line 14 · raw

@-T:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Op<T> -> Type

template mk source · line 17 · raw

@-T:Data -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Op<T> -> @sh2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Obs<T> -> @e1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, sh), op) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, sh2), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Obs<T>)} -> @e2:{(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh2), o) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh), op) : Pair(List<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Obs<T>)} -> StepOK(T, sh, op)

template Ready source · line 44 · raw

@-T:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> Type

template ready source · line 47 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> Ready(T, sh)

template Read source · line 60 · raw

@-T:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Obs<T>) -> @spec:Pair(List<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Obs<T>) -> Type

template dequeue_ready source · line 63 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @+hr:{rdy(T, sh) == True{} : Bool} -> Read(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.obs_item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.dequeue_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, sh))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.dequeue(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh)))

template peek_ready source · line 73 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @+hr:{rdy(T, sh) == True{} : Bool} -> Read(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.obs_item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.peek_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, sh))), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.OItem{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.head(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh)))}))

template dq_fin source · line 82 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @+sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, sh1) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>} -> @+em:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh) : List<&2, T>} -> @rd:Read(T, sh1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.obs_item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.dequeue_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, sh1))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.dequeue(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh1))) -> StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Dequeue{})

template dq_rd source · line 89 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @r:Ready(T, sh) -> StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Dequeue{})

template pk_fin source · line 94 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @+sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, sh1) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>} -> @+em:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh) : List<&2, T>} -> @rd:Read(T, sh1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.obs_item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.peek_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, sh1))), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh1), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.OItem{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.item(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.head(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh1)))})) -> StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Peek{})

template pk_rd source · line 101 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @r:Ready(T, sh) -> StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Peek{})

template op_length source · line 108 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Length{})

template op_enqueue source · line 115 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @+x:T -> StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Enqueue{x})

template op_to_list source · line 122 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> StepOK(T, sh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.ToList{})

template step_ok source · line 129 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Op<T> -> StepOK(T, sh, op)

every public operation refines the spec step