1,205 papers · page 59 of 61
A formal system for proving properties of programs accessing a database is introduced. Proving that a program preserves consistency of the database is one of the possible applications of the system. The formal system is a variant of dynamic logic and incorporates a data definitio…
Work with compiler compilers has dealt principally with automatic generation of parsers and lexical analyzers. Until recently, little work has been done on formalizing and generating the back end of a compiler, particularly an optimizing compiler. This paper describes formalizati…
Owicki and Gries have developed a proof system for conditional critical regions . In their system, logically related variables accessed by more than one process are grouped together as resources , and processes are allowed access to a resource only in a critical region for that r…
The median split tree is an elegant technique for searching static sets of keys when the frequency of access is highly skewed. This paper generalizes the median split search technique, relates it to sequential search and binary search, discusses the choice of an optimum search st…
Peephole optimizers improve object code by replacing certain sequences of instructions with better sequences. This paper describes PO, a peephole optimizer that uses a symbolic machine description to simulate pairs of adjacent instructions, replacing them, where possible, with an…
The programming language MODULA is extended to permit the formal specification of the structure and functional capabilities of modules. This makes true hierarchical programming possible in MODULA by allowing programmers of higher level parts of a system to ignore completely the i…
The problem of parsing and compiling arithmetic expressions on vector computers is considered. Methods are developed which allow encodings of one or more arithmetic expressions to be transformed directly into encodings of their corresponding derivation trees. The algorithm which …
Discussed is a distributed system based on communication among disjoint processes, where each process is capable of achieving a post-condition of its local space in such a way that the conjunction of local post-conditions implies a global post-condition of the whole system. The s…
A new algorithm for recognizing and parsing arbitrary context-free languages is presented, and several new results are given on the computational complexity of these problems. The new algorithm is of both practical and theoretical interest. It is conceptually simple and allows a …
The multiple assignment statement is defined in full generality—including assignment to subscripted variables and record fields—using the “axiomatic” approach of Hoare. Proof rules are developed for calls of procedures using global variables, var parameters, result parameters, an…
SNOBOL4 is best known for its string processing facilities, which are based on patterns as data objects. Despite the demonstrated success of patterns, there are many shortcomings associated with their use. The concept of patterns in SNOBOL4 is examined and problem areas are discu…
A simple tree-like programming/specification language is presented. The central idea is the dividing of conventional programming constructs into the two classes of and and or subgoaling, the subgoal tree itself constituting the program. Programs written in the language can, in ge…
Error analysis involves the examination of a collection of programs whose errors are known. Each error is analyzed and validation techniques which would discover the error are identified. The errors that were present in version five of a package of Fortran scientific subroutines …
Although the use of abstract types has been widely advocated as a specification and implementation technique, their use has often been associated with programming languages that are not widely available, and examples published to date are rarely taken from actual applications. SI…
The assembled length of a span-dependent jump instruction depends on the distance between the instruction and its target. Such instructions are found on many computers and typically have two forms, long and short. We consider the problem of minimizing object program length for su…
A method of documenting exception propagation and handling in Ada programs is proposed. Exception propagation declarations are introduced as a new component of Ada specifications, permitting documentation of those exceptions that can be propagated by a subprogram. Exception handl…
Methods are described to translate a certain machine-independent intermediate language (IML) to efficient microprograms for a class of horizontal microprogrammable machines. The IML is compiled directly from a high-level microprogramming language used to implement a virtual instr…
Program synthesis is the systematic derivation of a program from a given specification. A deductive approach to program synthesis is presented for the construction of recursive programs. This approach regards program synthesis as a theorem-proving task and relies on a theorem-pro…
The construction of sequential testing procedures from functions of discrete arguments is a common problem in switching theory, software engineering, pattern recognition, and management. The concept of the activity of an argument is introduced, and a theorem is proved which relat…
An algorithm for prettyprinting is given. For an input stream of length n and an output device with linewidth m , the algorithm requires time O ( n ) and space O ( m ). The algorithm is described in terms of two parallel processes: the first scans the input stream to determine th…