~/bend-docscommunity

proofs/containers/queue/proof.bend checks

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

11 imports
import Base
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
import ./steps.bend as PS
import ./trace.bend as FT
import ../../lib/logic.bend as L
import ../../../spec/lib/common.bend as SC
import ../../../spec/lib/sequence.bend as V
import ../../lib/sequence.bend as VL

Definitions

def length_result source · line 60 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.Length.length_result(T, xs)

---- Length, iteration ----

def length_frame source · line 63 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.Length.length_frame(T, xs)

def to_list_model source · line 66 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.Iteration.to_list_model(T, xs)

def to_list_frame source · line 69 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.Iteration.to_list_frame(T, xs)

def enqueue_length source · line 81 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.Append.enqueue_length(T, xs, v)

---- Append: Length + 1, Equal_Prefix (Model'Old, Model), Element (Last'Old + 1) = New_Item ----

def enqueue_prefix source · line 84 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.Append.enqueue_prefix(T, xs, v)

def enqueue_element source · line 87 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.Append.enqueue_element(T, xs, v)

def dequeue_length source · line 91 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.Delete_First.dequeue_length(T, h, t)

---- Delete_First: Length - 1, Range_Shifted (New, Old, First, Last, 1); dequeue returns First_Element'Old ----

def dequeue_shifted source · line 94 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.Delete_First.dequeue_shifted(T, h, t)

def dequeue_result source · line 97 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.Delete_First.dequeue_result(T, h, t)

def dequeue_empty source · line 100 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.Delete_First.dequeue_empty(T)

def peek_first source · line 104 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.First_Element.peek_first(T, h, t)

---- First_Element: Element (Model, First); nothing changes ----

def peek_frame source · line 107 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.First_Element.peek_frame(T, xs)

def peek_empty source · line 110 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.First_Element.peek_empty(T)

Templates

template new_abs source · line 25 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.initial(T)) == [] : List<&2, T>}

template new_real source · line 28 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.new(T) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.initial(T)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>}

template step_ok source · line 31 · raw

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

template shadow_unique source · line 35 · raw

@-T:Data -> @+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, a) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, b) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>} -> {a == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T>}

a queue determines its shadow

template trace_from source · line 38 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Op<T>> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/trace.TraceOK(T, ops, sh0)

template trace_new source · line 42 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Op<T>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/trace.TraceOK(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.initial(T))

arbitrary finite operation traces from the real constructor

template Impl source · line 48 · raw

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

---- the implementation ----

template impl_of source · line 51 · raw

@-T:Data -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Op<T> -> @-Post:(@_:Pair(List<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Obs<T>) -> Type) -> @k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/steps.StepOK(T, sh, op) -> @pf:Post(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh), op)) -> Impl(T, sh, op, Post)

template impl source · line 56 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Op<T> -> @-Post:(@_:Pair(List<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Obs<T>) -> Type) -> @pf:Post(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, sh), op)) -> Impl(T, sh, op, Post)

template new_empty source · line 73 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.initial(T))) == 0n : Nat}

---- Empty_Vector ----

template new_impl source · line 77 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.new(T) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.initial(T)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>}