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

Motty, Stephen D. (2014) Using Scala for computer-assisted stepwise refinement of software (from specification to implementation). Masters thesis, Memorial University of Newfoundland.

[img] [English] PDF - Updated Version
Available under License - The author retains copyright ownership and moral rights in this thesis. Neither the thesis nor substantial extracts from it may be printed or otherwise reproduced without the author's permission.

Download (16MB)
[img] [English] PDF - Accepted Version
Available under License - The author retains copyright ownership and moral rights in this thesis. Neither the thesis nor substantial extracts from it may be printed or otherwise reproduced without the author's permission.

Download (17MB)

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.

Item Type: Thesis (Masters)
URI: http://research.library.mun.ca/id/eprint/8300
Item ID: 8300
Additional Information: Includes bibliographical references (pages 139-141).
Department(s): Engineering and Applied Science, Faculty of
Date: October 2014
Date Type: Submission
Library of Congress Subject Heading: Computer software--Development; Programming languages (Electronic computers)--Syntax; Parsing (Computer grammar); Scala (Computer program language); Logic programming

Actions (login required)

View Item View Item

Downloads

Downloads per month over the past year

View more statistics