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

Adding Invariants



Hello,

I would like to add some invariants to my PVS specs and have them hold
during the proof process.  I am not sure how to do this.  I have made
them axioms, but am not sure how to get them used during the proof.
The invariants are of the form A IFF B, and X Implies Y, etc.

Thanks,

Barb
czerny@cps.msu.edu