equal
deleted
inserted
replaced
8 From Misra, "A Logic for Concurrent Programming", 1994 |
8 From Misra, "A Logic for Concurrent Programming", 1994 |
9 *) |
9 *) |
10 |
10 |
11 header{*Progress*} |
11 header{*Progress*} |
12 |
12 |
13 theory WFair = UNITY: |
13 theory WFair imports UNITY begin |
14 |
14 |
15 text{*The original version of this theory was based on weak fairness. (Thus, |
15 text{*The original version of this theory was based on weak fairness. (Thus, |
16 the entire UNITY development embodied this assumption, until February 2003.) |
16 the entire UNITY development embodied this assumption, until February 2003.) |
17 Weak fairness states that if a command is enabled continuously, then it is |
17 Weak fairness states that if a command is enabled continuously, then it is |
18 eventually executed. Ernie Cohen suggested that I instead adopt unconditional |
18 eventually executed. Ernie Cohen suggested that I instead adopt unconditional |