How to get err status in PVS batch mode

[Min Jing <jingm@mcsergjr.cas.mcmaster.ca>]

Hello fellow PVS users,

I am trying to prove some theories in PVS batch mode. However, some theories 
should be proved or not depends on other theories' proving status. Is that 
possible to get the error status of proving explicitly? 

Following example may be helpful to understand my question.

Batch File (pseudo code)

--------------------------------------
 proving Mytheorem
 if something is wrong (e.g. unproved)  <==== Is that possible to get error status?
   then proving (not Mytheorem)
 else
   pvs-message "successful"  
--------------------------------------   

Thanks,

Min

---

• Prev by Date: SPAM on PVS mailing list
• Next by Date: Promoting Formal Methods (fwd)
• Prev by thread: SPAM on PVS mailing list
• Next by thread: Promoting Formal Methods (fwd)
• Index(es):
  • Date
  • Thread