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