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
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine
