[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] about PVS ASSUMPTIONS
hi,
i am writing a theory about which takes no formal parameters.i have declared
three variables
flp: var bvec[54]
fsopa: var bvec[118]
seff: var bit.
my lemmas will work only under the assumption that
flp(53) = TRUE or flp(52) = TRUE
fsopa(117) = seff
fsopa(116) = seff
if i do not have any formal parameters, PVS complains that i do not need an
ASSUMING block.whatever the case might be i need to set those bits to those
values to use it later on.how can I do that.is there a different way of
stating these assumptions.
rgds
-NDK
---
http://engr.smu.edu/~nikhil
_________________________________________________________________
Want to meet David Beckham? http://www.msn.co.in/gillette/ Fly to Madrid
with Gillette!