Proofs for specifications

Abstract

The approach throughout the preceding chapters has been overwhelmingly semantic and model-theoretic. What is missing are formal proofs, whereby syntax of specifications, sentences and programs are directly manipulated, without reference to models. Such proofs are of obvious central importance in actually using specifications in software engineering. Proofs are required at different levels: among other things, we need to be able to prove that a sentence follows from a set of axioms, or more generally from a structured specification, and that one structured specification is a correct implementation of another. In addition, in order to take the developments of Chapter 8 into account, at each of these levels we need to consider both a “literal” version and a behavioural version of the proof concepts and techniques. In line with our institution-based treatment, we show how a basic proof system for a given institution “lifts” to proof systems at the other levels. In each case our starting point is a corresponding model-theoretic relation that has been introduced in earlier chapters, which serves as a standard that we aim to soundly approximate by proof-theoretic means.