1	import Base
2	import ./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.