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

Re: [PVS-Help] about PVS ASSUMPTIONS



have you tried to introduce those as axioms for your lemma?
ahmed

Nikhil D. Kikkeri wrote:

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