Go backward to
Invariance Properties
Go up to
Top
Go forward to
Proof
Example: Type Correctness
Type declarations in TLA:
Invariance property assuring that program variables are always from certain domain.
Phi
=>
always
T
natural
x
,
y
T
<=>
(
x
in
Nat
)
and
(
y
in
Nat
).
Must prove:
Init
Phi
=>
T
T
and
[
A
]
<x, y>
=>
T'
Then we know:
Phi
=>
Init
Phi
and
[
A
]
<x, y>
=>
T
and
always
[
A
]
<x, y>
=>
always
T
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998