Go backward to
The Raw Logic
Go up to
Top
Go forward to
Describing Programs with RTLA
Describing Programs with RTLA
Program in guarded command language.
var natural
x
,
y
= 0
do
<
true
->
x
:=
x+1
>
[]
<
true
->
y
:=
y+1
>
od
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
sigma
[[
Phi
]] =
true
iff
sigma
represents possible execution of program.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998