2,199 papers · page 98 of 110
This paper proposes an expressional loop notation (XLoop) based on the ideas described in [16,17] which makes it practical to express loops as compositions of functions. The primary benefit of XLoop is that it brings the powerful metaphor of expressions and decomposability to bea…
Inverse currying transformation of an attribute grammar moves a context condition to places in the grammar where the violation of the condition can be detected as soon as the semantic information used in the condition is computed. It thereby takes into account the evaluation orde…
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 …
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…
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…
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 g…
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. W…
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 th…
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 th…
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 sk…
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…
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…
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 …
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 e…
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 t…
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 match…
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 ver…
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 ac…
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 o…
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, th…