Postscript and PDF files

Chapter Title

Contents


Preliminary Pages

Title page, Signature page, Dedication, Table of Contents, List of Figures, List of Tables, Acknowledgments, Vita, Publications,
Abstract


Part I:

Background


Chapter 1:
Introduction

Introduces and motivates the need for program correctness, and introduces the concept of verification condition generators.


Chapter 2:
Underlying Technologies

Describes the foundational technologies that underlie this work, such as structural operational semantics and Floyd/Hoare
rules.


Chapter 3:
Survey of Previous Research

A survey of previous research on verification condition generators, and in particular, methods to prove the total correctness
of procedures.


Chapter 4:
Organization of Dissertation

Gives the overall organization of the dissertation, and description of each chapter.


Part II:

Results


Chapter 5:
Sunrise

Defines the syntax and semantics of the Sunrise programming language and assertion language.


Chapter 6:
Program Logics

Presents the five program logics, with their fourteen correctness specifications, that can be used to prove Sunrise programs
totally correct.


Chapter 7:
Verification Condition Generator

The heart of this work. Defines a verification condition generator for the Sunrise system, and also presents theorems that
verify it.


Chapter 8:
Example Runs

Takes this VCG and applies it to several examples, with transcripts.


Chapter 9:
Source Code

Describes the source code of the Sunrise system and where it may be found.


Part III:

Tour of Interesting Aspects


Chapter 10:
Partial Correctness

Describes various aspects of the system relating to partial correctness, including variants, substitution, translation, wellformedness,
and semantic stages.


Chapter 11:
Total Correctness

Describes the proof of termination of mutually recursive procedures and programs.


Part IV:

Conclusions


Chapter 12:
Significance

Our sense of this work's significance.


Chapter 13:
Ease of Use

Examines the question of ease of use for Sunrise.


Chapter 14:
Future Research

Gives an outline of our plans for future research in this area.


Chapter 15:
Conclusions and References

Presents our conclusions.
Includes the list of references.
