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

Re: [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?

Depending on what you actually want to do, SAL and its infinite
bounded model checker may be more suitable than PVS.

SAL is oriented to specification of state machines (so state is built
in) and provides more automation for certain kinds of problems; PVS is
more general, but less automated.