Toggle Main Menu Toggle Search

ePrints

On the Search for Tractable Ways of Reasoning about Programs

Lookup NU author(s): Professor Cliff Jones

Downloads


Abstract

This paper traces the important steps in the history --up to around 1990--of research on reasoning about programs. The main focus is on sequential imperative programs but some comments are made on concurrency. Initially, researchers focussed on ways of verifying that a program satisfies its specification (or that two programs were equivalent). Over time it became clear that {\em post facto} verification is only practical for small programs and attention turned to verification methods which support the development of programs; for larger programs it is necessary to exploit a notation of compositionality. Coping with concurrent algorithms is much more challenging -- this and other extensions are considered briefly. The main thesis of this paper is that the idea of reasoning about programs has been around since they were first written; the search has been to find tractable methods.


Publication metadata

Author(s): Jones CB

Publication type: Report

Publication status: Published

Series Title: Department of Computing Science Technical Report Series

Year: 2001

Pages: 49

Print publication date: 01/07/2001

Source Publication Date: July 2001

Report Number: 740

Institution: Department of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/740.pdf


Share