1,205 papers · page 45 of 61
Informal specifications of protocols are often imprecise and incomplete and are usually not sufficient to ensure the correctness of even very simple protocols. Consequently, formal specification methods, such as finite-state models, are increasingly being used. The selection/reso…
A specialization method for logic programs that allows one to restrict a general program to special cases by means of constraint predicates is presented. A set of basic transformation operations, which are shown to produce equivalent programs, is defined. The method uses these op…
We reformulate interval analysis so that it can he applied to any monotone data-flow problem, including the nonfast problems of flow-insensitive interprocedural analysis. We then develop an incremental interval analysis technique that can be applied to the same class of problems.…
A record data type can be extended by addition of more fields. The extended type is a subtype of the original, in that any value of the extended type can be regarded as a value of the original type by ignoring the additional fields. This results in a type hierarchy. Milner [3] ha…
Global register allocation plays a major role in determining the efficacy of an optimizing compiler. Graph coloring has been used as the central paradigm for register allocation in modern compilers. A straightforward coloring approach can suffer from several shortcomings. These s…
This paper describes research associated with the development and evaluation of Odin-an environment integration system based on the idea that tools should be integrated around a centralized store of persistent software objects. The paper describes this idea in detail and then pre…
A new approach to goal-oriented programming is described, whereby the search for values of variables to satisfy a goal is invariably directed by that goal or by information provided by its failure. This goal-directed approach is in contrast to that employed by logic programming s…
In traditional interactive programming environments, each application individually manages its interaction with the human user. The result is duplication of effort in implementing user interface code and nonuniform—hence confusing—input conventions. This paper presents an approac…
A method is presented for using symbolic execution to generate the verification conditions required for proving correctness of programs written in a tasking subset of Ada. The symbolic execution rules are derived from proof systems that allow tasks to be verified independently in…
Turner popularized a technique of Wadsworth in which a cyclic graph rewriting rule is used to implement reduction of the fixed point combinator Y . We examine the theoretical foundation of this approach. Previous work has concentrated on proving that graph methods are, in a certa…
A concurrent object is a data object shared by concurrent processes. Linearizability is a correctness condition for concurrent objects that exploits the semantics of abstract data types. It permits a high degree of concurrency, yet it permits programmers to specify and reason abo…
The notion of a program slice , originally introduced by Mark Weiser, is useful in program debugging, automatic parallelization, and program integration. A slice of a program is taken with respect to a program point p and a variable x ; the slice consists of all statements of the…
An algorithm for detecting deadlocks in distributed systems with CSP-like communication is proposed. Unlike previous work, the proposed algorithm avoids periodically sending deadlock-detecting messages by the processes and requires no local storage for the processes with size pre…
We present efficient algorithms for exhaustive and incremental evaluation of circular attributes under any conditions that guarantee finite convergence. The algorithms are derived from those for noncircular attribute grammars by partitioning the underlying attribute dependency gr…
We apply a new method for the development of parallel programs to the problem of finding maximum flows in graphs. The method facilitates concurrent program design by separating the concerns of correctness from those of hardware and implementation. It uses predicate transformer se…
A general, modular technique for designing efficient leader finding algorithms in distributed, asynchronous networks is developed. This technique reduces the problem of efficient leader finding to a simpler problem of efficient serial traversing of the corresponding network. The …
We improve on J. Kilbury's proposal to interchange “predictor” and “scanner” in Earley's parser. This modification of Earley's parser can trivially be combined with those suggested by S. Graham, M. Harrison, and W. Ruzzo, leading to smaller parse tables and almost the power of lo…
Peridot is an experimental tool that allows designers to create user interface components without conventional programming. The designer draws pictures of what the interface should look like and then uses the mouse and other input devices to demonstrate how the interface should o…
The wheel is repeatedly reinvented because it is a good idea. Perhaps Anson's "A Generalized Iterative Construct and Its Semantics" [1] confirms that “A Generalized Control Structure and Its Formal Definition” [2], and the earlier “An Alternative Control Structure and its Formal …