Re: ensuring full semantic checker coverage?

Ross Bencina said:


> My current plan is to build a database (some sort of tagged
> textfile) with separate items for each assertion that the checker
> must test, give each of these assertions an ID, then embed these IDs
> in comments with the source code that implements each check. That
> way I can write a script that crossreferences every required check
> to the code that performs it. Perhaps the error message text for
> each check might also form part of this approach.


That would formally guarantee that you've written the code to do the
required checks, but unless I'm mistaken, it would then require flow
analysis of the code that reaches the code that contains the checks to
determine that those checks are actually executed, which, of course,
would leave you with something that is undecidably correct.


I assume that not all of the checks apply to all of the code under
consideration for verification, and that the semantic checks occur in
grouped clusters. (For instance, code block A would have a proscribed
set of semantic checks, code B another, possibly different set, and so
on.) Thus, the checks that are required to be applied to any block of
source would depend on the source itself.


My suggestion would be to annotate the tree with a set of semantic
checking attributes, where each node would be decorated such that its
decorations would indicate which checks are required on that node.
Then, after decoration, semantic checking visitors would traverse the
tree, flagging as completed those checks that pass muster. A final
visitation on each node to verify that all semantic decorations have
been processed and accepted would then tell you with some certainty
that all proscribed semantic checks had been applied. This method
would scale to more checks in future, and would keep the semantic
checking code in its own sandbox, apart from lexing, parsing,
optimizing, and other code.


My 2 cents Canadian.


--
Quinn Tyler Jackson

Return to the comp.compilers page.
Search the comp.compilers archives again.