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