Derivation of a SETL2 Cycle Testing Program

1.  Initial program fragment

--
-- graph e is a binary edge relation
--
s := domain e;  -- compute the set of vertices that are tails of edges
while exists u in {x in s | inverse(e){x} * s = {} } loop
  s := s - {u};	-- inverse(e) stands for {[y,x]: [x,y] in e}
end loop;

2.  The first invariant to be used for speeding up the preceding program
is a reference count

(1)     refcount(x) = #(inverse(e){x}  * s)

which is stored for every value x belonging to the range of e.  If x does
not belong to the range of e, then refcount(x) must be 0.  This
invariant allows us to replace the predicate

inverse(e){x} * s = {}

that appears in the while-loop by the more efficient

refcount(x) ? 0  = 0

To see how this invariant can be established, maintained, and
exploited, let us first consider the following identity, where we
assume that c is some value belonging to the range of e, u belongs to
s, but u does not necessarily belong to inverse(e){c}:

#(inverse(e){c} * (s - {u}) ) = #(inverse(e){c} * s) - #(inverse(e){c} * {u})

Notice that the intersection inverse(e){c} * {u} must evaluate to either
{} or {u}.  It has the value {u} only when u belongs to inverse(e){c},
WHICH IS THE SAME AS WHEN c BELONGS TO e{u}.  Thus we have the identity,

#(inverse(e){c} * {u}) = if c in e{u} then 1 else 0 end if

Now letting refcount_old(c) = #(inverse(e){c} * s) and letting
refcount_new(c) = #(inverse(e){c} * (s - {u}) ), we obtain,

if c in e{u} then
	refcount_new(c)  = refcount_old(c) - 1
else
	refcount_new(c) = refcount_old(c)
end if

Suppose invariant (1) holds for every x in the range of e just prior
to executing assignment s := s - {u}.  Then by preceding analysis, we
know that invariant (1) still holds just after modifying s for all x
in the domain of refcount that doesn't belong to e{u}.  However, for
all x belonging to e{u}, refcount(x) is one greater than it should be.
In order to reestablish refcount just after modifying s, we can
execute the following code just before the change to s:

for c in e{u} loop	   -- find all values c in range e for which
	refcount(c) -:= 1; -- refcount(c) must be decremented
end loop;

We can create all the reference counts just before the assignment
s := domain e; by executing the following code:

refcount := {};
for x in domain e loop
  for c in e{x} loop
    if refcount(c) = om then
	refcount(c) := 1;
    else
	refcount(c) +:= 1;
    end if;
  end loop;
end loop;


Gathering all of the preceding code to establish and maintain refcount, and
simplifying the while-loop predicate as recommended above, we obtain the
following more efficient program fragment:

--
-- graph e is a binary edge relation
--
refcount := {};	-- code to establish invariant refcount
for x in domain e loop
  for c in e{x} loop
    if refcount(c) = om then
	refcount(c) := 1;
    else
	refcount(c) +:= 1;
    end if;
  end loop;
end loop;
s := domain e;  -- compute the set of vertices that are tails of edges
while exists u in {x in s | refcount(x) ? 0 = 0 } loop
  for c in e{u} loop	   -- code to reestablish refcount
	refcount(c) -:= 1;
  end loop;
  s := s - {u};	
end loop;



2.  The second invariant that can be used to improve speed is

zeroset = {x in s | refcount(x) ? 0 = 0}

This invariant can be established by executing the assignment

zeroset := {x in s | refcount(x) ? 0 = 0};

on entry to the while-loop.  Once this invariant is established, it
must be reestablished (by updating zeroset) whenever it is spoiled by
modifications to s or to refcount.  The code to maintain the zeroset
invariant is much easier to understand than the code to maintain
refcount.  Just before executing refcount(c) -:= 1, we can execute

if c in s and refcount(c) = 1 then
  zeroset with:= c;
end if;

Note that testing whether c belongs to s is necessary, since not every
value in the range of e has to belong to s!  Just before s is decremented
at the end of the program, we can execute

zeroset less := u;

No test is needed whether refcount(u) = 0.  We know that refcount(u) =
0 by the way that u is assigned as a side effect of the existential
quantifier.  Our final SETL2 program is thus,



--
-- graph e is a binary edge relation
--
refcount := {};	-- code to establish invariant refcount
for x in domain e loop
  for c in e{x} loop
    if refcount(c) = om then
	refcount(c) := 1;
    else
	refcount(c) +:= 1;
    end if;
  end loop;
end loop;
s := domain e;  -- compute the set of vertices that are tails of edges
zeroset := {x in s | refcount(x) ? 0 = 0}; -- establish zeroset
while exists u in zeroset loop
  for c in e{u} loop	   -- code to reestablish refcount and zeroset
	if c in s and refcount(c) = 1 then
		  zeroset with:= c;
	end if;
	refcount(c) -:= 1;
  end loop;
  zeroset less := u;	    -- reestablish zeroset
  s := s - {u};	
end loop;