2,199 papers · page 102 of 110
David J. Kuck, Robert H. Kuhn, David A. Padua, Bruce Leasure, Michael Wolfe
Dependence graphs can be used as a vehicle for formulating and implementing compiler optimizations. This paper defines such graphs and discusses two kinds of transformations. The first are simple rewriting transformations that remove dependence arcs. The second are abstraction tr…
Daniel Lehmann, Michael O. Rabin
It is shown that distributed systems of probabilistic processors are essentially more powerful than distributed systems of deterministic processors, i.e., there are certain useful behaviors that can be realized only by the former. This is demonstrated on the dining philosophers p…
P. Geoffrey Lowney
The idiomatic APL programming style is limited by the constraints of a rectangular, homogeneous array as a data structure. Non-scalar data is difficult to represent and manipulate, and the non-scalar APL functions have no uniform extension to higher rank arrays. The carrier array…
Eugene W. Myers
Data flow analysis is well understood at the intra-procedural level and efficient algorithms are available. When inter-procedural mechanisms such as recursion, procedure nesting, and pass-by-reference aliasing are introduced, the data flow problems become much more difficult. The…
Susan S. Owicki
This paper describes the formal specifications of garbage collection in the programming language Cedar Mesa. They were developed as part of the process of identifying a safe subset of Mesa for which garbage collection was possible. The purpose of the specifications was to provide…
Wolfgang Polak
A theory of partial correctness proofs is formulated in Scott's logic computable junctions. This theory allows mechanical construction of verification condition solely on the basis of a denotational language definition. Extensionally these conditions, the resulting proofs, and th…
Vaughan R. Pratt
When the "binding mechanisms" of assignment, quantification, and procedure definition are removed from a conventional first order total correctness logic of programs, the remaining logical system is decidable in time approximately one exponential in the length of the input. This …
Jay Ramanathan, Charley J. Shubra
Article Free Access Share on Modeling of problem domains for driving program development systems Authors: J. Ramanathan The Ohio State University, Columbus, Ohio The Ohio State University, Columbus, OhioView Profile , C. J. Shubra The Ohio State University, Columbus, Ohio The Ohi…
Barry K. Rosen
In analysis of programs and many other kinds of computation, algorithms are commonly written to have an input P and an output Q, where both P and Q are large and complicated objects. For example, P might be a routing problem and Q might be a solution to P. Although documented and…
William L. Scherlis
We investigate the specialization of programs by means of program transformation techniques. There are two goals of this investigation: the construction of program synthesis tools, and a better understanding of the development of algorithms.By extending an ordinary language of re…
Norihisa Suzuki
Smalltalk is an object-oriented language designed and implemented by the Learning Research (Group of the Xerox Palo Alto Research Center [2, 5, 14]. Some features of this language are: abstract data classes, information inheritance by a superclass-subclass mechanism, message pass…
Timothy A. Budd, Richard A. DeMillo, Richard J. Lipton, Frederick G. Sayward
In testing for program correctness, the standard approaches [11,13,21,22,23,24,34] have centered on finding data D, a finite subset of all possible inputs to program P, such that
Alan J. Demers, James E. Donahue
In statically typed programming languages, each variable and expression in a program is assigned a unique "type" and the program is checked to ensure that the arguments in each application are "type-compatible" with the corresponding parameters. The rules by which this "type-chec…
Alan J. Demers, James E. Donahue
In his recent Turing Lecture, John Backus delivered a trenchant argument for the proposition that "programming languages are in trouble." Backus claims this to be inevitable: the development of Algol-like languages must lead to this sorry state because it begins from faulty assum…
Daniel P. Friedman, David S. Wise
This paper proposes the encapsulization and control of contending parallel processes within data structures. The advantage of embedding the contention within data is that the contention, itself, thereby becomes an object which can be handled by the program at a level above the ac…
Dov M. Gabbay, Amir Pnueli, Saharon Shelah, Jonathan Stavi
The use of the temporal logic formalism for program reasoning is reviewed. Several aspects of responsiveness and fairness are analyzed, leading to the need for an additional temporal operator: the 'until' operator -U. Some general questions involving the 'until' operator are then…
John V. Guttag, James J. Horning
The formulation and analysis of a design specification is almost always of more utility than the verification of the consistency of a program with its specification. Good specification tools can assist in this process, but have generally not been proposed and evaluated in this li…
L. Howard Holley, Barry K. Rosen
It is known that not all paths are possible in the run time control flow of many programs. It is also known that data flow analysis cannot restrict attention to exactly those paths that are possible. It is therefore usual for analytic methods to consider all paths. Sharper inform…
Harry B. Hunt III, Daniel J. Rosenkrantz
Efficient algorithms are presented for several grammar problems relevant to compiler construction. These problems include(i) testing, for a reduced context-free grammar G and an LL(k), uniquely invertible, or BRC(m,n) grammar H, if G is structurally contained by H, and(ii) testin…
Samuel N. Kamin
A new specification method for data types is presented, which is distinguished by the semantic objects it specifies. In particular, only final data types [GGM,W] are specifiable. A final data type is one in which no two elements are "input-output equivalent". It is argued that th…