2,199 papers · page 99 of 110
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 theo…
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 th…
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.
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…
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 adoptio…
In this paper we present ACINCF and ACINCB, incremental update algorithms for forward and backward data flow problems, which are based on a linear equations model of Allen/Cocke interval analysis [Allen 77, Ryder 82a]. We have studied their performance on a robust structured prog…
This paper discusses features of a secure systems programming language designed and implemented at IBM's Watson Research Lab. Two features of the language design were instrumental in permitting security to be enforced with minimum run-time cost: (1) Language constructs (e.g. poin…
In our paper [Wand 82a], we introduced a paradigm for compilation based on combinators. A program from a source language is translated (via a semantic definition) to trees of combinators; the tree is simplified (via associative and distributive laws) to a linear, assembly-languag…
This paper shows how to rapidly determine the path relationships between k different elements of a graph (of the type primarily resulting from programs) in time proportional to k log k. Given the path relations between elements u,v, and w, it is easy to answer questions like "is …
Ada is rich in the variety of its abstraction mechanisms. It has both a data abstraction mechanism (packages with private data types) that supports a functional programming style and a program abstraction mechanism (generic program units) that supports an object-oriented program …
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 axiomat…
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 s…
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 …
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 powe…
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 …
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
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 fo…
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 …
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 i…
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-de…