Since production systems were first proposed in 1943 as a general

computational mechanism, the methodology has seen a great deal of

development and has been applied to a diverse collection of problems.

Despite the wide scope of goals and perspectives demonstrated by the

various systems, there appear to be many recurrent themes. This

paper is an attempt to provide an analysis and overview of those

themes, as well as a conceptual framework by which many of the

seemingly disparate efforts can be viewed, both in relation to each

other, and to other methodologies.

Accordingly, we use the term 'production system' in a broad sense,

and attempt to show how most systems which have used the term can be

fit into the framework. The comparison to other methodologies is

intended to provide a view of PS characteristics in a broader

context, with primary reference to procedurally-based techniques, but

with reference also to some of the current developments in

programming and the organization of data and knowledge bases.

This is a slightly revised version of a paper to appear in %2Machine

Representations of Knowledge%*, Dordrecht, D. Reidel Publishing

Company (1976).

The paper investigates methods for applying an on-line interactive

verification system designed to prove properties of PASCAL programs.

The methodology is intended to provide techniques for developing a

debugged and verified version starting from a program, that - is

possibly unfinished in some respects, - may not satisfy the required

specifications,i.e., may contain bugs, - may be incompletely

documented in the sense that the assertions provided by the

programmer are not sufficient for proving correctness. It deals with

programs that may be written in non-standard ways, e.g., permits user

defined data structures.

The methodology involves - techniques for describing data structures,

type constraints, and properties of programs and subprograms (i.e.

lower level procedures); - the use of (abstract) data types in

structuring programs and proofs. - interactive application of a

verification condition generator, an algebraic simplifier and a

theorem-prover;

Within each unit (i.e. segment of a problem), the interactive use is

aimed at reducing verification conditions to manageable proportions

so that the non-trivial factors may be analysed. Analysis of

verification conditions attempts to localize errors in the program

logic, to extend assertions inside the program, to spotlight

additional assumptions on program subfunctions beyond those already

specified by the programmer, and to generate appropriate lemmas and

assumptions that allow a verification to be completed. Methods for

structuring correctness proofs are discussed.

A detailed case study of a pattern matching algorithm illustrating

the various aspects of the methodology (including the role played by

the user) is given.