title: Expressiveness of the Operation Set of a Data Abstraction

authors:
Deepak Kapur
Mandayam K. Srivas

abstract: In a strongly typed system supporting user defined data abstractions, the designer of a data abstraction ought to be careful in choosing the operations for the abstraction. If the operation set chosen is not expressive enough, it might be impossible or inconvenient to implement certain useful functions on the values of the data abstraction. In this paper, we characterize the expressive power of the operation set by defining two properties for data abstractions - expressive completeness and expressive richness. The operation set of an expressively complete data abstraction is adequate enough to implement all computable functions on its values. An expressively rich data abstraction is expressively complete with an operation set that is rich enough to conveniently extract from a value, all relevant information required to reconstruct the value from scratch. Practical applications of the properties of expressiveness introduced are also discussed.


venue: popl

title: Analysis of Simple Programs Over Different Sets of Primitives

abstract: It is well known that most questions of interest about the behavior of programs--such as equivalence, halting, optimization, and other problems--are undecidable. On the other hand, it is possible to make some or all of these questions decidable by introducing appropriate restrictions on the programming language under consideration. And once such restrictions are made, the next step is to ask how hard it is to solve these problems for programming languages for which they are decidable.This analysis of programming languages has been undertaken by others, in particular by Jones and Muchnick [4], who choose to restrict their programs to operate over finite memory. Our approach starts from the language of loop-programs, as defined by Meyer and Ritchie [1], in which we in fact allow more general arithmetical operations. Unlike Jones and Muchnick, we do not place any restriction on memory here; instead, we (primarily) restrict our attention to loop-programs without nested loops.


title: An Overview of the Summer Programming Language

abstract: The language SUMMER is intended for the solution of problems in text processing and string manipulation. The language consists of a small kernel which supports success-directed evaluation, control structures, recovery caches and a data abstraction mechanism. It is shown how this kernel can be extended to support simultaneous pattern matching in arbitrary domains.


title: "Sometime" is Sometimes "Not Never" - On the Temporal Logic of Programs

abstract: Pnueli [15] has recently introduced the idea of using temporal logic [18] as the logical basis for proving correctness properties of concurrent programs. This has permitted an elegant unifying formulation of previous proof methods. In this paper, we attempt to clarify the logical foundations of the application of temporal logic to concurrent programs. In doing so, we will also clarify the relation between concurrency and nondeterminism, and identify some problems for further research.In this paper, we consider logics containing the temporal operators "henceforth" (or "always") and "eventually" (or "sometime"). We define the semantics of such a temporal logic in terms of an underlying model that abstracts the fundamental concepts common to almost all the models of computation which have been used. We are concerned mainly with the semantics of temporal logic, and will not discuss in any detail the actual rules for deducing theorems.We will describe two different temporal logics for reasoning about a computational model. The same formulas appear in both logics, but they are interpreted differently. The two interpretations correspond to two different ways of viewing time: as a continually branching set of possibilities, or as a single linear sequence of actual events. The temporal concepts of "sometime" and "not never" ("not always not") are equivalent in the theory of linear time, but not in the theory of branching time -- hence, our title. We will argue that the logic of linear time is better for reasoning about concurrent programs, and the logic of branching time is better for reasoning about nondeterministic programs.The logic of linear time was used by Pnueli in [15], while the logic of branching time seems to be the one used by most computer scientists for reasoning about temporal concepts. We have found this to cause some confusion among our colleagues, so one of our goals has been to clarify the formal foundations of Pnueli's work.The following section gives an intuitive discussion of temporal logic, and Section 3 formally defines the semantics of the two temporal logics. In Section 4, we prove that the two temporal logics are not equivalent, and discuss their differences. Section 5 discusses the problems of validity and completeness for the temporal logics. In Section 6, we show that there are some important properties of the computational model that cannot be expressed with the temporal operators "henceforth" and "eventually", and define more general operators.


title: Synchronous Schemes and Their Decision Problems

authors:
Zohar Manna
Amir Pnueli

abstract: A class of schemes called synchronous schemes is defined. A synchronous scheme can have several variables, but all the active ones are required to keep a synchronized rate of computation as measured by the height of their respective Herbrand values. A "reset" statement, which causes all the variables to restart a new computation, is admitted. It is shown that equivalence, convergence, and other properties are decidable for schemes in this class. The class of synchronous schemes contains, as special cases, the known decidable classes of Ianov schemes, one-variable schemes with resets, and progressive schemes.


title: Axiomatic Definitions of Programming Languages: A Theoretical Assessment

authors:
Albert R. Meyer
Joseph Y. Halpern

abstract: A precise definition is given of how partial correctness or termination assertions serve to specify the semantics of classes of program schemes. Assertions involving only formulas of first order predicate calculus are proved capable of specifying program scheme semantics, and effective axiom systems for deriving such assertions are described. Such axiomatic specifications are possible despite the limited expressive power of predicate calculus.


title: Experience with an Applicative String Processing Language

authors:
James H. Morris Jr.
Eric Schmidt
Philip Wadler

abstract: Experience using and implementing the language Poplar is described. The major conclusions are: Applicative programming can be made more natural through the use of built-in iterative operators and post-fix notation. Clever evaluation strategies, such as lazy evaluation, can make applicative programming more computationally efficient. Pattern matching can be performed in an applicative framework. Many problems remain.


title: On Proving Inductive Properties of Abstract Data Types

abstract: The equational axioms of an algebraic specification of a data type (such as finite sequences) often can be formed into a convergent set of rewrite rules; i.e. such that all sequences of rewrites are finite and uniquely terminating. If one adds a rewrite rule corresponding to a data type property whose proof requires induction (such as associativity of sequence concatenation), convergence may be destroyed, but often can be restored by using the Knuth-Bendix algorithm to generate additional rules. A convergent set of rules thus obtained can be used as a decision procedure for the equational theory for the axioms plus the property added. This fact, combined with a "full specification" property of axiomatizations, leads to a new method of proof of inductive properties--not requiring the explicit invocation of an inductive rule of inference.


title: Propositional Logics of Programs: Systems, Models, and Complexity

abstract: We indicate below the various results in this paper and the sections where these results are fully described. δ1 is introductory).(δ2). The partial correctness assertion (PCA) A{α}B is expressed in PDL in the form A → [α]B. We shall consider the question of when a given finite set of PCAs implies another and give optimal complexity bounds. We also give other results of an algebraic nature.(δ3). DPDL is less well understood than PDL since the filtration technique of F-L that applies to the latter falls for the former. We point out a translation from PDL to DPDL which leads to a lower bound for the latter.(δ4). What do models of PDL look like? We show the existence of canonical and universal models and show how an infinite model can be related to its F-L factors.


title: On Specifying Verifiers

abstract: The goal of automatic program verification is to prove programs correct formally. We argue that the existing notions of formal proof are too syntactic and as such too intimately bound up with details of low-level computation. We propose a more semantic notion of formal proof which nevertheless pays due respect to the problem of effectiveness in proof checking. Such a notion supplies a more practical basis for the specification of verifiers than do extant approaches. In particular the problem of constructing verifiers according to our approach is reduced entirely to routine development and implementation of decision methods, while permitting shorter proofs and yet remaining easy to develop proofs with.


title: A High-Level Approach to Computer Document Formatting

abstract: The very best document-formatting system is a good secretary. He can be given scrawled handwritten text in no particular format, and without further instruction produce a flawless finished document. Nevertheless, we believe that document formatting should be done by computers, because so much of it is the tedium that computers handle so well. Existing computer document formatting programs have met with some success; indeed, most computer systems offer some sort of text formatting capability. These programs are often difficult to use, and are almost invariably tied to a particular kind of printing device.The document-formatting language Scribe was designed to provide a simple, portable language in which document formatting could be specified; the Scribe compiler was written to process that language into finished documents. In following sections we describe the design goals, the implementation, and report on experience with the completed system.


title: A Dynamic Logic of Multiprocessing with Incomplete Information

authors:
John H. Reif
Gary L. Peterson

abstract: A crucial property of distributed multiprocessing systems is the lack of complete information by any given process about the states of other processes. The contribution of this paper is a fundamental modal logic, MPL, for multiprocessing with incomplete information. (Section 1.5 gives an informal introduction to MPL; the formal definitions are in Section 2.)By way of this logic, we develop a solid (practical and theoretical) correspondence between distributed multiprocessing and multiplayer games of incomplete information.Fischer and Ladner, [1979] have shown a logspace reduction from the outcome problem for two person games of perfect information to satisfiability of formulas in their propositional dynamic logic (PDL). We provide in Section 3 a log-space reduction from the outcome problem for multiplayer games of incomplete information to satisfiability of formulas in our logic MPL. Although in general satisfiability in out logic is undecidable, the satisfiability problem of formulae with hierarchical visibility structure is shown decidable (using the methods for solving hierarchical games developed in Reif [1979] and Peterson and Reif [1979], and also the model theoretic techniques of Fischer and Ladner [1979] and Pratt [1979b]).At a more practical level, we argue that the game-like semantics of our logic provides a robust paradigm in which to view distributed multiprocessing problems. We apply our logic to describe total correctness properties of multi-process programs with shared variables as well as communicating processes with "handshake"-type message passing.


title: A Case Study in Specifying the Semantics of a Programming Language

abstract: On and off over the period of about a year I have worked on a semantic specification for the C programming language My objective was to construct a readable and precise specification of C, aimed at compiler writers, maintainers, and language pundits. This paper is a report on the project.


title: Analysis of Pointer Rotation

abstract: Pointer manipulation is one of the trickiest operations in programming and is a major source of programming errors. A great deal of research effort has been dedicated to making programs with pointers more reliable. In this paper we will present pointer operations which reduce conceptual difficulties when writing pointer programs, and increase reliability of programs. We will analyze theoretically as well as empirically why these operations are more convenient. Finally, we will define the safety of rotations, and show that it is decidable to check whether the rotation is safe and also show that it is a good measure of the correctness of programs. (That is, if the rotation is safe it is highly probable that the program is correct, and if it is unsafe it is highly probable that the program is incorrect.)Probably the most successful effort to eliminate difficulties associated with pointer manipulation is the invention of abstract data types and the use of implementation modules. Pointers are often used to implement complex data structures, which in turn represent abstract data types. We can textually localize relevant pointer manipulations using abstract data types. Thus, we can easily check correctness of pointer programs. This approach is successful when the structure of abstract data types is simple, or efficiency is not seriously required. However, programs like garbage collection, list marking and copying, and balanced tree manipulations have not been well specified by abstract types.The approach taken in this paper is complementary to abstract data types, and makes programs like list marking and copying more reliable and easy to write. The idea behind this approach is to introduce higher-level pointer manipulation primitives instead of pointer assignments. Since most pointer assignments do not appear isolated, we can group several assignments together and replace them by one of these new primitives. We also show some theoretical evidence why these operations are nicer.Two primitives are introduced in this paper. One is the n-way pointer rotation, which is defined as being equivalent to the following procedure:Rotate: procedure(var x1, x2, … , xn:T) = begin var w:T; w:=x1; x1:=x2; … ;xn:=w endwhere all the locations of arguments x1, x2, … , xn are distinct. The other operation is n-way pointer slide, which is as powerful as pointer assignment yet keeps the elegance of rotation.Section 2 of this paper reviews previous work related to this subject. We give definitions of pointer operations analyzed in this paper in section 3. Using these operations, Deutsch-Schorr-Waite algorithm is rewritten in section 4. In section 5 we analyze pointer rotations extensively and obtain several properties which are not attainable by ordinary pointer assignments. In section 6 we define the safety of pointer rotation when applied to linear list and trees. Then, we extend this definition to arbitrary pointer data structures and show a decision procedure to check safety. In section 7 we show two examples, list marking and list copying programs written using rotations and slides. We examine how we can directly code the algorithms using these operations and safety checking algorithms are useful.


title: Prime Subprogram Parsing of a Program

abstract: A parsing method based on the triconnected decomposition of a biconnected graph is presented. The parsing algorithm runs in linear time and handles a large class of flow graphs. The applications of this algorithm to flow analysis and to the automatic structuring of programs are discussed.


title: Interprocedural Data Flow Analysis in the Presence of Pointers, Procedure Variables and Label Variables

abstract: Interprocedural data flow analysis is complicated by the use of procedure and label variables in programs and by the presence of aliasing among variables. In this paper we present an algorithm for computing possible values for procedure and label variables, thus providing a call graph and a control flow graph. The algorithm also computes the possible aliasing relationships in the program being analyzed.We assume that control flow information is not available to the algorithm; hence, this type of analysis may be termed "flow-free analysis." Given this assumption, we demonstrate the correctness of the algorithm, in the sense that the information it produces is conservative, and show that it is as precise as possible in certain cases. We also show that the problem of determining possible values for procedure variables is P-space hard. This fact indicates that any algorithm which is precise in all cases must also run very slowly for some programs.


title: A Program Development Tool

authors:
Cyril N. Alberga
Allen L. Brown
George B. Leeman Jr.
Martin Mikelsons
Mark N. Wegman

abstract: In this paper we describe how we have combined a number of tools (most of which understand a particular programming language) into a single system to aid in the reading, writing, and running of programs. We discuss the efficacy and the structure of our system. For the last two years the system has been used to build itself; it currently consists of 500 kilobytes of machine code (25,000 lines of LISP/370 code) and approximately one hundred commands with large numbers of options. We will describe some of the experience we have gained in evolving this system. We first indicate the system components which users have found most important; some of the tools described here are new in the literature. Second, we emphasize how these tools form a synergistic union, and we illustrate this point with a number of examples. Third, we illustrate the use of various system commands in the development of a simple program. Fourth, we discuss the implementation of the system components and indicate how some of them have been generalized.


title: The Temporal Logic of Branching Time

authors:
Mordechai Ben-Ari
Zohar Manna
Amir Pnueli

abstract: A temporal language and system are presented which are based on branching time structure. By the introduction of symmetrically dual sets of temporal operators, it is possible to discuss properties which hold either along one path or along all paths. Consequently it is possible to express in this system all the properties that were previously expressible in linear time or branching time systems. We present an exponential decision procedure for satisfiability in the language based on tableaux methods, and a complete deduction system. As associated temporal semantics is illustrated for both structured and graph representation of programs.


title: Formal Program Testing

abstract: This paper proposes a practical alternative to program verification -- called formal program testing -- with similar, but less ambitious goals. Like a program verifier, a formal testing system takes a program annotated with formal specifications as input, generates the corresponding verification conditions, and passes them through a simplifier. After the simplification step, however, a formal testing system simply evaluates the verification conditions on a representative set of test data instead of trying to prove them. Formal testing provides strong evidence that a program is correct, but does not guarantee it. The strength of the evidence depends on the adequacy of the test data.


title: Paths: An Abstract Alternative to Pointers

authors:
Robert Cartwright
Robert Hood
Philip Mathews

abstract: This paper introduces the path, a new programming language construct designed to supplant the use of pointers to access and destructively update recursive data structures. In contrast to the complex semantics and proof rules for pointers, the semantics and proof rules for paths are simple and abstract. In fact, they are easily formalized within a first-order theory of recursive data objects analogous to first-order number theory. We present a number of sample programs, including implementations of queues and binary trees, utilizing the new construct and prove that they are correct.


title: Programming Primitives for Database Languages

abstract: This paper examines a number of programming primitives in query languages for relational databases. The basic framework is a language based on relational algebra, whose variables take relations as values. The primitives considered are (i) looping, (ii) counters, (iii) generic (or unranked) variables, (iv) equality, (v) bounded looping (which corresponds to counting the number of tuples in a relation), and (vi) isomorphism class (which corresponds to knowing the isomorphism class of the data base). A comparison diagram is given relating all combinations of these six primitives, and several of the resulting classes of queries are characterized by their complexity or algebraic properties. It is shown, for example, that equality cannot be simulated using all the other primitives, that generic variables (with loops) cannot be simulated with only ranked variables and all the other primitives, and that with bounded loops one can determine the isomorphism class of the database when generic variables are allowed, but not otherwise.


title: Paging as a "Language Processing" Task

abstract: This paper examines "language processing" approach to paging where the of the programming language compiler or interpreter is responsible for generating the necessary control code for the page management of a program. We explore this idea for APL and describe an approach to incorporating in a program the necessary paging functions. The semantics of APL computation are examined to observe how paging operations can be incorporated into the computation. We discuss a model of data access in APL that exhibits storage use for both scalar and page references. A data structure that encodes the logical use of data from an array is introduced. We find that ordering computations efficiently and computing paging needs can be determined by simple transformations on this structure. This analysis leads us to an efficient method for paging an APL computation. Our approach builds on previous studies for efficiently executing APL.


title: Incremental Evaluation for Attribute Grammars with Application to Syntax-Directed Editors

authors:
Alan J. Demers
Thomas W. Reps
Tim Teitelbaum

abstract: A syntax-directed editor is a tool for structured program development. Such an editor can enforce syntactic correctness incrementally by restricting editing operations to legitimate modifications of the program's context-free derivation tree. However, not all language features can be described by the context-free formalism. To build editors that enforce non-context-free correctness, a more powerful specification technique is needed. In this paper we discuss the advantages of attribute grammars as a specification technique for a syntax-directed editing system. We also present an efficient algorithm for incrementally evaluating attributes as a program tree is derived.


title: Axiomatic Definitions of Programming Languages, II

authors:
Joseph Y. Halpern
Albert R. Meyer

abstract: Sufficient conditions are given for partial correctness assertions to determine the input-output semantics of quite general classes of programming languages. This determination cannot be unique unless states which are indistinguishable by predicates in the assertions are identified. Even when indistinguishable states are identified, partial correctness assertions may not suffice to determine program semantics.


title: Position Paper on Optimizing Compilers

abstract: No abstract available.


title: Program Optimization and Exception Handling

abstract: Optimization of programs that may contain exception handling facilities requires new techniques. Program optimizations that do not account for exception handling facilities may incorrectly transform a procedure that can raise an exception, producing different results from the unoptimized version. Restricted exception handling mechanisms that allow optimization are discussed. Data flow equations for determining the effects of exception handling are presented.


title: Verification of Attribute Grammars

authors:
Takuya Katayama
Yutaka Hoshino

abstract: Verification of attribute grammar is discussed. As is widely recognized, attribute grammar of Knuth [8] is a very convenient device to describe semantics of programming languages, especially in automating compiler construction. Many efforts have been made to obtain efficient evaluators for attribute grammar [1,3,4,5,7,10] so that efficient compilers may be produced from the semantic specifications written in the attribute grammar.There is another important problem about the semantic specifications. This is how to verify the correctness of the specification and is essential in ascertaining the correctness of produced compilers. In contrast with the evaluation problem, this has not been studied well and only a few partial results have been reported up to now [2,9].In this paper we propose a verification procedure for proving the correctness of attribute grammar, which is applicable to the wide class of attribute grammars called absolutely noncircular ones [7]. Our method can be extended to accept any noncircular attribute grammar since it is shown that any noncircular attribute grammar is transformed into an equivalent absolutely noncircular one [5].Our verification procedure utilizes dependency relations among attributes and verification is performed by induction based on this order relation, according to which attributes are evaluated. This procedure consists of (1) assigning assertions to relevant pairs of a nonterminal symbol and a parallelly evaluable subset of its attributes, (2) generating a set of verification conditions for each production rule with the aid of dependency graph of the rule and (3) proving the verification conditions. Of course, verification is performed production-rule-wise.Our method can accept attribute grammars which contain both synthesized and inherited attributes and handle them in a well-formed way. This contrasts to the previous works where only the synthesized case is considered [2] or there seems no general and formal descriptions about how to verify general attribute grammars [9].In this paper we first give necessary definitions and notations for attribute grammar and then propose a verification procedure to prove its correctness. After giving some examples of verification, we establish consistency and completeness of our procedure.


title: Dependence Graphs and Compiler Optimizations

authors:
David J. Kuck
Robert H. Kuhn
David A. Padua
Bruce Leasure
Michael Wolfe

abstract: Dependence graphs can be used as a vehicle for formulating and implementing compiler optimizations. This paper defines such graphs and discusses two kinds of transformations. The first are simple rewriting transformations that remove dependence arcs. The second are abstraction transformations that deal more globally with a dependence graph. These transformations have been implemented and applied to several different types of high-speed architectures.


title: On the Advantages of Free Choice: A Symmetric and Fully Distributed Solution to the Dining Philosophers Problem

authors:
Daniel Lehmann
Michael O. Rabin

abstract: It is shown that distributed systems of probabilistic processors are essentially more powerful than distributed systems of deterministic processors, i.e., there are certain useful behaviors that can be realized only by the former. This is demonstrated on the dining philosophers problem. It is shown that, under certain natural hypotheses, there is no way the philosophers can be programmed (in a deterministic fashion) so as to guarantee the absence of deadlock (general starvation). On the other hand, if the philosophers are given some freedom of choice one may program them to guarantee that every hungry philosopher will eat (with probability one) under any circumstances (even an adversary scheduling). The solution proposed here is fully distributed and does not involve any central memory or any process with which every philosopher can communicate.


title: Carrier Arrays: An Idiom-Preserving Extension to APL

abstract: The idiomatic APL programming style is limited by the constraints of a rectangular, homogeneous array as a data structure. Non-scalar data is difficult to represent and manipulate, and the non-scalar APL functions have no uniform extension to higher rank arrays. The carrier array is an extension to APL which addresses these limitations while preserving the economical APL style. A carrier array is a ragged array with an associated partition which allows functions to be applied to subarrays in parallel. The primitive functions are given base definitions on scalars and vectors, and they are extended to higher rank arrays by uniform application mechanisms. Carrier arrays also allow the last dimensions of an array to be treated as a single datum; the primitive functions are given extended definitions on scalars and vectors of this non-scalar data.This paper defines the carrier array and gives the accompanying changes to the definitions of the APL primitive functions. Examples of programming with carrier arrays are presented, and implementation issues are discussed.


title: A Precise Interprocedural Data Flow Algorithm

abstract: Data flow analysis is well understood at the intra-procedural level and efficient algorithms are available. When inter-procedural mechanisms such as recursion, procedure nesting, and pass-by-reference aliasing are introduced, the data flow problems become much more difficult. The avail, live, and must-summary data flow problems are shown to be NP-complete in the presence of aliasing. However, an algorithm is presented with O(SET*EDGE) time performance where EDGE is the size of the program's flow graph and SET is a possible exponential number which reflects the number of aliasing patterns of the program. It is argued that in practice SET is small and on the order of the number of variables of the program.


title: Making the World Safe for Garbage Collection

abstract: This paper describes the formal specifications of garbage collection in the programming language Cedar Mesa. They were developed as part of the process of identifying a safe subset of Mesa for which garbage collection was possible. The purpose of the specifications was to provide a precise definition of safety, along with criteria for checking the safety of proposed language features. Thus the specifications had to characterize the "invisibility" of the collector, as well as describe the services it provides. A beneficial effect of the specification effort was that the process of constructing the specifications led to a number of discoveries that improved the quality of the language.


title: Program Verification Based on Denotational Semantics

abstract: A theory of partial correctness proofs is formulated in Scott's logic computable junctions. This theory allows mechanical construction of verification condition solely on the basis of a denotational language definition. Extensionally these conditions, the resulting proofs, and the required program augmentation are similar to those of Hoare style proofs; conventional input, output, and invariant assertions in a first order assertion language are required. The theory applies to almost any sequential language defined by a continuation semantics; for example, there are no restrictions on aliasing or side-effects. Aspects of static semantics,such as type and declaration constraints, which are expressed in the denotational definition are validated as part of the verification condition generation process.


title: Program Logic Without Binding is Decidable

abstract: When the "binding mechanisms" of assignment, quantification, and procedure definition are removed from a conventional first order total correctness logic of programs, the remaining logical system is decidable in time approximately one exponential in the length of the input. This system is maximal in the sense that the presence of any one of the three binding mechanisms would make it undecidable. Such a decision procedure can play a central role in the construction of program verifiers based on decision methods.


title: Modeling of Problem Domains for Driving Program Development Systems

authors:
Jay Ramanathan
Charley J. Shubra

abstract: Article Free Access Share on Modeling of problem domains for driving program development systems Authors: J. Ramanathan The Ohio State University, Columbus, Ohio The Ohio State University, Columbus, OhioView Profile , C. J. Shubra The Ohio State University, Columbus, Ohio The Ohio State University, Columbus, OhioView Profile Authors Info & Claims POPL '81: Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1981 Pages 28–40https://doi.org/10.1145/567532.567535Online:26 January 1981Publication History 1citation183DownloadsMetricsTotal Citations1Total Downloads183Last 12 Months2Last 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 AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Linear Cost is Sometimes Quadratic

abstract: In analysis of programs and many other kinds of computation, algorithms are commonly written to have an input P and an output Q, where both P and Q are large and complicated objects. For example, P might be a routing problem and Q might be a solution to P. Although documented and discussed in this exhaustive style, algorithms are sometimes intended for use in contexts with two departures from the one-time analysis of an entire new input. First, the current value of P is the result of a small change to a previous value of P. We want to update the results of the previous analysis without redoing all of the work. Second, accurate information is only wanted in some designated portion of the large output Q. Possibly inaccurate information may appear elsewhere in Q. We want the analysis to be demand-driven: accurate where accuracy is demanded, but not burdened by the cost of providing much more than is demanded. This paper studies demand-driven algorithms capable of updating without extensive reanalysls. Such algorithms are called incremental, in contrast with the one-time analysis of an entire new input contemplated by exhaustive algorithms. In some cases, it is shown that an exhaustive algorithm can be easily recast in an efficient incremental style. Other algorithms for the same problem may be much less amenable to incremental use. It is shown that traditional exhaustive computational complexity bounds are poor predictors of incremental performance. The main examples are taken from global data flow analysis.


title: Program Improvement by Internal Specialization

abstract: We investigate the specialization of programs by means of program transformation techniques. There are two goals of this investigation: the construction of program synthesis tools, and a better understanding of the development of algorithms.By extending an ordinary language of recursion equations to include a generalized procedure construct (the expression procedure), our ability to manipulate programs in that language is greatly enhanced. The expression procedure provides a means of expressing information not just about the properties of individual program elements, but also about the way they relate to each other.A set of four operations for transforming programs in this extended language is presented. These operations, unlike the transformation rules of Burstall and Darlington and of Manna and Waldinger, preserve the strong equivalence of programs.This set of operations forms the basis of a general-purpose specialization technique for recursive programs. The practical value of this technique has been demonstrated in the systematic development of many programs, including several context-free parsing algorithms. We outline here the development of Earley's algorithm by specialization.This paper is an informal exposition of part of the results of the author's Ph.D. thesis [Scherlis80].


title: Inferring Types in Smalltalk

abstract: Smalltalk is an object-oriented language designed and implemented by the Learning Research (Group of the Xerox Palo Alto Research Center [2, 5, 14]. Some features of this language are: abstract data classes, information inheritance by a superclass-subclass mechanism, message passing semantics, extremely late binding no type declarations, and automatic storage management. Experience has shown that large complex systems can be written in Smalltalk in quite a short period of time; it is also used to teach programming to children quite effectively. Object-oriented languages like Smalltalk have begun to be accepted as friendly languages for novice programmers on personal computers.


title: A Logic for Expressions with Side-Effects

abstract: This paper presents a simple programming logic LES, which is particularly well suited for reasoning about so-called expression languages, i.e. languages that incorporate imperative features into expressions rather than distinguishing between expressions and statements. An axiomatization of a simple programming language is presented using this formalism. It is shown that this axiomatization is relatively complete, roughly in the sense of [Coo 76].


title: A Type Declaration and Inference System for Smalltalk

authors:
Alan Borning
Daniel H. H. Ingalls

abstract: An experimental system for declaring and inferring type in Smalltalk is described. (In the current Smalltalk language, the programmer supplies no type declarations.) The system provides the benefits of type declaration in regard to compile-time checking and documentation, while still retaining Smalltalk's flexibility. A type hierarchy, which is integrated with the existing Smalltalk class hierarchy, allows one type to inherit the traits of another type. A type may also have parameters, which are in turn other types.


title: On Effective Axiomatizations of Hoare Logics

authors:
Edmund M. Clarke
Steven M. German
Joseph Y. Halpern

abstract: For a wide class of programming languages P and expressive interpretations I, we show that there exist sound and relatively complete Hoare-like logics for both partial correctness and termination assertions. In fact, under mild assumptions on P and I, we show that the assertions true for P in I are uniformly decidable in the theory of I (Th(I)) iff the halting problem for P is decidable for finite interpretations. Moreover termination assertions are uniformly r.e. in Th(I) even if the halting problem for P is not decidable for finite interpretations. Since total correctness assertions coincide with termination assertions for deterministic programming languages, this last result unexpectedly suggests that the class of languages with good axiom systems for total correctness may be wider than for partial correctness.


title: On the Expressive Power of Query Languages for Relational Databases

abstract: The query languages used in relational database systems are a special class of programming languages. The majority, based on first-order logic, lend themselves to analysis using formal methods. First, we provide a definition of relational query languages and their expressive power. We prove some general results and show that only a proper subset of first-order logic formulas may be used as a practical query language. We characterize this subset in both semantic and syntactic terms. We then analyze the expressive power of several real query languages, including languages based on the relational calculus, languages with set operators and aggregate functions, and procedural query languages.Since the partial ordering "is more expressive than" determines a lattice among relational query languages, the results of the paper may be viewed as determining some of the structure of this lattice. We conclude with some applications of the results to the optimization problem for query processing.


title: On the Ability of Structures to Store and Access Information

abstract: Article On the ability of structures to store and access information Share on Author: Adrienne Critcher The University of Iowa, Iowa City, Iowa The University of Iowa, Iowa City, IowaView Profile Authors Info & Claims POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1982 Pages 366–378https://doi.org/10.1145/582153.582191Online:25 January 1982Publication History 1citation177DownloadsMetricsTotal Citations1Total Downloads177Last 12 Months2Last 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: Principal Type-Schemes for Functional Programs

authors:
Luís Damas
Robin Milner

abstract: the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of its publication and date appear, and notice is given


title: Eliminating Redundant Object Code

authors:
Jack W. Davidson
Christopher W. Fraser

abstract: Compilers usually eliminate common subexpressions in intermediate code, not object code. This reduces machine-dependence but misses the machine-dependent common subexpressions introduced by the last phases of code expansion. This paper describes a machine-independent procedure for eliminating machine-specific common subexpressions. It also identifies dead variables, defines windows for a companion peephole optimizer, and forms the basis of a retargetable register allocator. Its techniques for handling machine-specific data should generalize to other optimizations as well.


title: Experience with an Attribute Grammar-Based Compiler

abstract: Experience writing a production compiler based on an attribute grammar is related. The compiler is Intel Corporation's Pascal-86 compiler which runs on a microcomputer-based system. An attribute grammar was written describing semantic analysis, storage allocation and translation to intermediate code. Attribute evaluation is done in two alternating passes [J] and the program tree is kept in intermediate files on disk. Various techniques for optimizing the evaluator were tried. Their success is reported and compared with other ideas from the literature.


title: Extended Naming Conventions for Communicating Processes

abstract: We present two extensions of Communicating Sequential Processes [HO78]: computed communication targets and unspecified communication targets, as well as corresponding extensions to the system of cooperating proofs [AFR80] for verifying distributed programs. These extensions are important for the natural expressibility of many distributed programs. Examples of the use of these extensions are discussed and verified.


title: Description-Driven Code Generation using Attribute Grammars

authors:
Mahadevan Ganapathi
Charles N. Fischer

abstract: The instruction-set of a target architecture is represented as a set of attribute-grammar productions. A code generator is obtained automatically for any compiler using attributed parsing techniques. A compiler built on this model can automatically perform most popular machine-dependent optimizations, including peephole optimizations. The code generator is also easily retargetable to different machine architectures.


title: Semantics and Correctness of a Query Language Translation

authors:
E. Gansner
Joseph R. Horgan
Chandra M. R. Kintala
D. J. Moore
Pamela Surko

abstract: This paper proves the correctness of a translation from HISEL, a relational database query language, to HI, a hierarchical query language.The four components of Morris' [7] program are established. Appropriate semantics for the two languages are defined. A translation function is defined and an L-attributed grammar capturing the translation function is exhibited. The transformation of database trees into database relations is specified.


title: Automatic Generation of Machine Specific Code Optimizers

abstract: Article Free Access Share on Automatic generation of machine specific code optimizers Author: Robert Giegerich Institut für Informatik Technische Universität München West Germany Institut für Informatik Technische Universität München West GermanyView Profile Authors Info & Claims POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1982 Pages 75–81https://doi.org/10.1145/582153.582162Online:25 January 1982Publication History 6citation236DownloadsMetricsTotal Citations6Total Downloads236Last 12 Months10Last 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: Modular Verification of Concurrent Programs

authors:
Brent Hailpern
Susan S. Owicki

abstract: Verifying concurrent systems can be difficult because of the complex interactions possible between system components. In this paper, we propose a technique to simplify the task: modular composition of sequential proofs. We model a parallel program as a set of modules that interact by procedure calls. The properties of each module are proved using a sequential-program verification technique. If the modules satisfy a set of constraints presented in this paper, we may compose the modules into a system and the properties of the modules into properties of the system. The constraints ensure that the specifications are robust for each module where they are defined or used, in the sense that they are unaffected by current actions of other modules. A specification can be guaranteed robust for module m by restricting it to local variables of m, or by using monotonic predicates, which once true remain true forever. Our technique can be used to prove safety and liveness properties of parallel programs---the liveness properties are specified using temporal logic.


title: Termination of Probabilistic Concurrent Programs

authors:
Sergiu Hart
Micha Sharir
Amir Pnueli

abstract: The asynchronous execution behavior of several concurrent processes, which may use randomization, is studied. Viewing each process as a discrete Markov chain over the set of common execution states, we give necessary and sufficient conditions for the processes to converge almost surely to a given set of goal states, under any fair, but otherwise arbitrary schedule, provided that the state space is finite. (These conditions can be checked mechanically.) An interesting feature of the proof method is that it depends only on the topology of the transitions and not on the actual values of the probabilities. We also show that in our model synchronization protocols that use randomization are in certain cases no more powerful than deterministic protocols. This is demonstrated by (a) Proving lower bounds on the size of a shared variable necessary to ensure mutual exlusion and lockout-free behavior of the protocol; and (b) Showing that no fully symmetric 'randomized' protocol can ensure mutual exclusion and freedom from lockout.


title: Code Generation and Reorganization in the Presence of Pipeline Constraints

authors:
John L. Hennessy
Thomas R. Gross

abstract: Pipeline interlocks are used in a pipelined architecture to prevent the execution of a machine instruction before its operands are available. An alternative to this complex piece of hardware is to rearrange the instructions at compile-time to avoid pipeline interlocks. This problem, called code reorganization, is studied. The basic problem of reorganization of machine level instructions at compile-time is shown to be NP-complete. A heuristic algorithm is proposed and its properties and effectiveness are explored. The impact of code reorganization techniques on the rest of a compiler system are discussed.


title: Completion Semantics, Interpreter Generation

authors:
Martin C. Henson
Raymond Turner


title: Building Friendly Parsers

authors:
Fahimeh Jalili
Jean H. Gallier

abstract: An essential part of any interactive programming development system is an incremental parser capable of error recovery. This paper presents a general incremental parser for LR(1) grammars allowing several/any form of modifications in the input program. The parser is suplemented with error recovery routines using an error automaton. Errors can be corrected automatically by recovery routines, or by the user at his request.


title: Non-Syntactic Attribute Flow in Language Based Editors

authors:
Gregory F. Johnson
Charles N. Fischer

abstract: Article Free Access Share on Non-syntactic attribute flow in language based editors Authors: Gregory F. Johnson University of Wisconsin-Madison University of Wisconsin-MadisonView Profile , Charles N. Fischer University of Wisconsin-Madison University of Wisconsin-MadisonView Profile Authors Info & Claims POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1982Pages 185–195https://doi.org/10.1145/582153.582174Published:25 January 1982Publication History 18citation113DownloadsMetricsTotal Citations18Total Downloads113Last 12 Months12Last 6 weeks3 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: A Flexible Approach to Interprocedural Data Flow Analysis and Programs with Recursive Data Structures

authors:
Neil D. Jones
Steven S. Muchnick

abstract: A new approach to data flow analysis of procedural programs and programs with recursive data structures is described. The method depends on simulation of the interpreter for the subject programming language using a retrieval function to approximate a program's data structures.


title: Partial Evaluation as a Means for Inferencing Data Structures in an Applicative Language: A Theory and Implementation in the Case of Prolog

abstract: An operational semantics of the Prolog programming language is introduced. Meta-IV is used to specify the semantics. One purpose of the work is to provide a specification of an implementation of a Prolog interpreter. Another one is an application of this specification to a formal description of program optimization techniques based on the principle of partial evaluation.Transformations which account for pruning, forward data structure propagation and opening (which also provides backward data structure propagation) are formally introduced and proved to preserve meaning of programs. The so defined transformations provide means to inference data structures in an applicative language. The theoretical investigation is then shortly related to research in rule-based systems and logic.An efficient well-integrated partial evaluation system is available in Qlog --- a Lisp programming environment for Prolog.


title: Programming Aspects of VLSI

authors:
Richard J. Lipton
Robert Sedgewick
Jacobo Valdes

abstract: Two components of a VLSI design environment being built at Princeton are described. The general theme of this effort is to make the design of VLSI circuits as similar to programming as possible. A conscious attempt is being made to apply experience in the design of large software systems to the creation of an appropriate environment for VLSI circuits. The two components described are a procedural language to specify circuit layouts and a switch-level circuit simulator for layout produced with this language. They have been chosen for presentation because many issues in their design are very similar to the issues that arise in the design of programming languages and software environments.


title: Guardians and Actions: Linguistic Support for Robust, Distributed Programs

authors:
Barbara Liskov
Robert Scheifler

abstract: This paper presents an overview of an integrated programming language and system designed to support the construction and maintenance of distributed programs: programs in which modules reside and execute at communicating, but geographically distinct, nodes. The language is intended to support a class of applications in which the manipulation and preservation of long-lived, on-line, distributed data is important. The language addresses the writing of robust programs that survive hardware failures without loss of distributed information and that provide highly concurrent access to that information while preserving its consistency. Several new linguistic constructs are provided; among them are atomic actions, and modules called guardians that survive node failures.


title: Axiomatic Definability and Completeness for Recursive Programs

authors:
Albert R. Meyer
John C. Mitchell

abstract: The termination assertion pq means that whenever the formula p is true, there is an execution of the possibly nondeterministic program S which terminates in a state in which q is true. Termination assertions are more tractable technically than the partial correctness assertions usually treated in the literature. Termination assertions are studied for a programming language which includes local variable declarations, calls to undeclared global procedures, and nondeterministic recursive procedures with call-by-address and call-by-value parameters. By allowing formulas p and q to place conditions on global procedures, we provide a method for reasoning about programs with calls to global procedures based on hypotheses about procedure input-output behavior. The set of first-order termination assertions valid over all interpretations is completely axiomatizable without reference to the theory of any interpretation. Although uninterpreted assertions have limited expressive power, the set of valid termination assertions defines the semantics of recursive programs in the sense of Meyer and Halpern [10]. Thus the axiomatization constitutes an axiomatic definition of the semantics of recursive programs.


title: A Semantics-Directed Compiler Generator

abstract: Article Free Access Share on A semantics-directed compiler generator Author: Lawrence Paulson Stanford University and Computer Laboratory, University of Cambridge, U. K. Stanford University and Computer Laboratory, University of Cambridge, U. K.View Profile Authors Info & Claims POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1982 Pages 224–233https://doi.org/10.1145/582153.582178Online:25 January 1982Publication History 54citation699DownloadsMetricsTotal Citations54Total Downloads699Last 12 Months13Last 6 weeks7 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: On the Composition of Processes

abstract: We describe a model of net-connected processes that amounts to a reformulation of a model derived by Brock and Ackerman from the Kahn-McQueen model of processes as relations on streams of data. The reformulation leads directly to a straightforward definition of process composition. Our notion of processes and their composition constitutes a natural generalization of the notion of functions and their composition. We apply this definition of process composition to the development of an algebra of processes, which we propose as supplying a formal semantics for a language whose domain of discourse includes nets of interconnected processes. This in turn leads us to logics of such nets, about which we raise three open and fundamental problems: existence of a finite basis for the operations of the language, finite axiomatizability of the equational theory, and decidability of this theory. A natural generalization of the model deals with the time complexity of computations.


title: Optimal Code for Control Structures

authors:
M. V. S. Ramanath
Marvin H. Solomon

abstract: Article Free Access Share on Optimal code for control structures Authors: M. V. S. Ramanath University of Western Ontario, London, Ontario, Canada University of Western Ontario, London, Ontario, CanadaView Profile , Marvin Solomon Universiy of Wisconsin, Madison, Wisconsin Universiy of Wisconsin, Madison, WisconsinView Profile Authors Info & Claims POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1982 Pages 82–94https://doi.org/10.1145/582153.582163Online:25 January 1982Publication History 0citation207DownloadsMetricsTotal Citations0Total Downloads207Last 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 AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Unbounded Speed Variability in Distributed Communication Systems

authors:
John H. Reif
Paul G. Spirakis

abstract: This paper concerns the fundamental problem of synchronizing communication between distributed processes whose speeds (steps per real time unit) vary dynamically. Communication must be established in matching pairs, which are mutually willing to communicate. We show how to implement a distributed local scheduler to find these pairs. The only means of synchronization are boolean "flag" variables, each of which can be written by only one process and read by at most one other process.No global bounds in the speeds of processes are assumed. Processes with speed zero are considered dead. However, when their speed is nonzero then they execute their programs correctly. Dead processes do not harm our algorithms' performance with respect to pairs of other running processes. When the rate of change of the ratio of speeds of neighbour processes (i.e., relative acceleration) is bounded, then any two of these processes will establish communication within a constant number of steps of the slowest process with high likelihood. Thus our implementation has the property of achieving relative real time response. We can use our techniques to solve other problems such as resource allocation and implementation of parallel languages such as CSP and ADA. Note that we do not have any probability assumptions about the system behavior, although our algorithms use the technique of probabilistic choice.


title: Optimal-Time Incremental Semantic Analysis for Syntax-Directed Editors

abstract: Attribute grammars permit the specification of static semantics in an applicative and modular fashion, and thus are a good basis for syntax-directed editors. Such editors represent programs as attributed trees, which are modified by operations such as subtree pruning and grafting. After each modification, a subset of attributes, AFFECTED, requires new values. Membership in AFFECTED is not known a priori; this paper presents an algorithm that identifies attributes in AFFECTED and computes their new values. The algorithm is time-optimal, its cost is proportional to the size of AFFECTED.


title: Lithe: A Language Combining a Flexible Syntax, Classes

abstract: Article Free Access Share on Lithe: a language combining a flexible syntax and classes Author: David Sandberg University of Washington, Seattle, WA University of Washington, Seattle, WAView Profile Authors Info & Claims POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1982Pages 142–145https://doi.org/10.1145/582153.582169Published:25 January 1982Publication History 11citation369DownloadsMetricsTotal Citations11Total Downloads369Last 12 Months34Last 6 weeks4 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: Unified Dialogue Management in the Carousel System

abstract: The paper describes the design for a software environment which unifies the dialogue management support of a number of existing software tools, such as command-language handlers, operating-system shells, transition diagram interpreters, and forms management systems. The unification is accomplished without undue complexity: the resulting design is clean and inspectable.A key notion in the design is the use of three orthogonal abstraction hierarchies, for interaction contexts, for interactive operations (roughly = commands), and for data types. These orthogonal hierarchies are used for obtaining multi-dimensional inheritance, i.e. mappings of several arguments, which may be stored in the system's data repository, and which inherit their values along the hierarchies represented in the arguments. Mappings with multi-dimensional inheritance are used in the invocation mechanism, i.e. for selecting the appropriate procedure to be executed in various situations. Currently used programming languages and software tools only use single-dimensional inheritance.A working implementation called the CAROUSEL system, is available.


title: Algorithmic Program Diagnosis

abstract: The notion of program correctness with respect to an interpretation is defined for a class of programming languages. Under this definition, if a program terminates with an incorrect output then it contains an incorrect procedure. Algorithms for detecting incorrect procedures are developed. These algorithms formalize what experienced programmers may know already.A logic program implementation of these algorithms is described. Its performance suggests that the algorithms can be the backbone of debugging aids that go far beyond what is offered by current programming environments.Applications of algorithmic debugging to automatic program construction are explored.


title: Is the Interesting Part of Process Logic Uninteresting - A Translation from PL to PDL

authors:
Rivi Sherman
Amir Pnueli
David Harel

abstract: With the (necessary) condition that atomic programs in PL be binary, we present an algorithm for the translation of a PL formula X into a PDL program τ (X) such that a finite path satisfies X iff it belongs to τ (X). This reduction has two immediate corollaries: 1) validity in this PL can be tested by testing validity of formulas in PDL; 2) all finite-path program properties expressible in this PL are expressible in PDL.The translation, however, seems to be of non-elementary time complexity. The significance of the result to the search for natural and powerful logics of programs is discussed.


title: Practical Error Recovery in LR Parsing

authors:
Seppo Sippu
Eljas Soisalon-Soininen

abstract: An automatic syntax error handling technique applicable to LR parsing is presented and analyzed. The technique includes a "phrase-level" error recovery strategy augmented with certain additional features such as "local correction". Attention has also been paid to diagnostic aspects, i.e. the automatic generation of error message texts. The technique has been implemented in the compiler writing system HLP (Helsinki Language Processor), and some promising experimental results have been obtained by testing the technique with erroneous student-written Algol and Pascal programs.


title: Maple: a Programming Language, Operating System

abstract: Maple is a statically typed language system, with very general generic facilities. It incorporates its own programming environment and provides parallel processing with a new method of process synchronization. The synchronization is the direct outgrowth of its data abstraction facility.


title: Messages as Active Agents

abstract: Network algorithms are usually stated from the viewpoint of the network nodes, but they can often be stated more clearly from the viewpoint of an active message, a process that intentionally moves from node to node. This paper gives some examples of this notion, and then discusses a means of implementing it. This implementation applied in both directions also demonstrates the logical equivalence of the two viewpoints.


title: Semantics-Directed Machine Architecture

abstract: We show how to analyze the denotational semantics for a programming language to obtain a compiler and a suitable target machine for the language. We do this by rewriting the equations using suitable combinators. The machine operates by simulating the reduction sequences for the combinator terms. The reduction sequences pass through certain standard forms, which become an architecture for the machine, and the combinators become machine instructions. Despite the abstract nature of its development, the machine greatly resembles a conventional one. The method is illustrated by a simple expression language with procedures and input-output.


title: Specification and Synthesis of Communicating Processes using an Extended Temporal Logic

abstract: We apply an Extended Propositional Temporal Logic (EPTL) to the specification and synthesis of the synchronization part of communicating processes. To specify a process, we give an EPTL formula that describes its sequence of communications. The synthesis is done by constructing a model of the given specifications using a tableau-like satisfiability algorithm for the extended temporal logic. This model can then be interpreted as a program.


title: An Axiomatic Treatment of Exception Handling

abstract: Article Free Access Share on An axiomatic treatment of exception handling Author: Shaula Yemini New York University New York UniversityView Profile Authors Info & Claims POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1982Pages 281–288https://doi.org/10.1145/582153.582183Published:25 January 1982Publication History 1citation276DownloadsMetricsTotal Citations1Total Downloads276Last 12 Months15Last 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 SiteeReaderPDF


title: Conversion of Control Dependence to Data Dependence

authors:
John R. Allen
Ken Kennedy
Carrie Porterfield
Joe D. Warren

abstract: Program analysis methods, especially those which support automatic vectorization, are based on the concept of interstatement dependence where a dependence holds between two statements when one of the statements computes values needed by the other. Powerful program transformation systems that convert sequential programs to a form more suitable for vector or parallel machines have been developed using this concept [AllK 82, KKLW 80].The dependence analysis in these systems is based on data dependence. In the presence of complex control flow, data dependence is not sufficient to transform programs because of the introduction of control dependences. A control dependence exists between two statements when the execution of one statement can prevent the execution of the other. Control dependences do not fit conveniently into dependence-based program translators.One solution is to convert all control dependences to data dependences by eliminating goto statements and introducing logical variables to control the execution of statements in the program. In this scheme, action statements are converted to IF statements. The variables in the conditional expression of an IF statement can be viewed as inputs to the statement being controlled. The result is that control dependences between statements become explicit data dependences expressed through the definitions and uses of the controlling logical variables.This paper presents a method for systematically converting control dependences to data dependences in this fashion. The algorithms presented here have been implemented in PFC, an experimental vectorizer written at Rice University.


title: Derivation of Efficient DAG Marking Algorithms

authors:
Ralph-Johan Back
Heikki Mannila
Kari-Jouko Räihä

abstract: The best known linear-time list marking algorithms also require a linear amount of workspace. Algorithms working in bounded workspace have been obtained only by allowing quadratic execution time or by restricting the list structures to trees. We improve on this here by deriving a new linear-time, bounded workspace marking algorithm that works for dags. The algorithm is derived using correctness-preserving program transformations, which prove the correctness of the algorithm. Our derivation of the marking algorithm provides an example where this method has actually been used to derive a new, more efficient algorithm, rather than just to establish the correctness of a previously known algorithm.


title: Uncovering Principles of Novice Programming

authors:
Jeffrey Bonar
Elliot Soloway

abstract: It is widely known that programming, even at a simple level, is a difficult activity to learn. Why is this so? Are novice difficulties really inherent in programming or are they related, to the nature of the programming tools currently given to novices? To answer this question we have used novice Pascal computer programs collected from their terminal sessions, controlled clinical studies focusing on specific aspects of novice programming techniques, and video-taped interviews of novice programming [Bonar, 1982]. In each we focused on bugs and buggy programs. Bugs and errors illuminate what a novice is actually thinking -- providing us a window on the difficulties as they are experienced by the novice.In previous reports we presented evidence that current programming languages do not accurately reflect the cognitive strategies used by novice programmers [Soloway et al, 1981]. Instead, we have found that novice programmers possess knowledge about and experience with step-by-step specifications in natural language. This knowledge and experience gives them powerful intuitions for using a programming language. Programming languages, however, are, not designed to appeal to these intuitions. On a semantic and pragmatic level, there are incompatibilities between the way, natural and programming languages are used. Many novice programming bugs can be directly traced to an inappropriate use of natural language specification style or strategy.As an example of these incompatibility bugs consider the "while demon" bug. Novices with this bug assume that the actions in the body of the while loop are continuously monitored for the exit condition to become true. This interpretation is consistent with the English language usage of the word while: e.g."while the highway is two lanes, continue, north". In an earlier written study [Soloway et al, 1981] found that 34% of the students in an introductory programming course thought the test in a Pascal while loop was performed, as a demon. Furthermore, a later interview study showed that novices could even describe the implementation mechanism for such a demon:"… everytime I [the variable tested in the while condition] is assigned a new value, the machine needs to check that value …"In this report we describe our use of video-taped interview studies for understanding how novices use a programming system. Interviews provide valuable information not available through statistical analysis of written studies. Written studies allow us to manipulate specific factors and guage the results to performance or style. Furthermore, we can have statistical confidence in those results. An interview study, on the other hand, allows us to examine the source of performance or style differences uncovered. Interviews give us an "execution trace" while written studies give us the final output. We use both kinds of studies, depending on the kind of information needed.We have interviewed seventeen novice programmers. Four were interviewed regularly for the first 8-10 weeks of their introductory programming course. For these regular subjects we have about 15 hours of interviews tracing their learning and maturation through the course.In this report we show an example natural language specification and discuss strategies used in that specification. We then discuss two examples of novice programming difficulties stemming from an inappropriate use of natural language specification strategies. These examples are illustrated with video tape transcripts. We conclude with a brief discussion of the implications of this work.


title: Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach

authors:
Edmund M. Clarke
E. Allen Emerson
A. Prasad Sistla

abstract: We give an efficient procedure for verifying that a finite state concurrent system meets a specification expressed in a (propositional) branching-time temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global transition graph for the concurrent system. We also show how the logic and our algorithm can be modified to handle fairness. We argue that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite state concurrent systems.


title: Compilation of Data-Driven Programs for Synchronous Execution

authors:
Janice E. Cuny
Lawrence Snyder

abstract: We present algorithms that convert a class of parallel programs, called loop programs, from data-driven mode to synchronous mode. Such algorithms enable programmers to use a high-level, data-driven programming language without forfeiting the efficiency of a synchronous machine. We characterize loop programs for which conversion is possible in terms of sets of balancing equations and we present two conversion algorithms.


title: Making Variables Abstract: An Equational Theory for Russell

authors:
Alan J. Demers
James E. Donahue

abstract: One of the fundamental notions of programming, and thus of programming languages, is the variable. Recently, the variable has come under attack. The proponents of "functional programming" have argued that variables are at the root of all our problems in programming. They claim that we must rid our languages of all manifestations of the "vonNeumann bottleneck" and learn to live in the changeless world of functional combinators.While we may not, believe all the claims of the functional programming advocates, there is evidence that the treatment of variables in most programming languages leaves much to be desired. In this paper we discuss how to make variables "abstract", i.e., how to introduce the notion of variable in to a language so that variables have reasonable mathematical properties. This paper includes:--- a discussion of language design principles that allow a more mathematical treatment of variables in programming language, and--- a description of an equational logic for the programming language Russell [Boehm80]. Although this logic follows much of the development of abstract data types (cf. [Guttag78]), it is novel in its treatment of a language in which expressions not only produce values but also can have effects. We discuss the over all structure of the logic and present in detail the rules particularly relevant to the semantics of variables. A complete presentation of the logic appears in [Demers82], and the rule numbers in this paper agree with the numbers used there.In the next section, we discuss the underlying language principles needed to make an equational specification of variables possible. In the sections that follow, we present a logic that does so for Russell.


title: "Sometimes" and "Not Never" Revisited: On Branching Versus Linear Time

authors:
E. Allen Emerson
Joseph Y. Halpern

abstract: Temporal logic ([PR57], [PR67]) provides a formalism for describing the occurrence of events in time which is suitable for reasoning about concurrent programs (cf. [PN77]). In defining temporal logic, there are two possible views regarding the underlying nature of time. One is that time is linear: at each moment there is only one possible future. The other is that time has a branching, tree-like nature: at each moment, time may split into alternate courses representing different possible futures. Depending upon which view is chosen, we classify (cf. [RU71]) a system of temporal logic as either a linear time logic in which the semantics of the time structure is linear, or a system of branching time logic based on the semantics corresponding to a branching time structure. The modalities of a temporal logic system usually reflect the semantics regarding the nature of time. Thus,in a logic of linear time, temporal operators are provided for describing events along a single time path (cf. [GPSS80]). In contract, in a logic of branching time the operators reflect the branching nature of time by allowing quantification over possible futures cf. [AB80],[EC80]).


title: A Program Form Based on Data Dependency in Predicate Regions

authors:
Jeanne Ferrante
Karl J. Ottenstein

abstract: A new program representation is presented which permits certain optimizations to be performed at less expense than with other forms. This paper describes code motion, common subexpression elimination and induction variable detection. Scalar propagation and constant folding are sketched here, but detailed elsewhere. The powerful code motion strategy allows entire regions of the program to be moved. The representation described may be used as a compiler intermediate form or simply as a model for program analysis. It has great potential for use in translation for parallel machines.


title: Code Generation for Silicon

abstract: Compiler writers facea bleak future---soon everyone will be using Ada on the Nebula Architecture and there will be no further need for our services. Luckily, it appears to be possible to recycle compiler writers by encouraging them to build circuit design tools (Silicon Compilers). Many of the standard techniques used in compilers can be immediately applied in circuit design, especially for LSI circuits. In part, this paper attempts to serve as a tutorial, casting some of the problems of designing in nMOS with the Mead-Conway design rules into the vocabulary of the compiler writer. The paper also discusses experience with a Silicon compiler that has fabricated over two dozen different designs.


title: Precise Typing of Abstract Data Type Specifications

abstract: There are two important notions of types being used in programming languages today. In the concept called types, types are algebras; the semantics of programs is described in terms of operations in these algebras. Another notion of found in most of the typed programming languages in actual use regards types as sets of objects; the elements of types are the objects manipulated by the operators of a programming language. I shall be careful to use abstract when I mean the algebraic notion, and data or simply type to mean the set-based concept.This paper presents a formal theory of types as an approximation to the exact semantics of a language, following the lead of Milner [Mil78]. The semantics is based upon multi-sorted algebras [ADJ73, 76, 77, 78] and is applied to a language consisting of equational specifications that define an type. The principal results of the paper are to characterize a class of typings as uniform approximations to an exact semantics, to extend Milner's theory of types to include types formed by coproduct construction, and to explicate typing as an (approximate) semantics for an equational theory.In developing a formal theory of types as multi-sorted algebras, the word is used to designate names used to distinguish various sets of objects that may constitute the domains of operators. Sorts are thus analogous to types in programming languages. However, the sort signatures given to operators of types do not themselves constitute a very richly descriptive language. Sort names can be formed into sequences, corresponding to product construction in an object domain, but the theory (multi-sorted Σ-algebras) does not seem to allow alternation sequences of sorts, corresponding to coproduct construction in an object domain. If this were possible, then sort signatures could actually fulfill the role of types. We shall see that alternation sequences in signatures arise naturally as a consequence of the semantics given to an equational theory.


title: Abstraction Mechanisms in the Beta Programming Language

authors:
Bent Bruun Kristensen
Ole Lehrmann Madsen
Birger Møller-Pedersen
Kristen Nygaard

abstract: The BETA programming language is developed as part of the BETA project. The purpose of this project is to develop concepts, constructs and tools in the field of programming and programming languages. BETA has been developed from 1975 on and the various stages of the language are documented in [BETA a].


title: Reasoning About Nonatomic Operations

abstract: A method is presented that permits assertional reasoning about a concurrent program even though the atomicity of the elementary operations is left unspecified. It is based upon a generalization of the dynamic logic operator [α]. The method is illustrated by verifying the mutual exclusion property for a two-process version of the bakery algorithm.


title: Practical Use of a Polymorphic Applicative Language

authors:
Butler W. Lampson
Eric E. Schmidt

abstract: Assembling a large system from its component elements is not a simple task. An adequate notation for specifying this task must reflect the system structure, accommodate many configurations of the system and many versions as it develops, and be a suitable input to the many tools that support software development. The language described here applies the ideas of λ-abstraction, hierarchical naming and type-checking to this problem. Some preliminary experience with its use is also given.


title: Polymorphic Type Inference

abstract: The benefits of strong typing to disciplined programming, to compile-time error detection and to program verification are well known. Strong typing is especially natural for functional (applicative) languages, in which function application is the central construct, and type matching is therefore a principal program correctness check. In practice, however, assigning a type to each and every expression in a functional program can be prohibitively cumbersome. As expressions are compounded, the task of assigning a type to each expression and subexpression becomes practically impossible, even more so because the type-expressions themselves grow longer. It becomes imperative therefore to design friendly programming environments that permit the user type-free programming, but that generate fully typed programs in which the types of all expressions are inferred by the system from the program. For interactive functional programming environments of the kind implemented for the Edinburgh functional programming language ML, a type-inference system is an invaluable tool for on-line parse-time error detection and debugging.


title: Structural Semantics for Polymorphic Data Types

abstract: The semantic modeling of data types has been the subject ofincreased interest over the last few years, enhanced by thedevelopment of applicative languages such as Edinburgh's ML andHOPE, by the need for flexible highly structured languages thatwould nonetheless be amenable to verification, and by ongoinginquiries on polymorphism in programming languages. In particular,there has been a growing interest in generic type structures suchas the Reynolds-Girard discipline of full polymorphism, furtherextended by McCracken [McC] and MacQueen and Sethi [MS], and inuser-defined and recursively-defined types.Our aim here is to model semantically the notion of type so asto encompass full polymorphism, but in a very controlled way whichon the one hand allows the modeling to remain simple, and on theother hand conveys as much of the notion of type as seems feasiblyrelevant to programming languages.Our leading idea is that a type is a structural condition ondata objects rather than a collection of objects which satisfiescertain closure properties. Roughly, we argue that such structuralconditions are fully conveyed by syntactic expressions, not inisolation of course, but within a syntax-oriented typediscipline. In other words, we treat types as discrete objects,which merely code the ways data objects are allowed to interact (asin applying functional object a to object b). Once atype discipline is set to delineate a set of type expressions, andonce the meaning of the type-constructs is imposed on the ways thedata objects relate, the meaning of each type expression isconveyed by the expression itself (reduced to a canonical form ifnecessary). This conception of types permits a strikingly simplemodeling of the use of types as arguments of data objects, a usecentral to Reynolds' polymorphic type system [Rey].The use of types as genuine arguments of procedures is notdevoid of practical interest. E.g., one may wish to treat objectsof type o generically, except for an initial choice dependingon the principal type-constructor of o, that is, according towhether o is an atomic type, a functional type, a cartesianproduct, etc.A particular situation where such choices may be useful is wherea procedure has a formal parameter intended to range over some datastructure (trees of sequences of objects of type t, say), adata structure that has a number of accepted representations byformal data types. It seems desirable to permit the definition of apolymorphic procedure that would accept as valid a number of suchformal representations, branching on them internally. This kind offacility would elevate the polymorphism of a procedure from thelevel of uses with in a single program, to the level oftransportability from one set of data structure specifications toanother.This kind of use of types as arguments is compatible withReynold's discipline of type abstraction, but not with thequantificational discipline of [MS] (cf.[Lei83], §4.2). Whilethe two disciplines, as uninterpreted and unexpanded calculi, arecombinatorially isomorphic the difference between their intendedsemantics becomes apparent when primitive functions over types(such as discriminators over main type-constructor) areconsidered.The examples we have given of uses of types as arguments arefairly restricted in nature: all that is used of a type is itssyntactically representable structure. This is not merely anempirical observation on our limited perception at present time. Ina typed discipline of programming each object carries its type(explicitly or not), and all types of denotable objects arethemselves denotable. It follows that any question that one may askabout the type of a denotable object reduces to a question abouttype-expression(s) denoting that type. The issue of semanticallymodeling Reynold's rich discipline of type abstraction is thereforereduced, from a pragmatic point of view, to a modeling in whichquestions about types are all expressible as questions about typeexpressions.Existing approaches to the semantic modeling of data types are,in one form or another, conceptual continuations of thedenotational semantics approach to data objects. McCracken [McC],following [Sco], defines types as retracts of the universal domain.In Shamir and Wadge [SW], Milner [Mil] and MacQueen and Sethi [MS]types are modeled as some kind of ideal, where an ideal is asubset of the object-domain that satisfies certain closureconditions. In both approaches types are being defined via theproperties that they must satisfy, as sets of objects, so as tobecome compatible with their use. (This may be compared with thealgebraic approach to types, where each particular type isdefined via its algebraic properties rather than its intendedconception).Our modeling of types too is grafted on top of a denotationalsemantics for the object language, However,it has a life of itsown, and can be explained in isolation, or combined with forinstance, an operational semantics for the object language. Thepoint we are trying to make is that the semantics of types haslittle to do with the issues of self-application and continuitywhich motivate denotational semantics. Rather than amalgamateobjects and types, as in [SW] (where types as sets of objects aretreated on an equal footing with objects as sets ofapproximations), we separate the two radically.We make no claim, of course, that our approach should supplantthe modeling of types as retracts or as ideals. Rather, we believethat the semantics we propose is related to types-as-ideals in muchthe same way as operational semantics is related to denotationalsemantics: it is closer to programming practice, permits a smallerset of objects, and is sensitive to the choice of formal framework(which for us is the type discipline). We therefore feel that thetwo approaches should shed light on each other and, in combination,enhance our understanding of complex data-types and and theirproper use.In particular, we believe that even putting down the definitionsand proving basic existence theorems provides some insight aboutthe design and use of data types. For one, our modeling of typessuggests a feasible controlled use of types as arguments of dataobjects. For another, it points to directions in setting very richtype disciplines evolving naturally from a structural-computationalview of types. For instance, it may be useful and feasible toconsider types built as certain recursive sets of other types.Following preliminaries in sections 1 and 2 we define in section3 what is a model of the pure polymorphic lambda calculus.A termmodel is constructed in §4,in §5 we show how to constructa non-extensional model through the solution of a domain equation,and in §6 we construct an extensional model through such asolution. The latter construction involves breaking the circularityin the conditions underlying polymorphic typing, by a method akinto Girard's in the proof theory of higher order logic [Gir].We plan to extend this work in two directions. One is thetreatment of more general type disciplines, of the kinds defined byMcCracken [McC] and further studied by MacQueen and Sethi [MS]. Thecrucial issue here is that, in contrast to Reynold's discipline,distinct type expressions may denote the same type. However, eachtype expression has a normal form, which may be viewed as itsvalue (this view has been advocated in greater generality by PerMartin-Lof [Mar], on somewhat more philosophical grounds). A seconddirection, incorporating aspects of the first, is the treatment ofrecursively defined data types in a polymorphic context, andpossibly more general notions of types.


title: Computer Experiments with the Reve Term Rewriting System Generator

abstract: A term rewriting system generator called REVE is described. REVE builds confluent and uniformly terminating term rewriting systems from sets of equations. Particular emphasis is placed on mechanization of termination proof. Indeed, REVE is one of the few such systems which can actually be called automatic because termination is fully integrated into the algorithms. REVE uses an incremental termination method based on recursive decomposition ordering which constructs the termination proof step by step from the presentation of the set of equations and which requires little knowledge of termination methods from the user. All examples from this paper are taken from abstract data type specifications.


title: How to Cook a Temporal Proof System for Your Pet Language

authors:
Zohar Manna
Amir Pnueli

abstract: An abstract temporal proof system is presented whose program-dependent part has a high-level interface with the programming language actually studied. Given a new language, it is sufficient to deline the interface notions of atomic transitions, justice, and fairness in order to obtain a full temporal proof system for this language. This construction is particularly useful for the analysis of concurrent systems. We illustrate the construction on the shared-variable model and on CSP. The generic proof system is shown to be relatively complete with respect to pure first-order temporal logic.


title: Incremental Polymorphic Type Checking in B

abstract: The programming language B has been designed for personal computing. In B, variables need not be declared, nor formal parameters specified. Nevertheless, B is strongly typed. All type requirements can be checked statically. To signal type violations on the spot during editing, the computations can be organized so that local the source text require a modest amount of recomputation.


title: Locality in Software Systems

abstract: This paper proposes a technique for what we call localization of power in computer systems, which can be viewed as a generalization of such linguistic disciplines as scope rules, strong typing and data-abstraction. Although the proposed technique is conceptually based on the theory of protection, it is presented as a rather simple extension of the package construct of the Ada language. This technique is expected to be beneficial for software engineering in several ways. In particular:• It facilitates reasoning about large scale systems, by allowing one to ignore most of the details of the system when reasoning about specific aspects of it.• It provides us with a generalization of the conventional concept of data-abstraction, by allowing the formation of several different abstractions for the same type of objects, and by supporting "interactions" between the abstractions of different types.• It allows us to provide parts of a system with a certain ability to control the activity of the rest of it.• It supports a broad spectrum of policies for the design and management of large scale, evolving systems.


title: Practical Program Verification: Automatic Program Proving for Real-Time Embedded Software

authors:
John Nagle
Scott Johnson

abstract: Despite the attractiveness of the concept, attempts to date to use proof of correctness techniques on production software have been generally unsuccessful. The obstacles encountered are not fundamental. We have implemented a proof of correctness system to be used for improving the realiability of certain small, real-time programs. It appears that many of the problems of past systems can be avoided.This work is supported by the Long Range Research Program of the Ford Motor Company, Dearborn, Michigan.


title: Verifying Reachability Invariants of Linked Structures

abstract: The paper introduces a reachability predicate for linear lists, develops the elementary axiomatic theory of the predicate, and illustrates its application to program verification with a formal proof of correctness for a short program that traverses and splices linear lists.


title: Transformational Programming - Applications to Algorithms and Systems

abstract: Ten years ago Cheatham and Wegbreit [4] proposed a transformational program development methodology based on notions of top-down stepwise program refinement first expressed by Dijkstra [10] and Wirth [45]. A schema describing the process of this methodology is given in fig. 1. To develop a program by transformation, we first specify the program in as high a level of abstraction and as great a degree of clarity as our programming language admits. This high level problem statement program P is proved correct semimechanically according to some standard approach (see Flovd and Hoare [15, 21]), Next, using an interactive system equipped with a library of encoded transformations, each of which maps a correct program into another equivalent program, we select and apply transformations one at a time to successive versions of the program until we obtain a concrete, low level, effecient implementation version P'. The goals of transformational programming are to reduce programming labor, improve program reliability, and upgrade program performance. In order for labor to be reduced, the effort required to obtain P, prove it correct, and derive P' by transformation should be less than the effort required to code P from scratch, and also to debug it. Program reliability will be improved if P can be certified correct, and if each transformation preserves program meaning. Finally, program performance will be upgraded if transformations are directed towards increased efficiency.


title: Five Paradigm Shifts in Language Design and their Realization in Viron, a Dataflow Programming Environment

abstract: We describe five paradigm shifts in programming language design, some old and some relatively new, namely Effect to Entity, Serial to Parallel, Partition Types to Predicate Types, Computable to Definable, and Syntactic Consistency to Semantic Consistency. We argue for the adoption of each. We exhibit a programming language, Viron, that capitalizes on these shifts.