Linear iterator protocol (LiquidJava ``Iterator`` / hasNext-before-next).
Phases (``it_phase``):
0 — must call ``has_next`` before ``next``
1 — ``has_next`` returned true; ``next`` is legal
2 — exhausted (``has_next`` returned false); only ``discard`` remains
``it_remaining`` counts unread elements. Construct with ``from_array``.
def from_array (1 arr : Array a) : {it : Iterator a | it_phase it = 0 && it_remaining it = Array.size arr}
has_next
Probe whether more elements remain (phase 0 only).
If remaining > 0, recovers phase 1; otherwise phase 2.
def has_next (1 it : Iterator a | it_phase it = 0) : {
p : IteratorProbe a | probe_remaining p = it_remaining it
&&
(it_remaining it > 0 && probe_has_next p = True || it_remaining it = 0 && probe_has_next p = False)
}
has_next_flag
def has_next_flag (p : IteratorProbe a) : {b : Bool | b = probe_has_next p}
ready_iterator
Recover iterator after a true probe → phase 1, same remaining.
def ready_iterator (p : IteratorProbe a | probe_has_next p = True) : {it : Iterator a | it_phase it = 1 && (it_remaining it = probe_remaining p && it_remaining it > 0)}
exhausted_iterator
Recover iterator after a false probe → phase 2, remaining 0.
def exhausted_iterator (p : IteratorProbe a | probe_has_next p = False) : {it : Iterator a | it_phase it = 2 && (it_remaining it = 0 && probe_remaining p = 0)}
next
Take the next element (phase 1 only); returns to phase 0 with remaining - 1.
def next (1 it : Iterator a | it_phase it = 1 && it_remaining it > 0) : {s : IteratorStep a | step_remaining s = it_remaining it - 1}
next_value
def next_value (s : IteratorStep a) : a
next_iterator
def next_iterator (s : IteratorStep a) : {it : Iterator a | it_phase it = 0 && it_remaining it = step_remaining s}
discard
Drop an exhausted iterator (phase 2).
def discard (1 it : Iterator a | it_phase it = 2) : Unit
Uninterpreted
Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.