Complete proof rules for strong fairness and strong extreme fairness (Q685427)

The standard notion of strong fairness is extended to apply to repetitive statements with countably infinite sets of directions (represented as an iterative guarded command with countably infinite numbers of guarded elements). The proof rule for (strongly-) fair termination from the reviewer's book ``Fairness'' (1986; Zbl 0602.68007) is extended to apply to such extended repetitive statements, and the extended rule is shown to be sound and (semantically) complete. The main technical difficulty overcome here is that auxiliary fair termination assertions arising from the recursive application of (a clause of) the rule do not result in any ``syntactic simplification''. It is overcome by a reformulation of the structure of a proof, admitting well-founded induction. Clearly, this extension, in spite of its elegance and naturalness, does not apply directly to programming situations. However, it is a very useful tool for reasoning in other situations which are closer to ``real'' situations, and other constructions can be reduced to it. This is very convincingly shown by providing a sound and (semantically) complete proof rule for termination of an ``ordinary'' repetitive statement under Pnueli's `extreme fairness' notion, which is closely related to a ``real'' situation of termination with probability 1. It applies also to an extension of extreme fairness also to be found in [loc. cit.]. The paper is clearly and lucidly written and should be easy to read by anyone with some knowledge in program verification. As stated by the author, knowledge of the first few chapters of [loc. cit.] would be useful in better appreciating this paper.