~/bend-docscommunity

spec/containers/dynamic_array.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/spec/containers/dynamic_array.bend as Dynamic_array

4 imports
import Base
import ../lib/common.bend as C
import ../../src/containers/types/dynamic_array.bend as E
import ../lib/sequence.bend as V

Types

type Model source · line 12 · raw

@-T:Data -> Data

Definitions

def new source · line 15 · raw

@-T:Data -> Model<T>

def with_limit source · line 18 · raw

@-T:Data -> @+k:Nat -> Model<T>

def item_result source · line 21 · raw

@-T:Data -> @x:Maybe<&2, T> -> Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>

def fit source · line 29 · raw

@fuel:Nat -> @+d:Nat -> @+n:Nat -> Nat

Least k >= d with n <= 2^k, searching at most fuel doublings.

def ok_unit source · line 36 · raw

Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>

def pop source · line 39 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @xs:List<&2, T> -> Pair(Model<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)

def step_parts source · line 46 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> Pair(Model<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)

def step source · line 78 · raw

@-T:Data -> @m:Model<T> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> Pair(Model<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)

Every operation: the next model and the observation.

def cons_obs source · line 82 · raw

@-T:Data -> @o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T> -> @r:Pair(Model<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>) -> Pair(Model<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)

def run source · line 87 · raw

@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> @+m:Model<T> -> Pair(Model<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)

Arbitrary finite traces: final model and every observation, in order.

def items source · line 136 · raw

@-T:Data -> @m:Model<T> -> List<&2, T>

def depth source · line 141 · raw

@-T:Data -> @m:Model<T> -> Nat

def nx source · line 146 · raw

@-T:Data -> @+m:Model<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> Model<T>

def ob source · line 149 · raw

@-T:Data -> @+m:Model<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>

def room source · line 155 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> Bool

---- Append: Length + 1, Equal_Prefix (Model'Old, Model), Element (Last_Index'Old + 1) = New_Item ---- room: SPARK's Pre Length < Capacity; here the array doubles once when full and below its limit, so room is Length < 2^depth or depth < limit

def Length.length_result source · line 159 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> Type

Length (284)

def Length.length_frame source · line 163 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> Type

Length (284)

def Capacity.capacity_result source · line 167 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> Type

Capacity (322)

def Capacity.capacity_frame source · line 171 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> Type

Capacity (322)

def Iteration.to_list_model source · line 175 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> Type

iteration (Iter_Model, 1193)

def Iteration.to_list_frame source · line 179 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> Type

iteration (Iter_Model, 1193)

def Empty_Vector.new_empty source · line 183 · raw

@-T:Data -> Type

Empty_Vector (292)

def Empty_Vector.new_capacity source · line 187 · raw

@-T:Data -> Type

Empty_Vector (292)

def Empty_Vector.with_limit_empty source · line 191 · raw

@-T:Data -> @+k:Nat -> Type

Empty_Vector (292)

def Reserve_Capacity.reserve_equal source · line 195 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+n:Nat -> Type

Reserve_Capacity (328)

def Clear.clear_length source · line 199 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> Type

Clear (341)

def Clear.clear_capacity source · line 203 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> Type

Clear (341)

def Element.get_element source · line 207 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> @+v:T -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, xs, i) == Some{v} : Maybe<&2, T>} -> Type

Element (373)

def Element.get_frame source · line 211 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> Type

Element (373)

def Element.get_outside source · line 215 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), i) == True{} : Bool} -> Type

Element (373)

def First_Element.first_element source · line 219 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+h:T -> @+t:List<&2, T> -> Type

First_Element (913)

def Last_Element.last_element source · line 223 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> Type

Last_Element (923)

def Replace_Element.set_length source · line 227 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool} -> Type

Replace_Element (384)

def Replace_Element.set_element source · line 231 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool} -> Type

Replace_Element (384)

def Replace_Element.set_except source · line 235 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == True{} : Bool} -> Type

Replace_Element (384)

def Replace_Element.set_outside source · line 239 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+i:Nat -> @+v:T -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs)) == False{} : Bool} -> Type

Replace_Element (384)

def Append.push_length source · line 243 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+hr:{room(T, l, d, xs) == True{} : Bool} -> Type

Append (706)

def Append.push_prefix source · line 247 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+hr:{room(T, l, d, xs) == True{} : Bool} -> Type

Append (706)

def Append.push_element source · line 251 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+hr:{room(T, l, d, xs) == True{} : Bool} -> Type

Append (706)

def Append.push_full source · line 255 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, T> -> @+v:T -> @+h1:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == False{} : Bool} -> @+h2:{Nat.is_lt(d, l) == False{} : Bool} -> Type

Append (706)

def Delete_Last.pop_length source · line 259 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+h:T -> @+t:List<&2, T> -> Type

Delete_Last (866)

def Delete_Last.pop_prefix source · line 263 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+h:T -> @+t:List<&2, T> -> Type

Delete_Last (866)

def Delete_Last.pop_result source · line 267 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+h:T -> @+t:List<&2, T> -> Type

Delete_Last (866)

def Delete_Last.pop_empty source · line 271 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> Type

Delete_Last (866)