[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Can PVS keep and change state variables



Title: Can PVS keep and change state variables
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