2,199 papers · page 104 of 110
A logic for a relational data manipulation language is defined by augmenting a known logic of programs with rules for two new statements: the relational assignment, which assign a relational expression to a relation, and the random tuple selection, which extracts an arbitrary tup…
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 reso…
Many well-known functions are computed by interpretations of the recursion schemaprocedure f(x) ;if p(x)then return a(x)else return b(x,f(c1(x)),…,f(cn(x)))Some of these interpretations define redundant computations because they lead to multiple calls on f with identical argument…
Attribute grammars are an extension of context-free grammars devised by Knuth as a formalism for specifying the semantics of a context-free language along with the syntax of the language. The syntactic phase of the translation process has been extensively studied and many techniq…
PL/CV is a new formal system which mixes commands and assertions. It includes axioms and rules for a theory of programming over integers and characters. Since arguments in the theory can be checked by the PL/CV Proof Checker, the system offers an approach to mechanical program ve…
Semantic analysis of programs is essential in optimizing compilers and program verification systems. It encompasses data flow analysis, data type determination, generation of approximate invariant assertions, etc.
Article Free Access Share on The functional power of parameter passage mechanism Author: Adrienne Critcher Baylor University, Waco, Texas Baylor University, Waco, TexasView Profile Authors Info & Claims POPL '79: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles o…
In this paper we study the profitability of applying the "reduction in strength" technique to programs in set-theoretic languages, focusing on the high level constructs involving set-formers. We define recursively two classes of expressions we shall call inductively computable se…
Object code optimizers pay dividends but are usually ad hoc and machine-dependent. They would be easier to understand if, instead of performing many ad hoc optimizations, they performed a few general optimizations that give the same effect. They would be easier to implement if th…
Concurrency in Gypsy is based on a unique, formal approach to specifying and proving systems of concurrent processes. The specification and proof methods are designed so that proofs of individual processes are totally independent, even when operating concurrently. These methods c…
Hoare and Lauer [1974] have advocated using a variety of styles of programming language definitions to fit the variety of users from implementers to program verifiers. They consider the question of whether different definitions and specifications determine the same language by sh…
The meaning of "type" in an APL extended to contain nested arrays is discussed. It is shown that "type" is closely related to the variety of empty arrays of the same shape and to the possible fill values needed in the "expand" and "take" functions. Choices for fill functions are …
The problem of reasoning about recursive programs is considered. Utilizing a simple analogy between iterative and recursive programs viewed as unfinite unions of finite terms, we carry out an investigation analogous to that carried out recently for iterative programs. The main re…
Equations provide a rich, intuitively understandable notation for describing nonprocedural computing languages such as LISP and Lucid. In this paper, we present techniques for automatically generating interpreters from equations, analagous to well-known techniques for generating …
In [12] the authors introduced the concept of binding time optimization and presented a series of data flow analytic methods for determining some of the binding time characteristics of programs. In this paper we extend that work by providing methods for determining the class of s…
How can one organize the understanding of complex algorithms? People have been thinking about this issue at least since Euclid first tried to explain his innovative greatest common divisor algorithm to his colleagues, but for current research into verifying state-of-the-art progr…
There is a wide range of applications for string processing and SNOBOL4 (Griswold, et al. [1971]) has come to be the most widely implemented and accepted language for such applications. No doubt one of the principle reasons for this acceptance is the data structure around which t…
We present an algorithn for the determination of run-time types which functions in the presence of errors, and show that it provides more information than that obtained using a previously published algorithm.In Section 1 we define the problem and state the requirements for a prac…
We discuss problems arising in reasoning about on-going processes, using the modal constructs after, throughout, during, and preserves. Earlier work established decidability of the theory whose language included only the first two of these, along with program connectives | , ; an…
Data flow analysis is a technique essential to the compile-time optimization of computer programs, wherein facts relevant to program optimizations are discovered by the global propagation of facts obvious locally.This paper extends flow analysis techniques developed for sequentia…