SID_2: THEORY
BEGIN

%%%
%%% This is a refined prototype for a project on searching.  It uses a very simple
%%% search structure, lists of integers, which serve as search keys.  As before,
%%% information associated with a key is omitted because we're only interested in
%%% adding, finding, and deleting.
%%% 
%%% The refinement is to restrict our lists to contain at most one occurance of
%%% any key.  Under this restriction, deletion can in some cases terminate faster.
%%% This formulations also Inserts elements at the head of the list, which might
%%% be a reasonable thing to do if the application has locality properties.

slist: TYPE = list[int]

i,j,k: VAR int

%%%
%%% Define a function that counts the number of occurences of a key, k, in
%%% a list, l.
%%%
Count(k:int, l:slist): RECURSIVE nat =
  CASES l OF
    null: 0,
    cons(j, tl): (IF j=k THEN 1 ELSE 0 ENDIF) + Count(k, tl)
  ENDCASES
  MEASURE l BY <<

Count_lemma: LEMMA  forall (j,k:int, l:slist): Count(k, l) <= Count(k, cons(j,l))

%%%
%%% Now define a "good" slist to be on in which all keys occur at most once
%%%

glist:TYPE = {l:slist | FORALL k: Count(k, l) <= 1} CONTAINING null[int]

l,l1,l2: VAR glist

%%%
%%% S for "search".  S returns the list cell associated with the target key,
%%% or null if the search fails.  This time, we'll restrict S's domain to
%%% good lists, and similarly with D and I.
%%%

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

%%%
%%% Here is a potentially useful fact, saying that if S returns
%%% a cons-node, it contains the right key.  
%%%

S_spec_a: LEMMA cons?(S(k, l)) IMPLIES car(S(k, l)) = k

%%%
%%% D for "delete".
%%% Note that we can optimize the case where D deletes
%%%   because there can be no more occurences of the key.
%%% CAUTION: this definition generates important TCCs
%%%   to prove that D(k,l) actually returns a glist.
%%%

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

%%%
%%% Specifications relating S and D.
%%%

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))))


%%%
%%% I for "insert".
%%% I "caches" the key at the head of the list,
%%%   but must now delete subsequent occurances, if any.
%%% I is still guaranteed to produce a non-empty slist
%%%

I(k, l): glist = cons(k, D(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))


%%%
%%% More correctness properties, combining S, I and D
%%%

SID_spec_a: THEOREM S(k, D(k, I(k, l))) = null
SID_spec_b: THEOREM k /= j IMPLIES car(S(j, D(k, I(j, l)))) = j

%%%
%%% 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_2