[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] about PVS ASSUMPTIONS
i am writing a theory about which takes no formal parameters.i have declared
flp: var bvec
fsopa: var bvec
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.
Want to meet David Beckham? http://www.msn.co.in/gillette/ Fly to Madrid