Complete assertional proof rules for progress under weak and strong fairness

Hesselink, W. H., 1-Sep-2013, In : Science of computer programming. 78, 9, p. 1521-1537 17 p.

Research output: Contribution to journalArticleAcademicpeer-review

Copy link to clipboard


  • 2013SciComputProgHesselink1.pdf

    Final publisher's version, 324 KB, PDF document


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. (C) 2012 Elsevier B.V. All rights reserved.

Original languageEnglish
Pages (from-to)1521-1537
Number of pages17
JournalScience of computer programming
Issue number9
Publication statusPublished - 1-Sep-2013


  • UNITY, Temporal logic, Weak fairness, Strong fairness, Proof rules, UNITY LOGIC, PROGRAMS, DERIVATION, REFINEMENT, SYSTEM

ID: 5908464