| Abstract: | The theory of relative program correctness and its preservation allows for elaborate and practically adequate definitions of correct implementation notions as they are established by transformations implemented in a compiler. It generalizes Hoare's and Floyd's partial and total program correctness and correctness preservation by classifying finite and infinite errors to be either acceptable (unavoidable) or unacceptable (chaotic, to be avoided). We will define correct implementation by particular compositional diagram commutativities, and we will further extend this theory also to express correctness of compiling specifications and of compiler programs and their implementations in the same uniform relational setting. Unacceptable error outcomes can semantically model pre-conditions such as well-formedness conditions for compilers or optimization pre-conditions for user programs. Our theory allows to distinguish between different correct implementation requirements, for instance (horizontally) for user programs or (vertically) for the compiler implementation, just as if we would switch on and off compiler options and tune one compiler to appropriately preserve correctness in different application domains. |
