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

[PVS-Help] Finding Variables



Hello,

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>
        step1
        step2)

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.

Thank you,

    Erika Rice
    University of Washington