Mysterious D

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hello:

In the abstract of SCMFSA_9, theorem 11, there is a mysterious identifier
D which does not have a declaration visible in the abstract.  Actually,
there is no mystery as in the article there is:

	set D = Int-Locations U FinSeq-Locations;

which has been removed by the abstractor.

I suggest that such global "set" constructs be retained in the
abstract.  Furthermore, I see some use for "set" constructs
at the level of the definition block and they also should be visible
in the abstract.  For instance, instead of:

definition
 let a be Int-Location, I be Macro-Instruction,
     iset be finite Subset of Int-Locations;
 func iset-times(a, I) -> Macro-Instruction equals
:Ltimes:
 FirstRWNotIn (iset U UsedIntLoc Times(a, I)) := a ';'
 Times(FirstRWNotIn (iset U UsedIntLoc Times(a, I)), I);
 correctness;
end;

I would much prefer to write:

definition
 let a be Int-Location, I be Macro-Instruction,
     iset be finite Subset of Int-Locations;
  set aux = FirstRWNotIn (iset U UsedIntLoc Times(a, I));
 func iset-times(a, I) -> Macro-Instruction equals
:Ltimes:
 aux := a ';'  Times(aux, I);
 correctness;
end;


-- 
Piotr Rudnicki