What Level
of Mathematical Reasoning can Computer Science Demand of a Software Implementer
Christian-Albrechts-Universität zu Kiel, Germany
This talk starts out from the observation that software engineering splits in two large activity areas: software specification with its verification and software implementation with its verification. To find answers to the question in the title the talk studies a practical systems software engineering area where theory is better developed as compared to other areas: Compiler construction.
Our answer is a conclusion from work in the DFG-project Verifix, U.Karlsruhe, U.Kiel, U.Ulm, 1995-2003. One very complex cooperational task has been construction of a so called initial correct compiler for a realistic high level programming (and compiler writing) language correctly implemented and executed on a real life host processor. The interface between compiling specification and compiler implementation is given by algebraic-style, conditional formula transformation or program term rewriting rules which the specifier figures out and must prove correct w. r. t. source program and target processor semantics and data and states representations.
Intensive cooperation of compiling specifyers and compiler
implementers has revealed that the implementer's mathematical
reasoning is algebraic reasoning of moderate depth. The specifier
overtakes semantical issues and does induction proofs, a field of much
more intricate mathematical reasoning.