SID_1: THEORY
BEGIN

%%%
%%% This is a prototype for a project on searching.  It uses a very simple
%%% search structure, lists of integers, which serve as search keys.  Information
%%% associated with a key is suppressed because we're only interested in adding,
%%% finding, and deleting
%%% 

slist: TYPE = list[int]

l,l1,l2: VAR slist
i,j,k: VAR int

%%%
%%% S for "search".  S returns the list cell associated with the target key,
%%% or null if the search fails.
%%%

S(k, l): RECURSIVE slist =
  CASES l OF
    null: null,
    cons(j, tl): IF k = j THEN l ELSE S(k, tl) ENDIF
  ENDCASES
  MEASURE l by <<

%%%
%%% I for "insert".  All I does is put the key in the list.
%%% I is guaranteed to produce a non-empty slist
%%%

I(k, l): slist = cons(k, l)

%%%
%%% Insert works if:
%%% a)  Search can find what it inserts.
%%% b)  Search can still find whatever was in the list before the insert.
%%%

SI_spec_a: THEOREM car(S(k, I(k,l))) = k
SI_spec_b: THEOREM k /= j IMPLIES S(k, l) = S(k, I(j, l))

%%%
%%% D for "delete".
%%%

D(j, l): RECURSIVE slist =
  CASES l OF
   null: null,
   cons(i, tl): IF i = j
                THEN D(j, tl)
                ELSE cons(i, D(j, tl))
                ENDIF
  ENDCASES
  MEASURE l by <<

%%%
%%% SD_spec_b is changed from the previous version
%%% replacing node equality with simple null?-check.
%%%

SD_spec_a: THEOREM null?(S(k, D(k, l)))
SD_spec_b: THEOREM k /= j IMPLIES (null?(S(k, l)) IFF null?(S(k, D(j, l))))

%%%
%%% This begs the question of what is a sufficient correctness
%%% specification for S, I and D? That is, what is a "minimally
%%% complete" specification, that says everything you need to
%%% say with the fewest & smallest theorems? Suppose, for example,
%%% that S, I, and D were all defined to return null.  Which of the
%%% specification theorems still hold?
%%%

END SID_1