Re: [PVS-Help] about PVS ASSUMPTIONS

["Cesar A. Munoz" <munoz@nianet.org>]

Hi,

You do have a parameter (seff), but you don't need a clause ASSUMING: 

test[seff:bit] : THEORY
BEGIN

  BV54  : TYPE = bvec[54]
  BV118 : TYPE = bvec[118]

  flp:   var {flp:BV54 | flp(53)=TRUE OR flp(52)=TRUE}
  fsopa: var {fsopa:BV118 | fsopa(117) = seff AND fsopa(117) = seff}


END test,

Cesar

On Thu, 2005-03-17 at 17:05, 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!
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
144 Research Drive                  http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855