2,199 papers · page 103 of 110
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 c…
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 restrict…
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 …
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…
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 cau…
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 eff…
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 a…
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 da…
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 se…
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 whic…
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, be…
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 …
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…
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 con…
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 d…
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 …
We consider the question of how powerful a relational query language should be and state two principles that we feel any query language should satisfy. We show that although relational algebra and relational calculus satisfy these principles, there are certain queries involving l…
Path expressions are a tool for synchronization of concurrent processes. They are an integral part of the data abstraction mechanism in a programming language, and specify synchronization entirely in terms of the allowable sequences of operations on an object of the abstract data…
Article Free Access Share on An efficient way to find the side effects of procedure calls and the aliases of variables Author: John P. Banning Stanford Linear Accelerator Center, Stanford, California and Amdahl Corporation, Sunnyvale, California Stanford Linear Accelerator Center…
First Order Programming Logic is a simple, yet powerful formal system for reasoning about recursive programs. In its simplest form, it has one major limitation: it cannot establish any property of the least fixed point of a recursive program which is false for some other fixed po…