spec/containers/dlist_iterator.bend
bend-collections-laws-containers@1.0.0.0 · 31 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/doubly_linked_list.bend as DS
3
4# ---- contract (SPARK formal containers) ----
5# Each `<Subprogram>.<clause>` definition below states one Post clause of
6# that SPARK subprogram, as a proposition on this model; the table names the
7# clauses. proofs/containers/dlist_iterator/ proves every clause under its clause name,
8# and its `impl` lemma carries them to the implementation.
9#
10# Contracts of the list iterator in the style of SPARK's formal doubly
11# linked lists' cursor subprograms (SPARKlib
12# src/spark-containers-formal-doubly_linked_lists.ads, AdaCore/SPARKlib
13# master). The iterator owns a list and walks it; its state is the list, the
14# next link, the last-returned link, the direction and the position index.
15# What is proved here is the cursor-state part of SPARK's contracts, over
16# the actual implementation (proof.bend's component laws):
17#
18# SPARK subprogram (.ads line) ours clauses (proof.bend)
19# Has_Element (1814) has_next has_next_state (= next link present)
20# Has_Element (backward) has_previous has_previous_state (= position > 0)
21# Next (1614), at the end: No_Element next next_exhausted (Exhausted, state unchanged)
22# Replace_Element (430), Pre Has_Element set set_requires_current (NoCurrent, unchanged)
23# Delete (978), Pre Has_Element remove remove_requires_current (NoCurrent, unchanged)
24# Delete: cursor moves on removed removed_forward, removed_backward
25# Insert (523): position advances add added_clears_current
26# (the container is returned intact) finish finish_owns
27#
28# Not proved: the element-level Post clauses (Next returns P.Get (Positions,
29# Position + 1); Delete/Insert shift the model), because the iterator walks
30# the list's storage directly and has no sequence refinement proof yet; the
31# list itself (spec/containers/doubly_linked_list.bend) has all of those.