1,205 papers · page 50 of 61
Current research in specifications is emphasizing the practical use of formal specifications in program design. One way to encourage their use in practice is to provide specification languages that are accessible to both designers and programmers. With this goal in mind, the Larc…
An axiomatic semantic definition is given of the replacement model of exception handling in an expression-oriented language. These semantics require only two new proof rules for the most general case. An example is given of a program fragment using this model of exception handlin…
The problem of correctness of the solutions to the distributed termination problem of Francez [7] is addressed. Correctness criteria are formalized in the customary framework for program correctness. A very simple proof method is proposed and applied to show correctness of a solu…
The PSG programming system generator developed at the Technical University of Darmstadt produces interactive, language-specific programming environments from formal language definitions. All language-dependent parts of the environment are generated from an entirely nonprocedural …
We propose a methodology for the development of concurrent programs and apply it to an important class of problems: quiescence detection. The methodology is based on a novel view of programs. A key feature of the methodology is the separation of concerns between the core problem …
Aspect of the interaction between compiler theory and practice is addressed. Presented is a technique for the syntax-directed specification of compilers together with a method for proving the correctness of their parse-driven implementations. The subject matter is presented in an…
PARLOG is a logic programming language in the sense that nearly every definition and query can be read as a sentence of predicate logic. It differs from PROLOG in incorporating parallel modes of evaluation. For reasons of efficient implementation, it distinguishes and separates a…
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 state graph…
In spite of substantial progress in the theory of interprocedural data flow analysis, few practical compiling systems can afford to apply it to produce more efficient object programs. To perform interprocedural analysis, a compiler needs not only the source code of the module bei…
Consider a network of communicating finite state machines that exchange messages over unbounded FIFO channels. Each machine in the network can be defined by a directed graph whose nodes represent the machine states and whose edges represent its transitions. In general, for a node…
A language for describing communicating systems is described. It is sufficiently expressive to describe both the desired behavior of systems, their specifications , and their actual implementations in terms of simpler components. We say I satisfies S if 1 is a correct implementat…
The ability to generate language-based editors depends on the existence of a powerful, language-independent model of editing. A model is proposed in which programs are represented as attributed abstract-syntax trees with an associated relational database. Relations can depend on …
The “referential transparency” principle of applicative language expressions stipulates that a single value exists for all occurrences of an expression in a given context (where a context is a set of bindings of variables to values). In principle, each such value therefore need t…
A framework is presented for adding a general Undo facility to programming languages. A discussion of relevant literature is provided to show that the idea of Undoing pervades several areas in computer science, and even other disciplines. A simple model of computation is introduc…
The problem of concurrent accesses to registers by asynchronous components is considered. A set of axioms about the values in a register during concurrent accesses is proposed. It is shown that if these axioms are met by a register, then concurrent accesses to it may be viewed as…
PegsSys is an experimental system in which a user formally describes how a program is put together by means of a hierarchically structured collection of pictures, called formal dependency diagrams (FDDs). Icons in an FDD denote a wide range of data and control dependencies among …
In Part 1 of this paper [5], we presented a scheme whereby a compiler could propagate demands through programs in a powerful stream language L. A data-driven evaluation of the transformed program performed exactly the same computation as a demand-driven evaluation of the original…
In this paper we offer a short proof of the DeRemer-Pennello conjecture that if the LR(0) automaton for a grammar G contains a state p and a nonterminal A such that ( p , A ) is a nonterminal transition, ( p , A ) includes + ( p , A ) and Read ( p , A ) is not empty, then grammar…
The ideal computer language is seen as one that would be as readable as natural language, and so adaptable that it could serve as the only language a user need ever know. An approach to language design has emerged that shows promise of allowing one to come much closer to that ide…