CaltechAUTHORS
  A Caltech Library Service

Towards Reliable Modular Programs

Leino, K. Rustan M. (1995) Towards Reliable Modular Programs. California Institute of Technology . (Unpublished) http://resolver.caltech.edu/CaltechCSTR:1995.cs-tr-95-03

[img]
Preview
Postscript
See Usage Policy.

928Kb
[img]
Preview
Other (Adobe PDF (1.2MB))
See Usage Policy.

1155Kb

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCSTR:1995.cs-tr-95-03

Abstract

Software is being applied in an ever-increasing number of areas. Computer programs and systems are becoming more complex and consisting of more delicately interconnected components. Errors surfacing in programs are still a conspicuous and costly problem. It's about time we employ some techniques that guide us toward higher reliability of practical programs. The goal of this thesis is just that. This thesis presents a theory for verifying programs based on Dijkstra's weakest-precondition calculus. A variety of program paradigms used in practice, such as exceptions, procedures, object orientation, and modularity, are dealt with. The thesis sheds new light on the theory behind programs with exceptions. It develops an elegant algebra, and shows it to be the foundation on which the semantics of exceptions rests. It develops a trace semantics for programs with exceptions, from which the weakest-precondition semantics is derived. It also proves a theorem on programming methodology relating to exceptions, and applies this theorem in the novel derivation of a simple program. The thesis presents a simple model for object-oriented data types, in which concerns have been separated, resulting in the simplicity of the model. To deal with large programs, this thesis takes a practical look at modularity and abstraction. It reveals a problem that arises in writing specifications for modular programs where previous techniques fail. The thesis introduces a new specification construct that solves that problem, and gives a formal proof of soundness for modular verification using that construct. The model is a generalization of Hoare's classical data refinement. However, there are more problems to be solved. The thesis reports on some of these problems and suggests some future directions toward more reliable modular programs.


Item Type:Report or Paper (Technical Report)
Group:Computer Science Technical Reports
Record Number:CaltechCSTR:1995.cs-tr-95-03
Persistent URL:http://resolver.caltech.edu/CaltechCSTR:1995.cs-tr-95-03
Usage Policy:You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.
ID Code:26878
Collection:CaltechCSTR
Deposited By: Imported from CaltechCSTR
Deposited On:14 May 2001
Last Modified:26 Dec 2012 14:08

Repository Staff Only: item control page