Contribution to Goodenough's and Gerhart's theory of software testing and verification: Relation between strong compiler test and compiler implementation verification

Abstract

In view of J. B. Goodenough's and S. L. Gerhart's theory compiler πtS shows up to be a very well selected test datum to do translator implementation verification for πT supported by testing.

A posteriori verification of generated machine code as demanded by BSI in each program case relevant for safety critical applications should and can be made redundant. It suffices to do such a posteriori verification for initial compilers only.

For translator implementation verification we have used and refunctioned a real life system, host processor H0M plus S0 → H0-translator π _tH0 , as a proof assistant. We print and iuxtapose intermediate translators which represent formal proof trees understandable by usual programmers. No special formal logics are necessary as existing theorem provers require.

We create complete enough and readable proof documentations not only for translation verification but also for translator implementation verification. Our technique allows to put the finger on the wound of any compiler failure in translation specification as well as in translator implementation. Even for full compiler correctness only a reduced set of low level code must be double checked. Our proceeding is in accordance with A. Robinson's [Rob96] statements on formal and informal proof: Informatics should try to mechanise proof techniques of mathematicians. Their informal proofs are guided by good ideas. That is more effectful than pursuing swollen formal proof protocols in predicate logics.