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

[PVS-Help] help for prooving axioms








sir
 
  i have converted an ada program to typed transition form of PVS.  I am ataching the screen shot of a  sample program along with this mail and a part of TCCs generated. Inorder to discharge TCCs i gave inital values to the variables (s1 : state = (True, 0, 1.2....))
and used "grind" command.  I need an alternate method by specifying axioms in the pvs program for eg.  axiom _1:AXIOM (s1`3>=-10) AND (s1`3<=10)
 
  As i dont want to give inital values for variables i need an alternate proving command for discharging TCC based on this axiom.  Expecting ur help to overcome this problem
 
 
Sujith CS
 
 
 


Now, send attachments up to 25MB with Yahoo! India Mail. Learn how.


Add whatever you love to the Yahoo! India homepage. Try now!


Add whatever you love to the Yahoo! India homepage. Try now!

rcmdnull.JPG

rcmdnulltcc3.JPG