CaltechTHESIS
  A Caltech Library Service

Toward reliable modular programs

Citation

Leino, K. Rustan M. (1995) Toward reliable modular programs. Dissertation (Ph.D.), California Institute of Technology. http://resolver.caltech.edu/CaltechETD:etd-10162007-111256

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:Thesis (Dissertation (Ph.D.))
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Restricted to Caltech community only
Research Advisor(s):
  • Van de Snepscheut, Jan L. A. (advisor)
  • Chandy, K. Mani (advisor)
  • Nelson, Greg (advisor)
Thesis Committee:
  • Van de Snepscheut, Jan L. A. (chair)
  • Martin, Alain J.
  • Sanders, Beverly
  • Nelson, Greg
  • Chandy, K. Mani
  • Wilson, Richard M.
Defense Date:5 January 1995
Record Number:CaltechETD:etd-10162007-111256
Persistent URL:http://resolver.caltech.edu/CaltechETD:etd-10162007-111256
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:4114
Collection:CaltechTHESIS
Deposited By: Imported from ETD-db
Deposited On:26 Oct 2007
Last Modified:26 Dec 2012 03:05

Thesis Files

[img] PDF (Leino_krm_1995.pdf) - Final Version
Restricted to Caltech community only
See Usage Policy.

6Mb

Repository Staff Only: item control page