Deque

Linear double-ended queue with a ``size`` ghost (LiquidJava ``ArrayDeque``). Ends support push/pop/peek; pop and peek require ``size > 0``. The deque is multiplicity-1. ``discard`` frees an empty deque.
Table of Contents

Types

Deque

(type) linear
linear type Deque a

DequePop

(type)
type DequePop a

DequePeek

(type)
type DequePeek a

DequeLen

(type)
type DequeLen a

Functions

new_deque

Empty deque. Use as ``Deque.new_deque{Int} unit``.
def new_deque (_ : Unit) : {d : Deque a | deque_size d = 0}

push_back

def push_back (x : a) (1 d : Deque a) : {out : Deque a | deque_size out = deque_size d + 1}

push_front

def push_front (x : a) (1 d : Deque a) : {out : Deque a | deque_size out = deque_size d + 1}

pop_back

def pop_back (1 d : Deque a | deque_size d > 0) : {p : DequePop a | pop_size p = deque_size d - 1}

pop_front

def pop_front (1 d : Deque a | deque_size d > 0) : {p : DequePop a | pop_size p = deque_size d - 1}

pop_value

def pop_value (p : DequePop a) : a

pop_deque

def pop_deque (p : DequePop a) : {d : Deque a | deque_size d = pop_size p}

peek_back

def peek_back (1 d : Deque a | deque_size d > 0) : {p : DequePeek a | peek_size p = deque_size d}

peek_front

def peek_front (1 d : Deque a | deque_size d > 0) : {p : DequePeek a | peek_size p = deque_size d}

peek_value

def peek_value (p : DequePeek a) : a

peek_deque

def peek_deque (p : DequePeek a) : {d : Deque a | deque_size d = peek_size p}

len_of

def len_of (1 d : Deque a) : {l : DequeLen a | held_size l = deque_size d}

len_value

def len_value (l : DequeLen a) : {n : Int | n = held_size l && n ≥ 0}

len_deque

def len_deque (l : DequeLen a) : {d : Deque a | deque_size d = held_size l}

discard

def discard (1 d : Deque a | deque_size d = 0) : Unit

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

deque_size

uninterpreted
def deque_size : (d : Deque a) → Int

pop_size

uninterpreted
def pop_size : (p : DequePop a) → Int

peek_size

uninterpreted
def peek_size : (p : DequePeek a) → Int

held_size

uninterpreted
def held_size : (l : DequeLen a) → Int