[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Finding Variables
I am writing a strategy and have found myself in the
following situation. I have a store type and the guarantee
that variables of type store will always be quantified at
this point, and I want to do something like this
(if <formula mentions variable with of type store>
The challenge is the bit in angle brackets. Is there a way
of determining whether or not a formula makes any mention
of a variable of a certain type?
If that is too vague of a question, please give me
information about any of the following: comparing variable
types, peeling apart the structure of a formula, finding the
types of all quantified variables, or anything else that
seems vaguely related.
University of Washington