[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!