I found a paper that discusses exactly the issue we are talking
about, in terms of control dependences.
Bill
From:
http://iss.cs.cornell.edu/Publications/Papers/PLDI1996.pdf
Podgurski and Clarke have introduced weak control
dependence [PC90] which is more appropriate than
the classical one for proving total correctness of programs.
In this paper we call it loop control dependence because
we give an alternative definition of it based on the concept of
loop postdominance given below Figure 1 shows a program in
which classical and loop control dependence differ.
Consider node k in the
CFG. In the classical notion k is control dependent on
g -> a. However to prove that k will be executed it is
necessary to prove that the loop a -> b -> a terminates.
Therefore in the context of proving total correctness of
programs it is more appropriate to make k loop control dependent
on the exit of the loop namely the
edge b -> k In programs without cycles the classical
and loop control dependence relations are identical.
[PC90] Andy Podgurski and Lori Clarke A formal
model of program dependences and its implications
for software testing debugging and maintenance
IEEE Transactions on Software Engineering,
Septmeber, 1990.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:08 EDT