Using Scala for computer-assisted stepwise refinement of software (from specification to implementation)

Abstract

It is possible to generate compilable source code directly from logical formulas that describe the intended behaviour of software. Theories in support of this goal, including theories of predicative programming and programming by specification, were developed and well-understood by the mid-1990's. In practice these techniques result in code and specification libraries that are maintainable, sharable and unmistakably fit for their purpose. At present, the techniques have not met with widespread adoption. An underlying premise of this thesis is that adoption requires a proficient use of techniques outside the normal curriculum followed by many computer programmers. A Structured Imperative Modular Programming/proof-Language and Environment, nicknamed SIMPpLE, is proposed to pull these techniques together into a single framework. The specific objective of the thesis is to describe how the typed trees representing a SIMPpLE document are converted to queries to third-party provers. Using the queries, these provers verify the logical correctness of the SIMPpLE program as it is constructed line by line, a process known as stepwise refinement. Two classes of provers are considered: first, Satisfiability Modulo Theorem (SMT) provers; and secondly high-order Theorem Proving Systems (TPS). The thesis concludes that stepwise refinement of software is practiceable, and that the implementation is readily achievable with today's technology. Examples of programs created using the techniques are provided.