|Page 227 of 800||Search internet|
A page is verified thus:
The claim aspect of the base page reads:
Thus, if a page P does not define a claim of its own and if page P references the base page as its first reference, then page P will be verified by evaluating where c is the cache of page P.
We shall refer to test1 as the verifier for page P. The value definition of test1 on the base page reads:
so the verifier invokes .
By reading value definitions on the base page (either in the body or in the extract) allows to follow what the verifier does: It first looks up the expansion of the page (i.e. the macro expanded version of the body). The expansion is a parse tree. Then the verifier traverses the parse tree root to leaf, left to right. The verifier ignores strings and page symbols.
For all other constructs, the verifier looks up the claim aspect of the construct. If the claim aspect differs from then the construct is some sort of test construct. As an example, the principal operator of is a test construct because it has the following claim definition:
When the verifier finds a construct which has a claim definition, it applies the right hand side of the claim definition to where t is the test case to be verified (the one with the test construct as principal operator) and c is the cache of the page being verified.
If a construct does not have a claim aspect, the verifier sees if it has a definition aspect. If it has, the verifier does not traverse the subtrees of the construct. In this way, the verifier avoids traversing inside definitions. Test cases that appear in definitions typically either occur in the left hand side of a claim definition or in the right hand side of a macro definition, and such occurrences are not meant as test cases.
Test constructs are supposed to return if the test succeeds and a parse tree if the test fails. If all tests succeeds, the verifier returns . If some test fails, the verifiers stops traversing the expansion and returns the parse tree returned by the failing test.
When the verifier returns a parse tree, lgc(1) hangs the parse tree on the diagnose hook and then renders the parse tree and presents it to the user as the diagnose of the page.
|Page 227 of 800||Search logiweb.eu|