Go backward to
Proving Simple Program Properties
Go up to
Top
Go forward to
Example: Type Correctness
Invariance Properties
TLA formula
always
P
.
Partial correctness
If program has terminated, answer is correct.
Deadlock freedom
Program is not deadlocked.
Mutual exclusion
At most one process is in critical section.
Proofs based on rule INV1.
I
and
[
A
]
_{f}
=>
I'
I
and
always
[
A
]
_{f}
=>
always
I
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998