2,199 papers · page 101 of 110
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 …
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 th…
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 aspec…
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 fa…
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 discusse…
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 c…
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…
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 19…
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 ye…
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…
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 correspond…
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 a…
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…
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 incor…
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 ca…
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 identifi…
No abstract available.
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 uno…
No abstract available.
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 eval…