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.

This is a reference manual for FAIL, a fast, one-pass assembler for

PDP-10 and PDP-6 machine language. FAIL statements,

pseudo-operations, macros, and conditional assembly features are

described. Although FAIL uses substantially more main memory than

MACRO-10, it assembles typical programs about five times faster.

FAIL assembles the entire Stanford time-sharing operating system (two

million characters) in less than four minutes of CPU time on a KA-10

processor. FAIL permits an ALGOL-style block structure which

provides a way of localizing the usage of some symbols to certain

parts of the program, such that the same symbol name can be used to

mean different things in different blocks.

Man-machine dialogues using everyday conversational English present

difficult problems for computer processing of natural language.

Grammar-based parsers which perform a word-by-word, parts-of-speech

analysis are too fragile to operate satisfactorily in real time

interviews allowing unrestricted English. In constructing a

simulation of paranoid thought processes, we designed an algorithm

capable of handling the linguistic expressions used by interviewers

in teletyped diagnostic psychiatric interviews. The algorithm uses

pattern-matching rules which attempt to characterize the input

expressions by progressively transforming them into patterns which

match, completely or fuzzily, abstract stored patterns. The power of

this approach lies in its ability to ignore recognized and

unrecognized words and still grasp the meaning of the message. The

methods utilized are general and could serve any "host" system which

takes natural language input.