IEEE Transactions on Software Engineering

The ideas behind correctness proofs for programs are outlined, and conventional definitions of assignment, etc., are given. The main part of this paper is the idealized development of a nontrivial program in a disciplined fashion. The use of Dijkstra's "...

We will consider the inductive mechanisms in five techniques for verifying iterative/recursive program structures: inductive assertion, predicate transformers, subgoal induction, computation induction, and structural induction. We will discover that all ...

The programming language Alphard is designed to provide support for both the methodologies of "well-structured" programming and the techniques of formal program verification. Language constructs allow a programmer to isolate an abstraction, specifying ...

Software development has emerged as a critical bottleneck in the human use of automatic data processing. Beginning with ad hoc heuristic methods of design and implementation of software systems, problems of software maintenance and changes have become ...

This paper discusses the requirements of programmers working in varying environments in relation to software engineering, structured programming, and program verification.

Controlled sharing of information is needed for many applications. Access-control mechanisms exist in operating systems to provide such controlled sharing. However, programming languages currently do not support such a facility. This paper illustrates ...

Backtracking is a well-known technique for solving combinatorial problems. It is of interest to programming methodologists because 1) correctness of backtracking programs may be difficult to ascertain experimentally and 2) efficiency is often of ...

Software validation through testing will continue to be a very important tool for ensuring correctness of large scale software systems. Automation of testing tools can greatly enhance their power and reduce testing cost. In this paper, techniques for ...

The authors are engaged in a project to produce a precise description of a design for a family of operating systems. The design decisions ue being expressed by means of formal module specifications. In an attempt to write a concise specification of one ...

This paper describes a graph-theoretic complexity measure and illustrates how it can be used to manage and control program complexity. The paper first explains how the graph-theory concepts apply and gives an intuitive explanation of the graph concepts ...

Rochester's Intelligent Gateway (RIG) system provides convenient access to a wide range of computing facilities. The system includes five large minicomputers in a very fast internal network, disk and tape storage, a printer/plotter and a number of ...