POPL

Hoare-like deduction systems for establishing partial correctness of programs may fail to be complete because of (a) incompleteness of the assertion language relative to the underlying interpretation or (b) inability of the assertion language to express ...

Previous work on optimal code generation has usually assumed that the underlying machine has identical registers and that all operands fit in a single register or memory location. This paper considers the more realistic problem of generating optimal ...

This paper presents a systematic approach to the problem of generating good code with a compiler that is easy to construct. A compiler structure is proposed which relies on interprocedural data flow analysis, global optimization, and an intermediate ...

Control flow relations in a high level language program can be represented by a hierarchy of small graphs that combines nesting relations among statements in an ALGOL-like syntax with relevant perturbations caused by goto or leave statements. ...

We propose a new optimization technique applicable to set-oriented languages, which we shall call general common subexpression elimination. It involves the computation of the IAVAIL(n) function for all nodes n in a flow graph, where IAVAIL(n) is the set ...

This paper explores the technique of 'strength reduction' or 'formal differentation' in a set theoretic context, as recently introduced by Earley. We give pragmatic rules for the recognition and treatment of reasonably general cases in which the ...

A standard approach to the analysis of program structure for the purpose of code optimization is to construct the "control flow graph" which models the possible execution paths through the program. Various graph algorithms can be applied to the control ...

In this paper we show that some prevailing ideas on the elimination of left recursion in a context-free grammar are not valid. An algorithm and a proof are given to show that every proper context-free grammar is covered by a non-left-recursive grammar.

An LL(1)-based error-corrector which operates by "insertion-only" is studied. The corrector is able to correct and parse any input string. It is efficient (linear in space and time requirements) and chooses least-cost insertions (as defined by the user) ...

This paper is concerned with difficult global flow problems which require the symbolic evaluation of programs. We use, as is common in global flow analysis, a model in which the expressions computed are specified, but the flow of control is indicated ...

A new interprocedural data flow analysis algorithm is presented and analyzed. The algorithm associates with each procedure in a program information about which variables may be modified, which may be used, and which are possibly preserved by a call on ...

This paper describes a system which checks correctness of array accesses automatically without any inductive assertions or human interaction. For each array access in the program a condition that the subscript is greater than or equal to the lower bound ...

A programmer spends more time modifying already existing programs than constructing original ones. An attempt is made to formulate techniques of program modification, whereby a program that achieves one result can be transformed into a new program that ...

We develop a theory for the correctness of asynchronous parallel programs. A program is considered correct if its behavior is in some sense similar to that of an abstract version of the program. We discuss various criteria for this similarity. We then ...

Brosgol [Br] formalizes the notion that parsing methods can be classified by the positions at which production rules are recognized. In an LL parser, each rule is recognized at the left end, before the rule's yield has been read; in an LR parser, a rule ...

One of the most attractive techniques in optimizing LR parsers is to eliminate reductions by semantically insignificant productions of the form A → X (single productions), where X is a nonterminal or a terminal; such a modification can lead to substantial ...

We consider the problem of automating some of the duties of programmers. We take as our point of departure the claim that data management has been automated to the point where the programmer concerned only about the correctness (as opposed to the ...

Structuring can be defined independently of what is being structured, and can be applied profitably to more than one domain. Using one mechanism to structure both values and assignments, we obtain equivalents for a variety of data and control ...

Procedure call mechanisms have mainly been studied in the framework of recursive programs without assignments, for the simplicity of their operational and denotational semantics (See Scott [16], Nivat [14], Vuillemin [17]).

According to operational ...

We use the concept of evaluation up to a given threshold of information to generalize the semantics of call by value and assignment to non-discrete domains, and to define a formal semantics for generic procedures. We then prove the correctness of ...

A program denotes computations in some universe of objects. Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the results of abstract execution give some ...

In his thesis Paterson proved that equivalence is decidable for program schemata such that every instruction falls on at most one loop and only monadic function signs appear. Here we remove the restriction on function signs. The problem reduces to that ...

This paper presents a mechanism for the arbitration of parallel requests to shared resources. This mechanism is the serialize, which may be described as a kind of protection mechanism, in that it prevents improper orders of access to a protected ...