|
Dear Mitchell
Hirschfeld:
I think the follow can fix the
problem.
Test : Theory
Begin
Vars:
TYEP+
Value:
TYPE+
State : TYPE+=
[Vars->Value]
x: Var
Vars
s: Var
State
inc(x): [State->Value] =
LAMBDA s: s(x)+1
x=inc(x) % means
x++
End Test
Best regards
Song
----- Original Message -----
Sent: Tuesday, April 14, 2009 9:13
PM
Subject: [PVS-Help] Can PVS keep and
change state variables
I am just starting to use PVS
for a graduate thesis and am unsure of how or even if it is possible
to have state
variables. I realize the beauty of functional languages is to not have state, but it is necessary for
my research. For
example, is it possible to have a variable x that can call a function to increment it and increase its
value so that later the
variable can be checked to have been increased?
Much Thanks,
Mitchell
Hirschfeld
|