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

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

On Wed, 2009-04-15 at 11:31 +0800, SongFu wrote:
> 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

"x=inc(x)" isn't even type-correct, is it?

However, introducing an explicit state function (i.e., a mapping from
variables to values) like above is indeed a common solution to model
state.

http://en.wikipedia.org/wiki/Monads_in_functional_programming might be
worth reading.

Regards,
Tjark