title: Automatic Generation of Efficient Evaluators for Attribute Grammars

authors:
Ken Kennedy
Scott K. Warren

abstract: The translation process may be divided into a syntactic phase and a semantic phase. Context-free grammars can be used to describe the set of syntactically correct source texts in a formal yet intuitively appealing way, and many techniques are now known for automatically constructing parsers from given CF grammars. Knuth's attribute grammars offer the prospect of similarly automating the implementation of the semantic phase.


venue: popl

title: Mathematical Semantics and Data Flow Programming

abstract: A Data Flow program [1,2] is a flow-chart like network of operators which compute concurrently, dependent only on the availability of the data which flow along the paths. Each operator has only a local effect, transforming input data to output data. Although operators may exhibit memory and thus not be functional from an input to an output, all operators are functions from input sequences to output sequences. This plus the strong locality of effect allows mathematization of semantics more readily than traditional programming languages which are burdened with omnipresent storage and occasional GOTO's. This paper proves the semantic behavior of some elementary Data Flow programs and proves that certain optimization transformations preserve other behaviors.


title: On Directly Constructing LR(k) Parsers Without Chain Reductions

abstract: A chain production is a production of the form A→M where A is a nonterminal and M is either a terminal or nonterminal. Pager in [Pag5] has presented an algorithm which removes all chain reductions from LR(1) parsers after they have been constructed.


title: The Influence of Productions on Derivations and Parsing

authors:
Benton L. Leong
Detlef Wotschke

abstract: The concept of grammar forms [4,5] provides evidence that there seems to be no way to base the definitions of many grammar types used in parsing and compiling solely on the concept of productions.


title: Program Improvement by Source to Source Transformation

abstract: We treat a program as an object of manipulation, determine items of program constancy, and simplify the program based on the constancy. Some motivation for program manipulation is presented, along with two examples of “higher level optimization” written in an Algol-like language. A collection of program transformations and a model of the compilation process in terms of source-to-source transformations are presented. Finally a description of the application of these ideas to an existing programming language is given.


title: Techniques for the Automatic Selection of Data Structures

authors:
James R. Low
Paul Rovner

abstract: We are all aware of the development of increasingly sophisticated, elaborate, and expensive computer programs, particularly in the fields of artificial intelligence, data base management, and intelligent systems. The need for techniques to deal with such complexity has renewed interest in programming language research. Recent work on structured programming, intelligent compilers, automatic program generation and verification, and high-level optimization has resulted.


title: Automatic Design of Data Processing Systems

abstract: An automated business data processing system designer is described. Attention is centered on the I/O aspects of such systems and the development of optimizing design heuristics.


title: A Methodology for Lisp Program Construction from Examples

abstract: This paper reports on a system, THESYS, that synthesizes LISP recursive programs from examples of what they do. There has been recent interest in this form of program specification[1,4,8]. The theory of such inductive systems has been investigated by Blum and Blum[2], Kugel[5] and Summers[10]. In this paper we describe the practical results of an investigation into the problem of program synthesis from examples. The methodology to be presented is based on a firm theoretical foundation which may provide a basis for generalizing the results to other kinds of program synthesis systems. The various theoretical models for computation and data that comprise the theory are not described in detail in this paper but may be found in [10].


title: Goal-Directed Program Transformation

abstract: Program development often proceeds by transforming simple, clear programs into complex, involuted, but more efficient ones. This paper examines ways this process can be rendered more systematic. We show how analysis of program performance, partial evaluation of functions, and abstraction of recursive function definitions from recurring subgoals can be combined to yield many global transformations in a methodical fashion. Examples are drawn from compiler optimization, list processing, very high level languages, and APL execution.


title: Code Generation for Machines with Multiregister Operations

authors:
Alfred V. Aho
Stephen C. Johnson
Jeffrey D. Ullman

abstract: 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 code for expressions involving single and double length operands, using several models of register-pair machines permitting both single and double word instructions. With register-pair machines a new phenomenom arises that is not present in optimal code generation for single register machines: In an optimal evaluation of an expression it may be necessary to oscillate back and forth between evaluating subexpressions of the expression.A linear-time optimal code generation algorithm is derived for a register-pair machine in which all registers are interchangeable. The algorithm is based on showing that for this model there is an optimal evaluation sequence with limited oscillation between the sub-trees dominated by the children of a given node. For other machine models including the familiar even-odd register-pair machine, optimal evaluation sequences can always require unlimited oscillation.


title: An Interprocedural Data Flow Analysis Algorithm

abstract: 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 the procedure, and all of it subcalls. The algorithm is sufficiently powerful to be used on recursive programs and to deal with the sharing of variables which arises through reference parameters. The algorithm is unique in that it can compute all of this information in a single pass, not requiring a prepass to compute calling relationships or sharing patterns. A lower bound for the computational complexity of gathering interprocedural data flow information is derived and the algorithm is shown to be asymptotically optimal. The algorithm has been implemented and it is practical for use even on quite large programs.


title: Minimal and Optimal Computations of Recursive Programs

authors:
Gérard Berry
Jean-Jacques Lévy

abstract: 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]).


title: A Complete and Consistent Hoare Semantics for a Simple Programming Language

authors:
John C. Cherniavsky
Samuel N. Kamin

abstract: Article A complete and consistent hoare axiomatics for a simple programming language Share on Authors: J. Cherniavsky SUNY at Stony Brook, N.Y. SUNY at Stony Brook, N.Y.View Profile , S. Kamin SUNY at Stony Brook, N.Y. SUNY at Stony Brook, N.Y.View Profile Authors Info & Claims POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1977 Pages 1–9https://doi.org/10.1145/512950.512951Online:01 January 1977Publication History 3citation179DownloadsMetricsTotal Citations3Total Downloads179Last 12 Months21Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access


title: Programming Language Constructs for Which it is Impossible to Obtain "Good" Hoare-Like Axiom Systems

abstract: 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 the invariants of loops. S. Cook has shown that if there is a complete proof system for the assertion language (e.g. all true statements of the assertion language) and if the assertion language satisfies a certain natural expressibility condition, then sound and complete axiom systems for a fairly large subset of Algol may be devised. We exhibit programming language constructs for which it is impossible to obtain sound and complete sets of Hoare-like axioms even in this special sense of Cook's. These constructs include (i) recursive procedures with procedure parameters in a programming language which uses static scope of identifiers and (ii) coroutines in a language which allows parameterless recursive procedures. Modifications of these constructs for which it is possible to obtain sound and complete systems of axioms are also discussed.


title: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints

authors:
Patrick Cousot
Radhia Cousot

abstract: 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 information on the actual computations. An intuitive example (which we borrow from Sintzoff [72]) is the rule of signs. The text -1515 * 17 may be understood to denote computations on the abstract universe {(+), (-), (±)} where the semantics of arithmetic operators is defined by the rule of signs. The abstract execution -1515 * 17 → -(+) * (+) → (-) * (+) → (-), proves that -1515 * 17 is a negative number. Abstract interpretation is concerned by a particular underlying structure of the usual universe of computations (the sign, in our example). It gives a summary of some facets of the actual executions of a program. In general this summary is simple to obtain but inaccurate (e.g. -1515 + 17 → -(+) + (+) → (-) + (+) → (±)). Despite its fundamentally incomplete results abstract interpretation allows the programmer or the compiler to answer questions which do not need full knowledge of program executions or which tolerate an imprecise answer, (e.g. partial correctness proofs of programs ignoring the termination problems, type checking, program optimizations which are not carried in the absence of certainty about their feasibility, …).


title: Social Processes and Proofs of Theorems and Programs

authors:
Richard A. DeMillo
Richard J. Lipton
Alan J. Perlis

abstract: Article Free Access Share on Social processes and proofs of theorems and programs Authors: Richard A. DeMillo Georgia Institute of Technology Georgia Institute of TechnologyView Profile , Richard J. Lipton Yale University Yale UniversityView Profile , Alan J. Perlis Yale University Yale UniversityView Profile Authors Info & Claims POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1977 Pages 206–214https://doi.org/10.1145/512950.512970Online:01 January 1977Publication History 22citation680DownloadsMetricsTotal Citations22Total Downloads680Last 12 Months16Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Generalized Left Corner Parsing

abstract: 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 is recognized at its right end, after its yield has been read; and in an LC parser a rule is recognized after the yield of its "left corner" has been read. We generalize on these techniques by allowing the user to specify arbitrarily for each production rule the position at which that rule is to be recognized. The resulting GLC or generalized left corner technique includes the LR, LL, LC, and ELC methods as special cases. It also allows for less conventional parsing strategies, such as grammar splitting [K] with certain component grammars parsed top-down and the others parsed bottom-up, as suggested in [AU].This paper is organized as follows. In Section 2 we give some necessary background and notation. Section 3 defines GLC parsing. A canonical GLC(k) parsing technique can be defined analogous to the LR(k) technique. However, the resulting parsers tend to be unacceptably large. We therefore restrict our attention to the SGLC(k), or simple generalized left corner parsing technique, which is analogous to the SLR(k) technique of DeRemer [D]. We give an algorithm for the construction of SGLC(k) parsing tables and prove that the resulting parser is correct.In Section 4 we develop some potentially useful properties of SGLC(1) parsers. We show that there is a well-defined leftmost position at which each production rule can be recognized, and that a minimal left corner parser can be constructed which recognizes each rule as early as possible. We derive a simple expression relating the size (number of states) of an SGLC(1) parser to the size of the corresponding SLR(1) parser. If G is not left-recursive, then the minimal left-corner parser is the smallest parser for G in this class, while the SLR(1) parser is the largest.In Section 5 we extend the techniques 5 of [HSU] to give an O(n2) algorithm to test whether a grammar with no left recursion is SGLC(1), and if so to compute its minimal left corners.


title: The Evolution of Programs: A System for Automatic Program Modification

authors:
Nachum Dershowitz
Zohar Manna


title: Parallel Program Correctness Through Refinement

abstract: 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 concentrate on one of them and develop a technique for showing that a parallel program is correct with respect to this criterion.


title: An Efficient Insertion-Only Error-Corrector for LL(1) Parsers

authors:
Charles N. Fischer
D. R. Milton
S. B. Quiring

abstract: 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) in correcting syntax errors. Moreover, the error-corrector can be generated automatically from the grammar and a table of terminal symbol insertion costs. The class of LL(1) grammars correctable by this method contains (with minor modifications) grammars used to specify most common programming languages. Preliminary results suggest that this method can be used to advantage in LL(1)-driven compilers.


title: Generalized Common Subexpressions in Very High Level Languages

abstract: 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 of expressions such that along every path leading to n, there will be found a computation of the expression followed by only incidental assignments (i.e. A = A ∪ {x} or A = A - {x}) to its operands and that the number of such assignments is bounded, independent of the path taken. We shall try to justify our definitions and demonstrate the usefulness of this technique by several examples. We shall show that this optimization problem does not fit into the semilattice-theoretic model for global program optimization [Ki, KU, GW], and that the standard iterative algorithm for such problems does not work in this case. We then give several theorems which allow the problem to be solved for reducible flow graphs. The formulae given in the theorems are in such a form that an efficient algorithm can be found by adapting an algorithm given in [U]. The resulting algorithm takes 0(e log e) steps of an extended type, where bit vector operations are regarded as one step, and e is the number of edges of the flow graph. It takes 0(n log n) extended steps for a program flow graph of n nodes.


title: A New Strategy for Code Generation - The General Purpose Optimizing Compiler

abstract: 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 language schema to simplify the task of writing the code generating portions of a compiler without sacrificing code quality. This structure is contrasted with a more conventional structure to explore the reasons why the new structure solves several problems inherent in the conventional structure. Further advantages which accrue from the new structure are also presented.


title: Structuring

abstract: 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 structures. Structuring assignments is preferable to structuring control: the former is more conducive to a mathematical style of programming while the latter is more conducive to tracing.


title: Parallelism and Synchronization in Actor Systems

authors:
Russell R. Atkinson
Carl Hewitt

abstract: 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 resource. The mechanism is a generalization and improvement of the monitor mechanism of Brinch-Hansen and Hoare.Serializers attempt to systematize and abstract desirable structural features of synchronization control structure into a coherent language construct. They represent an improvement in the modularity of synchronization over monitors in several respects. Monitors synchronize requests by providing a pair of operations for each request type [examples are STARTREAD/ENDREAD and STARTWRITE/ENDWRITE for the readers-writers problems]. Such a pair of operations must be used in a certain order for the synchronization to work properly, yet nothing in the monitors construct enforces this use. Serializers incorporate this structural aspect of synchronization in a unified mechanism to guarantee proper check-in and check-out. In scheduling access to a protected resource, it is often desired to wait in a queue for a certain condition before it continues execution. Monitors require that a process waiting in a queue will remain dormant forever, unless another process explicitly signals to the dormant process that it should continue. Serializers improve the modularity of synchronization by providing that the condition for resuming execution must be explicitly stated when a process enters a queue making it it unnecessary for processes to signal other processes. Each process determines for itself the conditions required for its further execution.The behavior of a serializer is defined using the actor message-passing model of computation. Different versions of the "readers-writers" problems are used to illustrate how the structure of a serializer corresponds in a natural way to the structure of the arbitration problem to be solved. The correspondence makes it easier to synthesize a scheduler from behavioral specifications and to verify that an implementation satisfies its specifications.No claim is made for the "completeness" of the serializer mechanism, beyond showing that semaphores can be implemented using serializers. Further, no "complete" solution is proposed to the "no-starvation" specification which requires that a resource reply to each request which it receives. Rather, it is shown for some simple examples that serializers represent a step toward better structuring of parallel access to shared resources, and that proofs that starvation is impossible for these examples are easier with serializers than with some of the currently existing mechanisms for controlling parallel access to resources.


title: Applications of Graph Grammar for Program Control Flow Analysis

authors:
Ken Kennedy
Linda Zucconi

abstract: 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 flow graph to produce data flow information, possible optimizations, etc. [A1,A2,AC,AU2,AU3,CS,HU1,HU2.HU3,Ke1,Ke2,Ke3,Ke4,Sc,U]. Studies of the form of typical control flow graphs indicate that such graphs tend to fall into a restricted subclass of general graphs. For example, empirical investigations have shown that the vast majority of program graphs have no multiple-entry loops [AC,HU2,HU3,Kn1].The recent work on "structured programming" has suggested that "good" programs fall into an even more restricted subclass. In fact, purists recommend that all programs be synthesized from three basic control structures: sequential statements, if-then-else statements, and single-entry single-exit loops [Di,Wi].Formal language theory [HoU] has given us a practical way to specify the set of strings which comprise a given language: via a grammar. It is then a natural idea to extend grammars from the strings to graphs in hopes of getting the same power of expression. Several researchers have used this approach [FKZ,J2,Ro].In this paper we study the applicability of a grammatical approach to describing the set of control flow graphs which arise from "good" programs in the sense proposed by many programming practitioners. The resulting flow graph language contains all those programs constructed according to the purists' rules and also admits programs with multiple-exit loops if such loops are constructed sensibly. The grammar we use is the "semi-structured flow graph" grammar GSSFG which was studied originally in [FKZ]. There are several appealing properties of this grammar; perhaps the most important, from the point-of-view of a compiler-writer, is the existence of a linear-time parsing algorithm which leads directly to a linear-time data flow analysis method [FKZ].In the present work we summarize the results from [FKZ] and address several new questions. First, how often do programs written by people with no knowledge of the SSFG rules fall into the language defined by GSSFG? In other words, is the language a natural one for programming? Second, once a program has been parsed according to GSSFG do benefits other than fast data flow analysis accrue?The paper is organized into three main sections. Section II introduces GSSFG and the parsing algorithm from [FKZ]. Section III is devoted to an empirical study conducted by the authors in an attempt to answer the question of naturalness, described above. Section IV discusses several applications of the graph parse in a "graph attribute grammar" framework. The summary at the end of the paper includes suggestions for further investigation.


title: Threshold Evaluation and the Semantics of Call by Value, Assignment and Generic Procedures

abstract: 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 McCarthy's transformation of iterative programs into recursive ones provided the same threshold is used for assignment and parameter passing.


title: The Equivalence Problem for Program Schemata with Nonintersecting Loops

abstract: 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 of showing that the numerical exponents which satisfy certain word equations over a semigroup of acyclic directed graphs may be characterized by sentences of Presburger arithmetic; these exponents correspond to loop coefficients of the program schemata. The central construction is a finite automaton whose memory is a window of bounded size on an acyclic directed graph corresponding to a solution to such a word equation.


title: On the Covering of Left Recursive Grammars

abstract: 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.


title: Reduction in Strength of High Level Operations

authors:
Robert Paige
Jacob T. Schwartz


title: The Competence/Performance Dichotomy in Programming

abstract: 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 efficiency) of his program need not involve himself in any aspect of the storage allocation problem. We focus on what we feel is a sensible next step, the problem of automating aspects of control. To accomplish this we propose a definition of control based on a fact/heuristic dichotomy, a variation of Chomsky's competence/performance dichotomy. The dichotomy formalizes an idea originating with McCarthy and developed by Green, Hewitt, McDermott, Sussman, Hayes, Kowalski and others. It allows one to operate arbitrarily on the control component of a program without affecting the program's correctness, which is entirely the responsibility of the fact component. The immediate objectives of our research are to learn how to program keeping fact and control separate, and to identify those aspects of control amenable to automation.


title: Symbolic Evaluation and the Global Value Graph

authors:
John H. Reif
Harry R. Lewis

abstract: 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 only by a directed graph whose nodes are blocks of assignment statements. We show that if such a program model is interpreted in the domain of integer arithmetic then many natural global flow problems are unsolvable. We then develop a direct (non-iterative) method for finding general symbolic values for program expressions. Our method gives results similar to an iterative method due to Kildall and a direct method due to Fong, Kam, and Ullman. By means of a structure called the global value graph which compactly represents both symbolic values and the flow of these values through the program, we are able to obtain results that are as strong as either of these algorithms at a lower time cost, while retaining applicability to all flow graphs.


title: Applications of High-Level Control Flow

abstract: 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. Applications of the new style of representation include denotational semantics, data flow analysis, source level compiler diagnostics, and program proving.


title: Elimination of Single Productions from LR Parsers in Conjunction with the Use of Default Reductions

abstract: 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 savings in both space and time. Therefore, much effort has been devoted to the development of methods for eliminating reductions by single productions from LR parsers (Aho and Ullman [1973a,1973b], Anderson, Eve and Horning[1973], Pager[1973a,1974], Demers[1974,1975], Backhouse [1976], Joliat[1976], Koskimies[1976], LaLonde [1976], Soisalon-Soininen[1976]).


title: Implementation of an Array Bound Checker

authors:
Norihisa Suzuki
Kiyoshi Ishihata

abstract: 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 and a condition that the subscript is smaller than or equal to the upper bound are checked and the results indicating within the bound, out of bound, or undetermined are produced. It can check ordinary programs at about fifty lines per ten seconds, and it shows linear time complexity behavior.It has been long discussed whether program verification will ever become practical. The main argument against program verification is that it is very hard for a programmer to write assertions about programs. Even if he can supply enough assertions, he must have some knowledge about logic in order to prove the lemmas (or verification conditions) obtained from the verifier.However, there are some assertions about programs which must always be true no matter what the programs do; and yet which cannot be checked for all cases. These assertions include: integer values do not overflow, array subscripts are within range, pointers do not fall off NIL, cells are not reclaimed if they are still pointed to, uninitialized variables are not used.Since these conditions cannot be completely checked, many compilers produce dynamic checking code so that if the condition fails, then the program terminates with proper diagnostics. These dynamic checking code sometimes take up much computation time. It is better to have some checking so that unexpected overwriting of data will not occur, but it is still very awkward that the computation stops because of error. Moreover, these errors can be traced back to some other errors in the program. If we can find out whether these conditions will be met or not before actually running the program, we can benefit both by being able to generate efficient code and by being able to produce more reliable programs by careful examination of errors in the programs. Similar techniques can be used to detect semantically equivalent subexpressions or redundant statements to do more elaborate code movement optimization.The system we have constructed runs fast enough to be used as a preprocessor of a compiler. The system first creates logical assertions immediately before array elements such that these assertions must be true whenever the control passes the assertion in order for the access to be valid. These assertions are proved using similar techniques as inductive assertion methods. If an array element lies inside a loop or after a loop a loop invariant is synthesized. A theorem prover was created which has the decision capabilities for a subset of arithmetic formulas. We can use this prover to prove some valid formulas, but we can also use it to generalize nonvalid formulas so that we can hypothesize more general loop invariants.Theoretical considerations on automatic synthesis of loop invariants have been taken into account and a complete formula for loop invariants was obtained. We reduced the problem of loop invariant synthesis to the computation of this formula. This new approach of the synthesis of loop invariant will probably give more firmer basis for the automatic generation of loop invariants in general purpose verifiers.


title: Clauses: Scope Structures and Defined Functions in Lucid

authors:
Edward A. Ashcroft
William W. Wadge

abstract: In this paper we describe how Lucid can be extended to allow user-defined functions and scope conventions, i.e. conventions for limiting the range or scope of the validity of definitions. This is done using new constructs called clauses which are similar in form to the blocks and procedure declarations of Algol-like languages, but are nevertheless strictly non-imperative, because a clause is actually a compound assertion, i.e. an assertion formed, as a program is, by combining a collection of assertions.Each type of clause (there are four) has a straightforward mathematical semantics together with its own characteristic "manipulation rules" for general program massage. In addition, the informal operational view of (some) Lucid programs (described in a previous paper) can be extended to give an (incomplete) operational understanding of the effect of the clauses. In this framework a "compute" clause defines a block; a "mapping" clause defines a conventional (pointwise) function; a "produce" clause defines a block with persistent memory (or an anonymous 'process' or 'actor'); and a "function" clause defines a sort of procedure with own variables (or a general kind of coroutine).


title: Unrestricted Procedure Calls in Hoare's Logic

authors:
Robert Cartwright
Derek C. Oppen

abstract: This paper presents a new version of Hoare's logic including generalized procedure call and assignment rules which correctly handle aliased variables. Formal justifications are given for the new rules.


title: Automatic Discovery of Linear Restraints Among Variables of a Program

authors:
Patrick Cousot
Nicolas Halbwachs

abstract: The model of abstract interpretation of programs developed by Cousot and Cousot [2nd ISOP, 1976], Cousot and Cousot [POPL 1977] and Cousot [PhD thesis 1978] is applied to the static determination of linear equality or inequality invariant relations among numerical variables of programs.


title: Almost Control-Free (Indeterministic) Parallel Computation on Permit Schemes

abstract: The parallelity means "simultaneous performance or execution" and it may concern either computer units of different sorts (e.g. a memory and a processor), or computer units of the same sort (e.g. several processors).The computers Illiac 4 and Burroughs Scientific Processor (BSP) (announced recently) have several arithmetic processors. They are designed for large-scale computations with a special sort of numeric data structures, i.e. with large matrices (arrays). Their parallelity concerns naturally and essentially the definitions of matrix operations.According to [Br] the software techniques for exploiting the parallelism of the BSP consists of a "vectorization" of an usual serial program. There are 16 processors in the BSP which are heavily dependent each on the other, because at each instant by each of these processors just one and the same operation may be performed. Therefore a synchronization of all processors is assumed, which is the most important difference from the concept of parallel program scheme of [KM], which allows to speak about a sequence of particular steps, each of which is represented by execution of particular statements in parallel.In this paper a parallel computer with m ≥ 1 processors is assumed, which is also synchronized [Cu 1], but the processors are fully independent each on the other, i.e. on different processors different operations may be performed at each instant. Further, the parallelity concerns arbitrary simple data and arbitrary operations in all generality (and not only matrices). Thus the inherent parallelity of any serial program should be discovered and used for speeding up the duration of computation at most m times, while the memory space requirements remain unchanged.In [Cu 2] parallel flow diagrams were introduced and further the following "parallelization " (i.e. a "computation" of a parallel execution sequence of steps) of a serial program, was discussed in two parts: 1) newly permitted statements are determined by a permitter, and then 2) a subset of m (or less) statements is selected from the set of all permitted (and not yet selected) statements by a selector. The selected statements are executed in parallel on m processors, etc. until all permitted statements are selected (and executed), and the computation terminates. The permitter and the selector should replace the statement counter of serial programs or flow diagrams, by which is determined which statement should be executed as the next one. It is nuclear whether a suitable hardware technology can be designed to perform as a permitter and selector require.The linearity of programs is connected with serial computers (having just one processor, thus m = 1) essentially, and therefore in the following flow diagrams (or program schemes) will be used instead, because they allow a natural and transparent modification to permit diagrams and schemes, which represent a new sort of computing prescription (not necessarily deterministic algorithms) being a generalization of well-known binary trees, by which usual arithmetic expressions are represented.It is well known that there is no inherent reason for performing an operation from the numerator of a fraction sooner than an operation from the denominator. This arbitrariness of the order conceals an intrinsic parallelism of any expression which contains an n-ary operation with n ≥ 2 (which corresponds to the fact that the value of such operation does not depend on the order in which the values of its n arguments were achieved). This obvious fact is less clear when algorithms instead of operations are considered.


title: Data Types as Values: Polymorphism, Type-Checking, Encapsulation

authors:
Alan J. Demers
James E. Donahue
Glenn Skinner

abstract: This paper describes a novel approach to the treatment of data types in programming languages, which allows a simple interpretation of "polymorphic" or "generic" procedures, makes a simple set of type-checking rules semantically justifiable and provides a straightforward treatment of encapsulation.


title: Off-Line and On-Line Algorithms for Deducing Equalities

authors:
Peter J. Downey
Hanan Samet
Ravi Sethi

abstract: The classical common subexpression problem in program optimization is the detection of identical subexpressions. Suppose we have some extra information and are given pairs of expressions ei1=ei2 which must have the same value, and expressions fj1≠fj2 which must have different values. We ask if as a result, h1=h2, or h1≠h2. This has been called the uniform word problem for finitely presented algebras, and has application in theorem-proving and code optimization. We show that such questions can be answered in O(nlogn) time, where n is the number of nodes in a graph representation of all relevant expressions. A linear time algorithm for detecting common subexpressions is derived. Algorithms which process equalities, inequalities and deductions on-line are discussed.


title: Automating Proofs of the Absence of Common Runtime Errors

abstract: The Runcheck Verifier is a working system for proving the absence of common runtime errors. The language accepted is Pascal without variant records, side effects in functions, shared variable parameters to procedures, or functional arguments. The errors checked are: 1) accessing a variable that has not been assigned a value, 2) array subscripting out of range, 3) subrange type error, 4) dereferencing a NIL pointer, 5) arithmetic overflow, and 6) division by zero.


title: A New Method for Compiler Code Generation

authors:
R. Steven Glanville
Susan L. Graham

abstract: An algorithm is given to translate a relatively low-level intermediate representation of a program into assembly code or machine code for a target computer. The algorithm is table driven. A construction algorithm is used to produce the table from a functional description of the target machine. The method produces high quality code for many commercially available computers. By replacing the table, it is possible to retarget a compiler for another kind of computer. In addition techniques are given to prove the correctness of the translator.


title: A Metalanguage for Interactive Proof in LCF

authors:
Michael J. C. Gordon
Robin Milner
F. Lockwood Morris
Malcolm C. Newey
Christopher P. Wadsworth

abstract: Article Free Access Share on A Metalanguage for interactive proof in LCF Authors: M. Gordon University of Edinburgh University of EdinburghView Profile , R. Milner University of Edinburgh University of EdinburghView Profile , L. Morris Syracuse University Syracuse UniversityView Profile , M. Newey Australian National University Australian National UniversityView Profile , C. Wadsworth University of Edinburgh University of EdinburghView Profile Authors Info & Claims POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1978Pages 119–130https://doi.org/10.1145/512760.512773Published:01 January 1978Publication History 55citation684DownloadsMetricsTotal Citations55Total Downloads684Last 12 Months96Last 6 weeks5 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Compilation and Delayed Evaluation in APL

authors:
Leonidas J. Guibas
Douglas K. Wyatt

abstract: Most existing APL implementations are interpretive in nature, that is, each time an APL statement is encountered it is executed by a body of code that is perfectly general, i.e. capable of evaluating any APL expression, and is in no way tailored to the statement on hand. This costly generality is said to be justified because APL variables are typeless and thus can vary arbitrarily in type, shape, and size during the execution of a program. What this argument overlooks is that the operational semantics of an APL statement are not modified by the varying storage requirements of its variables.


title: A Partial Evaluator, Its Use for Compiling Iterative Statements in Lisp

abstract: A partial evaluation program for LISP is described, and an application where it has been used. The partial evaluator performs a number of other, related operations such as opening of functions and certain optimizations on programs. The application is based on the fact that we can generate from an interpreter and a partial evaluator the same object code as a corresponding compiler should do. The paper will first formally describe the relationship between an interpreter and a compiler through partial evaluation. The partial evaluator system is then briefly described and finally an experiment is shown where an interpreter for the iterative statement in INTERLISP is partially evaluated.


title: Nondeterminism in Logics of Programs

authors:
David Harel
Vaughan R. Pratt

abstract: We investigate the principles underlying reasoning about nondeterministic programs, and present a logic to support this kind of reasoning. Our logic, an extension of dynamic logic ([22] and [12]), subsumes most existing first-order logics of nondeterministic programs, including that developed by Dijkstra based on the concept of weakest precondition. A significant feature is the strict separation between the two kinds of nonterminating computations: infinite computations and failures. The logic has a Tarskian truth-value semanics, an essential prerequisite to establishing completeness of axiomatizations of the logic. We give an axiomatization for flowchart (regular) programs that is complete relative to arithmetic in the sense of Cook. Having a satisfactory tool at hand, we turn to the clarification of the concept of the total correctness of nondeterministic programs, providing in passing, a critical evaluation of the widely used "predicate transformer" approach to the definition of programming constructs, initiated by Dijkstra [5]. Our axiom system supplies a complete axiomatization of wp.


title: The Smalltalk-76 Programming System

abstract: This paper describes a programming system based on the metaphor of communicating objects. Experience with a running system shows that this model provides flexibility, modularity and compactness. A compiled representation for the language is presented, along with an interpreter suitable for microcoding. The object-oriented model provides naturally efficient addressing; a corresponding virtual memory is described which offers dense utilization of resident space.


title: A Portable Compiler: Theory and Practice

abstract: A compiler for the C language has recently been constructed which is now compiling C for about half a dozen machines. The compiler was influenced in various ways by recent theoretical developments. This paper gives an overview of the compiler structure and algorithms, emphasizing those areas where theory was helpful, and discussing the approaches taken where theory was lacking.


title: Local Constraints in the Syntax and Semantics of Programming Languages

authors:
Aravind K. Joshi
Leon S. Levy
Kang Yueh

abstract: The method of local constraints attempts to describe context-free languages in an apparently context-sensitive form which helps to retain the intuitive insights about the grammatical structure. This form of description, while apparently context-sensitive is, in fact, context-free and allows a program derivation structure to be represented as a tree with additional constraints, thus allowing for the possibility of a correctness proof in the form of Knuthian semantics. A part of ALGOL 60 syntax has been restated as a grammar with local constraints. It is also shown that parsing of grammars with local constraints can be carried out by a suitable extension of Early's algorithm. Finally, the relationship of local constraints to the semantics of programs is discussed in Section 4 by considering some program transformations.


title: A General Scheme for the Automatic Inference of Variable Types

authors:
Marc A. Kaplan
Jeffrey D. Ullman

abstract: We present the best known algorithm for the determination of run-time types in a programming language requiring no type declarations. We demonstrate that it is superior to other published algorithms and that it is the best possible algorithm from among all those that use the same set of primitive operators.


title: A Straightforward Denotational Semantics for Non-Determinant Data Flow Programs

abstract: Data flow programming languages are especially amenable to mathematization of their semantics in the denotational style of Scott and Strachey. However, many real world programming problems, such as operating systems and data base inquiry systems, require a programming language capable of non-determinacy because of the non-determinate behavior of their physical environment. To date, there has been no satisfactory denotational semantics of programming languages with non-determinacy. This paper presents a straightforward denotational treatment of non-determinate data flow programs as functions from sets of tagged sequences to sets of tagged sequences. A simple complete partial order on such sets exists, in which the data flow primitives are continuous functions, so that any data flow program computes a well defined function.


title: Verification and Design Aspects of "True" Concurrency

abstract: Most abstract models of a set of parallel processes define a computation of the model to be a sequence. It is either a sequence of actions taken by the system [Lip] or a sequence of states of the system existing between actions [Kel, Lau, Ash]. Parallelsim is represented only by the fact that following a given action or state, the "next" action or state is not necessarily unique. That is, parallesim is represented by nondeterminism. A. W. Holt has called this representation approach "serializable concurrency" as opposed to "true concurrency" [Hol]. He, among others, has questioned the appropriateness of implying a total ordering between events that are only known to be partially ordered.In this paper, a definition of an algebraic model of a set of concurrently-executing sequential processes is presented. The "computations" of this model are directed acyclic graphs. The nodes of each computation graph represent computer operations and the edges represent the partial ordering of operations with respect to time.Examples demonstrate that these directed acyclic graphs aid in focusing a programmer/verifier's attention on the most important features of a computation. The model suggests the following verification paradigm: since systems often execute a certain sequence of actions to achieve a certain goal, verification procedures should identify these sequences, whether or not each is performed within a single process.A key notion in the abstract model is the treatment of synchronization mechanisms as full-fledged processes. A programming language syntax called "path programs" which is suggested by this notion is presented. Path programs are a generalization of the path expressions of Campbell and Habermann [CamHab]. The programming notation is based on the assumption that a processor can be dedicated to each shared data structure in the system. The duty of this processor is to control the synchronization of operations on the data structure.


title: A Simplifier Based on Efficient Decision Algorithms

authors:
Charles G. Nelson
Derek C. Oppen

abstract: We describe a simplifier for use in program manipulation and verification. The simplifier finds a normal form for any expression over the language consisting of individual variables, the usual boolean connectives, the conditional function cond (denoting if-then-else), the integers (numerals), the arithmetic functions and predicates +, - and ≤, the LISP constants, functions and predicates nil, car, cdr, cons and atom, the functions store and select for storing into and selecting from arrays, and uninterpreted function symbols. Individual variables range over the union of the rationals, the set of arrays, the LISP s-expressions and the booleans true and false. The constant, function and predicate symbols take their natural interpretations.The simplifier is complete; that is, it simplifies every valid formula to true. Thus it is also a decision procedure for the quantifier-free theory of rationals, arrays and s-expressions under the above functions and predicates.The organization of the simplifier is based on a method for combining decision algorithms for several theories into a single decision algorithm for a larger theory containing the original theories. More precisely, given a set S of functions and predicates over a fixed domain, a satisfiability program for S is a program which determines the satisfiability of conjunctions of literals (signed atomic formulas) whose predicates and function signs are in S. We give a general procedure for combining satisfiability programs for sets S and T into a single satisfiability program for S ∪ T, given certain conditions on S and T. We show how a satisfiability program for a set S can be used to write a complete simplifier for expressions containing functions and predicates of S as well as uninterpreted function symbols.The simplifier described in this paper is currently used in the Stanford Pascal Verifier.


title: Complexity of Expressions Allowing Concurrency

authors:
William F. Ogden
William E. Riddle
William C. Rounds

abstract: We study some consequences of the formal language approach to modelling software system behavior for the case of asynchronous, concurrent subsystems. We use the formal language shuffle operation to give an "algebraic" definition of semantics for a simple (structured) concurrent programming language and prove that the use of this operation is necessary. Having established this necessity, we investigate other types of behavioral expressions which use the operation and show that the analysis problem for these expressions is either undecidable or intractable. The results provide some limitations, for example, on the path expression method of system behavior analysis. Our lower bound proofs involve the use of synchronization symbols, which seem to be a formal language analogue of semaphores.


title: Reasoning about Recursively Defined Data Structures

abstract: A decision algorithm is given for the quantifier-free theory of recursively defined data structures which, for a conjunction of length n, decides its satisfiability in time linear in n. The first-order theory of recursively defined data structures, in particular the first-order theory of LISP list structure (the theory of CONS, CAR, CDR), is shown to be decidable but not elementary recursive.


title: A Forward Move Algorithm for LR Error Recovery

authors:
Thomas J. Pennello
Frank DeRemer

abstract: A move algorithm, and some of its formal properties, is presented for use in a practical syntactic error scheme for LR parsers. The algorithm finds fragment (comparable to a valid prefix) just to the right of a point of error detection. For expositional purposes the algorithm is presented as parsing arbitrarily far beyond the point of error detection in a parallel mode, as long as all parses agree on the read or reduce action to be taken at each parse step. In practice the forward move is achieved serially by adding recovery states to the LR machine. Based on the formal properties of the forward move we propose an error algorithm that uses the accumulated right context. The performance of the algorithm is illustrated in a specific case and discussed in general.


title: Efficient Computation of Expressions with Common Subexpressions

authors:
Bhaskaram Prabhala
Ravi Sethi


title: Symbolic Programming Analysis in Almost Linear Time

abstract: A global flow model is assumed; as usual, the flow of control is represented by a digraph called the control flow graph. The objective of our program analysis is the construction of a mapping (a cover) from program text expressions to symbolic expressions for their value holding over all executions of the program. The particular cover constructed by our methods is in general weaker than the covers obtainable by the methods of [Ki, FKU, R1], but our method has the advantage of being very efficient; requiring O(ℓ + aα(a)) extended bit vector operations (a logical operation or a shift to the first nonzero bit) on all control flow graphs (whether reducible or not), where a is the number of edges of the control flow graph, ℓ is the length of the text of the program, and α is Tarjan's function (an extremely slowly growing function).


title: Syntactic Control of Interference

abstract: In programming languages which permit both assignment and procedures, distinct identifiers can represent data structures which share storage or procedures with interfering side effects. In addition to being a direct source of programming errors, this phenomenon, which we call interference can impact type structure and parallelism. We show how to eliminate these difficulties by imposing syntactic restrictions, without prohibiting the kind of constructive interference which occurs with higher-order procedures or SIMULA classes. The basic idea is to prohibit interference between identifiers, but to permit interference among components of collections named by single identifiers.


title: Monoids for Rapid Data Flow Analysis

abstract: The earliest data flow analysis research dealt with concrete problems (such as detection of available expressions) and with low level representations of control flow (with one large graph, each of whose nodes represents a basic block). Several recent papers have introduced an abstract approach, dealing with any problem expressible in terms of a semilattice L and a monoid M of isotone maps from L to L, under various algebraic constraints. Examples include [CC77; GW76; KU76; Ki73; Ta75; Ta76; We75]. Several other recent papers have introduced a high level representation with many small graphs, each of which represents a small portion of the control flow information in a program. The hierarchy of small graphs is explicit in [Ro77a; Ro77b] and implicit in papers that deal with syntax directed analysis of programs written within the confines of classical structured programming [DDH72, Sec. 1.7]. Examples include [TK76; ZB74]. The abstract papers have retained the low level representations while the high level papers have retained the concrete problems of the earliest work. This paper studies abstract conditions on L and M that lead to rapid data flow analysis, with emphasis on high level representations. Unlike some analysis methods oriented toward structured programming [TK76; Wu75; ZB74], our method retains the ability to cope with arbitrary escape and jump statements while it exploits the control flow information implicit in the parse tree.


title: Type Definitions with Parameters

abstract: It has long been known that recursively defined types in a highly typed language such as Algol 68 or Pascal may be tested for structural equivalence by the same algorithm that compares finite automata [5,11]. Several authors (for example, [3,8,9,16]) have proposed that classes of types be simultaneously defined by the use of parameterized type definitions, such asType list(x) = record val:x; next:↑list(x) end .This paper shows that unless the use of such parameterized definitions is restricted, new (unparameterized) types may be defined which more closely resemble deterministic context-free languages. In fact, the equivalence problem for such types becomes as hard as the (currently unsolved) deterministic pushdown automaton equivalence problem. Several restrictions on type definitions are considered which allow known equivalence algorithms to be applied.


title: The Universality of Data Retrieval Languages

authors:
Alfred V. Aho
Jeffrey D. Ullman

abstract: We consider the question of how powerful a relational query language should be and state two principles that we feel any query language should satisfy. We show that although relational algebra and relational calculus satisfy these principles, there are certain queries involving least fixed points that cannot be expressed by these languages, yet that also satisfy the principles. We then consider various extensions of relational algebra to enable it to answer such queries. Finally, we discuss our extensions to relational algebra in terms of a new programming language oriented model for queries.


title: Predicate Path Expressions

abstract: Path expressions are a tool for synchronization of concurrent processes. They are an integral part of the data abstraction mechanism in a programming language, and specify synchronization entirely in terms of the allowable sequences of operations on an object of the abstract data type. This paper describes an attempt to push the path expression synchronization construct along three dimensions - specification, verification, and implementation - into a useful theoretical and practical tool. We define Predicate Path Expressions (PPEs), which allow for a more convenient specification of many synchronization problems. The predicate is a powerful extension to path expressions that increases their expressiveness. We formally define the semantics of PPEs by a transformation to a corresponding nondeterministic program, thus allowing the use of known verification techniques for nondeterministic programs to be used for proving properties of the PPE and the data abstraction of which it is a part. We also describe our existing implementation, in Algol 68, of a data abstraction mechanism that incorporates PPEs.


title: An Efficient Way to Find Side Effects of Procedure Calls and Aliases of Variables

abstract: Article Free Access Share on An efficient way to find the side effects of procedure calls and the aliases of variables Author: John P. Banning Stanford Linear Accelerator Center, Stanford, California and Amdahl Corporation, Sunnyvale, California Stanford Linear Accelerator Center, Stanford, California and Amdahl Corporation, Sunnyvale, CaliforniaView Profile Authors Info & Claims POPL '79: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1979 Pages 29–41https://doi.org/10.1145/567752.567756Online:01 January 1979Publication History 161citation871DownloadsMetricsTotal Citations161Total Downloads871Last 12 Months15Last 6 weeks5 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: First Order Programming Logic

authors:
Robert Cartwright
John McCarthy

abstract: First Order Programming Logic is a simple, yet powerful formal system for reasoning about recursive programs. In its simplest form, it has one major limitation: it cannot establish any property of the least fixed point of a recursive program which is false for some other fixed point. To rectify this weakness, we present two intuitively distinct approaches to strengthening First Order Programming Logic and prove that either extension makes the logic relatively complete. In the process, we prove that the two approaches are formally equivalent. The relative completeness of the extended logic is significant because it suggests it can establish all "ordinary" properties (obviously we cannot escape the Godelian incompleteness inherent in any programming logic) of recursive programs including those which compute partial functions.The second contribution of this paper is to establish that First Order Programming Logic is applicable to iterative programs as well. In particular, we show that the intermittent assertions method--an informal proof method for iterative programs which has not been formalized--is conveniently formalized simply as sugared First Order Programming Logic applied to the recursive translations of iterative programs.


title: The Logic of a Relational Data Manipulation Language

authors:
Marco A. Casanova
Philip A. Bernstein

abstract: 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 tuple from a relation. The usual operations on relations-retrieve, insert, delete, update-are then defined as special cases of the relational assignment, and the for-each construct scanning a relation tuple by tuple is introduced with the help of the random tuple selection.


title: Synthesis of Resource Invariants for Concurrent Programs

abstract: 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 resource. Proofs of synchronization properties are constructed by devising predicates called resource invariants which describe relationships among the variables of a resource when no process is in a critical region for the resource. In constructing proofs using the system of Owicki and Gries, the programmer is required to supply the resource invariants.We show that convexity plays a key role in the derivation of strong resource invariants. We also develop methods for automatically synthesizing resource invariants. Specifically, we characterize the resource invariants of a concurrent program as least fixpoints of a functional which can be obtained from the text of the program. By using this fixpoint characterization and a widening operator which exploits our observation on the importance of convexity, good approximations may be obtained for the resource invariants of many concurrent programs.


title: Characterization and Elimination of Redundancy in Recursive Programs

abstract: 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 values. The existence and nature of the redundancy depend on properties of the functions ci. We explore four sets of assumptions about these functions. We analyze directed acyclic graphs formed by merging the nodes of the computation tree for f(x) which are known to be equal for each set of assumptions. In each case there is a transformed program which computes f(x) without redundancy, provided that certain additional assumptions about p, a, and the ci are satisfied. The transformed programs avoid redundancy by saving exactly those intermediate results which will be needed again later in the computation. These programs are all valueless recursive procedures which leave intermediate and final results in specified global locations; in each case recursion can be eliminated without use of a stack. We compare the storage requirements of the transformed programs, discuss the applicability of these transformations to an automatic program improvement system, and present a general criterion for establishing the existence of redundancy.


title: Automatic Generation of Near-Optimal Translators for Noncircular Attribute Grammars

authors:
Rina S. Cohen
E. Harry

abstract: 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 techniques are available for automatically generating efficient parsers for context-free grammars. Attribute grammars offer the prospect of similarly automating the implementation of the semantic phase. In this paper we present a general method of constructing, for any non-circular attribute grammar, a deterministic translator which will perform the semantic evaluation of each syntax tree of the grammar in time linear with the size of the tree. Each tree is traversed in a manner particularly suited to the shape of the tree, yielding a near optimal evaluation order for that tree. Basically, the translator consists of a finite set of "Local Control Automata", one for each production; these are ordinary finite-state acyclic automata augmented with some special features, which are used to regulate the evaluation process of each syntax tree. With each node in the tree there will be associated the Local Control Automaton of the production applying at the node. At any given time during the translation process all Local Control Automata are inactive, except for the one associated with the currently processed node, which is responsible for directing the next steps taken by the translator until control is finally passed to a neighbour node, reactivating its Local Control Automaton. The Local Control Automata of neighbour nodes communicate with each other.The construction of the translator is custom tailored to each individual attribute grammar. The dependencies among the attributes occurring in the semantic rules are analysed to produce a near-optimal evaluation strategy for that grammar. This strategy ensures that during the evaluation process, each time the translator enters some subtree of the syntax tree, at least one new attribute evaluation will occur at each node visited. It is this property which distinguishes the method presented here from previously known methods of generating translators for unrestricted attribute grammars, and which causes the translators to be near-optimal.


title: A PL/CV Precis

authors:
Robert L. Constable
Scott Johnson

abstract: 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 verification. The Proof Checker is efficient enough for classroom use. Early experience with PL/CV indicates that it nicely supports formal verification of elementary arguments. Continued work should enable the formalization of non-elementary reasoning as well.


title: Systematic Design of Program Analysis Frameworks

authors:
Patrick Cousot
Radhia Cousot

abstract: 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.


title: The Functional Power of Parameter Passage Mechanisms

abstract: 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 of programming languagesJanuary 1979 Pages 158–168https://doi.org/10.1145/567752.567767Online:01 January 1979Publication History 2citation201DownloadsMetricsTotal Citations2Total Downloads201Last 12 Months5Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Automatic Improvement of Programs in Very High Level Languages

abstract: 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 set-formers and inductively computable predicates which can be evaluated with an order of magnitude improvement of the asymptotic running time as compared to the straightforward evaluation. The quantity developed for this comparison can be used to derive further results when additional information is known. For programs written in very high level languages, which often consist mostly of "nested" iterative constructs, this technique amounts to altering the "algorithm" used to compute the program by replacing it with an asymptotically faster algorithm.


title: A Compact, Machine-Independent Peephole Optimizer

abstract: 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 they were machine-independent and parametrized by symbolic machine descriptions. This paper describes such a compact, machine-independent peephole optimizer.


title: Principles of Proving Programs Correct in Gypsy

authors:
Donald I. Good
Richard M. Cohen
James G. Keeton-Williams

abstract: 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 can be applied both to terminating and non-terminating processes, and the proof methods are well suited to automated verification aids. The basic principles of these methods and their interaction with the design of Gypsy are described.


title: Specifying Programming Language Semantics

authors:
Irene Greif
Albert R. Meyer

abstract: 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 showing that the definitions are what they call "consistent". However, their treatment skirts the question of whether their definitions can each be taken to specify the language adequately. Although, as we will show, any one of the kinds of semantics they discuss -- operational, relational, deductive -- can be used to specify meaning uniquely, Hoare and Lauer do not make the case in their paper. In fact, both their relational and deductive definitions are satisfied by several different semantics, only one of which is desired.Thus, the main point of this paper is to clarify the characteristics of a proper specification of language semantics and to formulate alternative specifications each of which is equally good as the language definition. We basically agree with Hoare and Lauer that several specifications can and should be given, but are disturbed by confusions about such specifications, some of which are illustrated in their paper. In particular we refer to confusions between the mathematical object which is designated to be the meaning of a program and methods for specifying that object; the similar confusion between predicate and expression; between consistency and equivalence of two definitions; between completeness of a theory and its having a unique model. While these issues are familiar in mathematical logic, we take this opportunity to survey them in the context of programming language semantics.This paper can be read without prior familiarity with Hoare and Lauer's paper. The authors plan another paper extending this work which will include a more comprehensive bibliography.


title: Decisions for "Type" in APL

authors:
W. E. Gull
Michael A. Jenkins

abstract: 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 systematically presented. They are classified according to the possibility of maintaining important identities involving level-manipulating functions in the case of empty arguments, to their effect on other design choices still to be made (the restriction to homogeneous arrays and the definition of the nature of basic data), and to their ability to express "type" in a natural way.


title: Recursion in Logics of Programs

abstract: 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 results are the arithmetical completeness of axiom systems for (1) context-free dynamic logic and (2) its extension for dealing with infinite computations. Having the power of expression of these logics in mind, these results can be seen to supply (as corollaries) complete proof methods for the various kinds of correctness of recursive programs.


title: Interpreter Generation Using Tree Pattern Matching

authors:
Christoph M. Hoffmann
Michael J. O'Donnell

abstract: 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 parsers from context-free grammars. The interpreters so generated are exactly faithful to the simple traditional mathematical meaning of the equations-no lattice-theoretic or fixpoint ideas are needed to explain the correspondence. The main technical problem involved is the extension of efficient practical string matching algorithms to trees. We present some new efficient table-driven matching techniques for a large class of trees, and point out unsolved problems in extending this class. We believe that the techniques of this paper form the beginnings of a useful discipline of interpreting, comparable to the existing discipline of parsing.


title: Flow Analysis and Optimization of Lisp-Like Structures

authors:
Neil D. Jones
Steven S. Muchnick

abstract: 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 shapes which an unbounded data object may assume during execution of a LISP-like program, and describe a number of uses to which that information may be put to improve storage allocation in compilers and interpreters for advanced programming languages.We are concerned chiefly with finding, for each program point and variable a finite description of a set of graphs which includes all the shapes of values the variable could assume at that point during the execution of a program. If this set is small or regular in structure, this information can be used to optimize the program's execution, mainly by use of more efficient storage allocation schemes.In the first part we show how to construct from a program without selective updating a tree grammar whose nonterminals generate the desired sets of graphs; in this case they will all be trees. The tree grammars are of a more general form than is usually studied [8, 19], so we show that they may be converted to the usual form. The resulting tree grammar could naturally be viewed as a recursive type definition [11] of the values the variables may assume. Further, standard algorithms may be employed to test for infiniteness, emptiness or linearity of the tree structure.In the second part selective updating is allowed, so an alternate semantics is introduced which more closely resembles traditional LISP implementations, and which is equivalent to the tree model for programs without selective updating. In this model data objects are directed graphs. We devise a finite approximation method which provides enough information to detect cell sharing and cyclic structures whenever they can possibly occur. This information can be used to recognize when the use of garbage collection or of reference counts may be avoided.The work reported in the second part of this paper extends that of Schwartz [17] and Cousot and Cousot [7]. They have developed methods for determining whether the values of two or more variables share cells, while we provide information on the detailed structure of what is shared. The ability to detect cycles is also new. It also extends the work of Kaplan [13], who distinguishes only binary relations among the variables of a program, does not handle cycles, and does not distinguish selectors (so that his analysis applies to nodes representing sets rather than ordered tuples).


title: The Evolution of List-Copying Algorithms

authors:
Stanley Lee
Willem P. de Roever
Susan L. Gerhart

abstract: 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 programs, some precise answers to the question are needed. Over the past decade the various verification methods which have been introduced (inductive assertions, structural induction, least-fixedpoint semantics, etc.) have established many basic principles of program verification (which we define as: establishing that a program text satisfies a given pair of input-output specifications). However, it is no coincidence that most published examples of the application of these methods have dealt with "toy programs" of carefully considered simplicity.Experience indicates that these "first generation" principles, with which one can easily verify a three-line greatest common divisor algorithm, do not directly enable one to verify a 10,000 line operating system (or even a 50 line list-processing algorithm) in complete detail. To verify complex programs, additional techniques of organization, analysis and manipulation are required. (That a similar situation exists in the writing of large, correct programs has long been recognized -- structured programming being one solution.)This paper examines the usefulness of correctness-preserving program transformations (see [6]) in structuring fairly complex correctness proofs. Using our approach one starts with a simple, high-level (or "abstract") algorithm which can be easily verified, then successively refines it by implementing the abstractions of the initial algorithm to obtain various final, detailed algorithms. In Section 2 we introduce the technique by deriving the Deutsch-Schorr-Waite list-marking algorithm [14]. Our main example is the more complex problem of verifying bounded-workspace list-copying algorithms: Section 3 defines the issues, Section 4 presents the key intermediate algorithm in detail and Section 5 considers three of the most complex (published) implementations of list-copying, one of which is discussed in detail. In Section 6 we make some general remarks on program verification and the relevance of our results to the (larger) field of program correctness; Section 7 mentions some related work.


title: String Pattern Matching in Polynomial Time

authors:
Ken C. Liu
Arthur C. Fleck

abstract: 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 the language is organized, the string pattern. This structure together with the associated pattern matching process provide great flexibility. Nevertheless it has been widely recognized in informal terms that the pattern matching process is often grossly inefficient (Ripley & Griswold [1975], Dewar & McCann [1977]) and that the pattern structure is notoriously difficult to explain and use (Ripley & Griswold [1975], Stewart [1975]). Each of these areas of difficulty relates to such things as two modes of operation (quick-full scan), problems with left-recursion, heuristics in the scan, etc. Some difficulties are inherent with string patterns but many are not; we feel the developments described here help to clarify this situation.In section 2 we describe the formal model upon which we base this work. This allows the careful analysis of the variety of sets of strings which may be specified by the patterns which we admit and deduction to be made concerning the possibility/impossibility of algorithms of interest. With SNOBOL4 it has been the case that the careful definition of the meaning of a pattern is in terms of the actions taken by the pattern matching algorithm. This has led to the incorporation of idiosyncrasies of a particular algorithm into the understanding of the pattern structure. This seems akin to using a compiler as the definition of a programming language and we believe it is important to future progress to have other alternatives.In section 3 we point out that the worst-case execution time of the usual SNOBOL pattern matching algorithm is exponential in the length of the subject string, even on some quite simple patterns. We then present an algorithm whose worst-case time is polynomial and that operates on patterns which include a true set complement operator. As side benefits we find that the algorithm is not multi-modal and correctly handles the null string as an alternative and left-recursion.In order to conserve space we will assume throughout this paper that the reader is familiar with the idea of a string pattern in the sense that it is described in Griswold et al. [1971]. Also it is probably necessary that the reader have some general knowledge of the formal languages area.


title: Type Checking in an Imperfect World

abstract: 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 practically useful type prediction algorithm. In Section 2 we introduce a model programing language and in Section 3 define type inference rules for that language. Section 4 presents a type prediction algorithm and Section 5 describes how to apply the results to solve the problems stated in Section 1. Section 6 presents an example of our procedure and demonstrates how previous work does not satisfy all requirements.


title: Process Logic

abstract: 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 | , ; and *. Here we give a complete Gentzen-type axiomatizations for useful combinations of the other modalities. We also indicate how such Gentzen-type axiomatizations lead to deterministic exponential time upper bounds on the complexity of decision procedures for these languages. It remains an open problem how to completely axiomatize the combination of modalities during and preserves.


title: Data Flow Analysis of Communicating Processes

abstract: 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 sequential programs to the analysis of communicating, concurrent processes.


title: Certifying Information Flow Properties of Programs: An Axiomatic Approach

authors:
Richard P. Reitman
Gregory R. Andrews

abstract: Interesting program properties other than functional correctness can be addressed and proved using axiomatic logic. An information flow logic that defines the flow semantics of a parallel programming language is presented. Proofs in this logic can be used to certify programs with respect to information security policies. The flow logic can also be combined with correctness logics to form an even more powerful deductive system.


title: Space-Time Tradeoffs for Linear Recursion

authors:
Sowmitri Swamy
John E. Savage

abstract: A linear recursive procedure is one in which a procedural call can activate at most one other procedural call. When linear recursion cannot be replaced by iteration, it is usually implemented with a stack of size proportional to the depth of recursion. In this paper we analyze implementations of linear recursion which permit large reductions in storage space at the expense of a small increase in computation time. For example, if the depth of recursion is n, storage space can be reduced to √n at the cost of a constant factor increase in running time. The problem is treated by abstracting linear recursion into the pebbling of a simple graph and for this abstraction we exhibit the optimal space-time tradeoffs.


title: Automatic Data Structure Selection in SETL

authors:
Edmond Schonberg
Jacob T. Schwartz
Micha Sharir

abstract: SETL is a very high level programming language supporting set theoretical syntax and semantics. It allows algorithms to be programmed rapidly and succinctly without requiring data structure declarations to be supplied, though such declarations can be manually specified later, without recoding the program, to improve the efficiency of program execution. We describe a new technique for automatic selection of appropriate data representations during compile-time for undeclared, or partially declared programs,and present an efficient data structure selection algorithm, whose complexity is comparable with those of the fastest known general data-flow algorithms of Tarjan [TA2] and Reif [RE].


title: Theoretical and Emperical Studies on Using Program Mutation to Test the Functional Correctness of Programs

authors:
Timothy A. Budd
Richard A. DeMillo
Richard J. Lipton
Frederick G. Sayward

abstract: 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


title: Data Types, Parameters, and Type Checking

authors:
Alan J. Demers
James E. Donahue

abstract: 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-checking" is performed must be carefully considered for modern languages that allow the programmer to define his own data types and allow parameterized types or types as parameters. (Such languages include Alphard [Wulf78], CLU [Liskov77], Euclid [Lampson77] and Russell [Demers79].) These features increase the expressive power of the languages, but also increase the difficulty of type-checking them.In this paper, we describe a treatment of type-checking that makes it possible to do completely static checking with a general parameterization mechanism allowing parameterized types, types as parameters, and even a disciplined form of self-application. Our method defines a calculus of "signatures," where signatures are similar to the "program types" of [Reynolds78]. Each identifier and expression is given a signature, and applications are type-correct when argument and parameter signatures are equivalent under a simple set of signature transformation rules. Below we present the signature calculus of Russell; we also present a semantic justification of this calculus and specify the language constraints necessary for us to justify our purely static approach to type-checking.


title: "Type-Completeness" as a Language Design Principle

abstract: 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 assumptions.A less radical interpretation of the difficulties of language design is that we still do not understand the fundamental principles that should guide our design efforts; the machines we use may limit our results, but our ignorance has far greater effect. As evidence to support this position, we can cite the difficulties of building successors to Algol 60 and Pascal. Both languages have been acclaimed as well-designed, but it has proved extremely difficult to capture just what they "got right." Thus, Hoare has claimed that "Algol 60 was not only a great improvement on its predecessors, but also on nearly all of its successors." [73a] The recent Ada design suggests that the same fate may befall Pascal.In this paper, we expand on an idea of Landin [66] to develop an important principle of programming languages: type-completeness. We argue that application of this principle is an effective tool in understanding problems of programming language design. In particular, type-completeness1. allows us to point out many of the flaws and inconsistencies in existing languages (so we can know what mistakes not to repeat) and2. provides a framework for the design of languages (or language families) that have wide variation in their changeable parts.Below, we present the principle of type-completeness and its ramifications for language design. We then discuss some common examples of incompleteness found in existing Algol-like languages. And we end by presenting the type structure of the type-complete programming language Russell, which has been designed by the authors. As we show, the flexibility provided in Russell by the combination of a small, rich type structure and type-completeness belie Backus's assertion of inherent weakness of vonNeumann languages.


title: An Indeterminate Constructor for Applicative Programming

authors:
Daniel P. Friedman
David S. Wise

abstract: 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 actions of the processes themselves. This means that an indeterminate behavior, never precisely specified by the programmer or by the input, may be shared in the same way that an argument to a function is shared by every use of the corresponding parameter, an ability which is of particular importance to applicative-style programming.


title: On the Temporal Analysis of Fairness

authors:
Dov M. Gabbay
Amir Pnueli
Saharon Shelah
Jonathan Stavi

abstract: 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 discussed. It is shown that with the addition of this operator the temporal language becomes expressively complete. Then, two deductive systems DX and DUX are proved to be complete for the languages without and with the new operator respectively.


title: Formal Specification as a Design Tool

authors:
John V. Guttag
James J. Horning

abstract: 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 light. In this paper we outline a specification language combining algebraic axioms and predicate transformers, present part of a non-trivial example (the specification of a high-level interface to a display), and finally discuss the analysis of this specification.


title: Qualified Data Flow Problems

authors:
L. Howard Holley
Barry K. Rosen

abstract: 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 information can be obtained by considering a recursive set of paths that is large enough to include all possible paths but small enough to exclude many of the impossible ones. This paper presents a simple uniform methodology for sharpening data flow information by considering certain recursive path sets of practical importance. Associated with each control flow arc there is a relation on a finite set Q. The paths that qualify to be considered are (essentially) those for which the composition of the relations encountered is nonempty. For example, Q might be the set of all assignments of values to each of several bit variables used by a program to remember some facts about the past and branch accordingly in the future. Given any data flow problem together with qualifying relations on Q associated with the control flow arcs, we construct a new problem. Considering all paths in the new problem is equivalent to considering only qualifying paths in the old one. Preliminary experiments (with a small set of real programs) indicate that qualified analysis is feasible and substantially more informative than ordinary analysis. The methodology also has a beneficial feedback effect on the delicate task of passing from programs to meaningful data flow analysis problems. Even when all paths qualify, unusually sharp information can be obtained by passing from programs to problems in ways suggested by our theorems.


title: Efficient Algorithms for Structural Similarity of Grammars

authors:
Harry B. Hunt III
Daniel J. Rosenkrantz

abstract: 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) testing, for a reduced context-free grammar G and a structurally unambiguous grammar H, if G is Reynolds covered by H or if there is an on to homomorphisem from G to H.Related complexity results are presented for several problems for the regular grammars, program schemes, and monadic program schemes.


title: Final Data Tye Specifications: A New Data Type Specification Method

abstract: 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 the mathematical properties of final data types characterize abstractness on the semantic level.Examples are given to show that final data type specifications are easy to construct and use.