Go up to
Top
Go forward to
Invariance Properties
Proving Simple Program Properties
Program
P
:
var natural
x
,
y
= 0
do
<
true
->
x
:=
x+1
>
[]
<
true
->
y
:=
y+1
>
od
TLA Formula
Phi
:
Init
Phi
<=>
(x=0)
and
(y=0)
A
1
<=>
(x' = x+1)
and
(y' = y)
A
2
<=>
(y' = y+1)
and
(x' = x)
A
<=>
A
1
or
A
2
Phi
<=>
Init
Phi
and
always
[
A
]
<x, y>
and
WF
<x, y>
(
A
1
)
and
WF
<x, y>
(
A
2
)
Program
P
has property
F
:
Phi
=>
F
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998