Go backward to
Formal Specification (Contd)
Go up to
Top
Go forward to
Quantification over Flexible Variables
Quantification over Flexible Variables
exists
x
:
F
Flexible variable
x
.
There exists values for
x
such that
F
holds.
Auxiliary definitions:
s
=
x
t
: states
s
and
t
assign same values to all variables other than
x
.
s
=
x
t
<=>
forall
'
v
'
notequal
'
x
'
s
[[
v
]] =
t
[[
v
]]
<
s
0
,
s
1
, ...> =
x
<
t
0
,
t
1
, ...>
<=>
forall
n
in
Nat
:
s
n
=
x
t
n
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998