The UNITY rules for leads-to, based on totality of the commands and weak fairness, are generalized to specifications with nontotal commands and impartiality. The rules and the corresponding predicate transformers are proved to be sound and complete by elementary means. These results are subsequently extended to specifications where the liveness property also contains a finite number of strong fairness assumptions. This is illustrated by means of a proof of starvation freedom for the standard implementation of mutual exclusion by plain semaphores, with strong fairness for the P operations.
A paper is in preparation. A PVS dumpfile is available. PVS users can unzip it and undump it, and inspect the specification and proof files. It is made primarily for author confidence, not for communication. It is therefore not very instructive.
Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink