[Next] [Up] [Previous] [Contents]
Next: Refinements Up: Assertions Previous: The assert declaration

Using...Prove declarations

A using...prove declaration tells the verification system to use one assertion as an assumption when verifying another. A declaration of the form

	using foo prove bar;
where foo and bar are identifiers for assertions, tells the verification system to use assertion foo as an assumption when proving assertion bar. A list of assumptions may also be used:
	using a1,a2,...,an prove bar;
Such a ``proof'' may not contain circular chains of reasoning. Thus, for example,
	using foo prove bar;
        using bar prove foo;
is illegal.



Ken McMillan
Sat Jun 6 21:41:59 PDT 1998