Automated Generation of Strictly Conforming Tests Based on Formal Specification of Dynamic Semantics of the Programming Language

A technique for an automated test generation for compilers, which is based on formal specifications of the programming language, is suggested. The technique makes it possible to generate tests correct from the dynamic semantics standpoint that do not depend on specific features (undefined or implementation-specific) of the semantics (the so-called strictly conforming tests). The application of the suggested technique to generating tests for C compilers is discussed in detail. For this purpose, a subset of C is defined the semantics of which, first, does not depend on the above-mentioned specific features and, second, possesses properties of type soundness and determinism, which guarantee the correct test execution for any implementation satisfying the C standard.