POPL

A new approach to global program data flow analysis which constructs a "node listing" for the control flow graph is discussed and a simple algorithm which uses a node listing to determine the live variables in a program is presented. This algorithm ...

A new algorithm for global flow analysis on reducible graphs is presented. The algorithm is shown to treat a very general class of function spaces. For a graph of e edges, the algorithm has a worst case time bound of 0(e log₂e) function operations. In ...

CS-4 is an extensible language currently being developed for the Navy. The language design was influenced strongly by ECL and Algol-68; some of the more important aspects of CS-4 are as follows: (1) CS-4 has strong type checking and a rich data ...

SETL is a set-theoretically oriented language of very high level whose repertoire of semantic objects includes finite sets, ordered n-tuples, and sets of ordered n-tuples useable as mappings. This paper sets forth techniques for the logical analysis and ...

A framework for validating surface properties of programming language constructs, composed of proof rules (akin to those of Hoare) and supporting hypotheses, is constructed using the mathematical semantics of Scott and Strachey. The following approach ...

This paper extends the predicate calculus formalization of the partial correctness properties of programs (Ki, Go) to include the preservation of correctness under program transformations. The general notion of "program transformations which preserve ...

Work on PLANNER-73 and actors has led to the development of a basis for semantics of programming languages. Its value in describing programs with side-effects, parallelism, and synchronization is discussed. Formal definitions are written and explained ...

When proving that a system of processes has a given property it is often convenient to assume that a routine is uninterruptible, i.e. that the routine cannot be interleaved with the rest of the system. Here sufficient conditions are obtained to show ...

This paper presents a semantic model for parallel systems with a scheduling mechanism that is useful for expressing and proving a wider range of properties than semantic models that do not consider scheduling.We formally describe a number of properties ...

Petri nets are used to define a path and process notation which is more general in its ability to express synchronization than previous path notations. The Petri net classes corresponding to the path notation prove to be interesting in their own right ...

It has long been known that most questions of interest about the behavior of programs are recursively undecidable. These questions include whether a program will halt, whether two programs are equivalent, whether one is an optimized form of another, and ...

It is shown that both the upper and the lower bounds on the time complexity of the circularity test for Knuth's attribute grammars are exponential functions of the size of the grammar description. This result implies the "intractability" of the ...

In this paper we derive upper bounds on the complexity of LR(k) testing both when k is considered to be a fixed integer and also when k is considered to be a parameter of the problem. In the latter case, we show that the lower bounds on the running time ...

Some social aspects of programming are illuminated through analogies with similar aspects of mathematics and natural languages. The split between pure and applied mathematics is found similarly in programming. The development of natural languages toward ...

In this paper we wish to consider the problem of proving assertions about programs that construct and alter arbitrarily complex data structures. In recent years several papers have been written on the subject of proving assertions about such programs; ...

A class of program schemas with concurrency is defined as a natural extension of the standard notion of sequential flow-chart-like schemas. The question is considered as to whether such a program schema may reach a premature termination (or "hangup") ...

This paper contains a suggestion for a calculus for constructing 'flowchartable' algorithms. The calculus is a generalization of an Algol-like calculus, and hence maintains some discipline over the algorithms constructible with it.The essence of the ...

In this paper, we define what exception conditions are, discuss the requirements exception handling language features must satisfy, survey and analyze existing approaches to exception handling, and propose some new language features for dealing with ...

This paper extends the relational algebra of data bases, presented by Codd [4] and others, in four areas. The first is the use of selector names to remove order dependencies from the columns of a relation. This use of selector names enables us to define ...

This paper describes a system being developed to bridge the gap between an application program and a user inexperienced in the ways of computers. The user explores the characteristics of the available programs by a natural language dialogue with the ...