7.11.4 Formal proofs

Prev Up Next Page 229 of 800 Search internet

The claim definition of the check page reads:

verifier test1 &c proofcheck end verifier

That statement macro expands into a claim definition of the page construct of the check page.

The x &c y construct is defined on the base page:

define value of x &c y as \ c . x ' c .and. y ' c end define

Hence, the verifier of the check page is a conjunction of two verifiers: the test1 verifier from the base page which verifies test cases and a new one called proofcheck which happens to check proofs.

The two verifiers are executed left to right. If test1 finds an error in a test case then proofcheck is not invoked.

A page which does not define a verifier of its own and which references the check page as first reference is verified by both test1 and proofcheck. A page with does not define a verifier of its own and which references the base page as first reference is merely verified by test1. Hence, it is entirely up to the author of a page what should be verified.

If you want to test your pages e.g. for type correctness w.r.t. some typing system you like, then write a type checker and include it in your conjunction of verifiers.

Prev Up Next Page 229 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05