R. L. Graham proposed an O(n log n) algorithm for determining the convex hull of a finite set of points in the plane. Variations of this method in five published papers contain errors in this rather simple algorithm. ...
详细信息
R. L. Graham proposed an O(n log n) algorithm for determining the convex hull of a finite set of points in the plane. Variations of this method in five published papers contain errors in this rather simple algorithm. The authors believe that the difficulty lies in the method used for developing and describing the algorithm and its proof - typically directly in terms of circular doubly-linked lists. They present an alternative method which they believe allows for a more rigorous but simple and understandable treatment.
作者：
MORGAN, CComputing Laboratory
Programming Research Group Oxford University 8-11 Keble Road Oxford United Kingdom OXI 3QD
A set of local variables in a program is considered auxiliary if its members occur only in assignments to members of the same set. Data refinement changes a program, replacing one set of local variables by another se...
详细信息
A set of local variables in a program is considered auxiliary if its members occur only in assignments to members of the same set. Data refinement changes a program, replacing one set of local variables by another set, in order to move toward a more efficient representation of data. Most techniques of data refinement give a direct transformation, but there exists an indirect technique, using auxiliary variables, that proceeds in several stages. Generally, the 2 techniques are considered separately. It is demonstrated that the several stages of the indirect technique are themselves special cases of the direct one, thus unifying the separate approaches. Removal of auxiliary variables is formalized incidentally.
While the use of global time is an expensive tool to implement, it can simplify the design and description of distributed algorithms. It is demonstrated that, in some cases, global time can be assumed while designing...
详细信息
While the use of global time is an expensive tool to implement, it can simplify the design and description of distributed algorithms. It is demonstrated that, in some cases, global time can be assumed while designing an algorithm, but need not be implemented. In these cases, it can be replaced with Lamport's logical time in a routine fashion, which clearly assures the correctness of the algorithm. The method is illustrated by 3 examples: 1. Chandy and Lamport's distributed snapshot algorithm, 2. Banatre and Lapalme's fair agreement algorithm for the distributed auction system, Enchere, and 3. a new distributed algorithm for restarting from a saved checkpoint state. It is shown that, if a property of a distributed computation is preserved by reorderings that respect event sequences in nodes and channels individually, then that property can be established by an algorithm that assumes global time, but is provided with logical time.
Matrix Code gives imperative programming a mathematical semantics and heuristic power comparable in quality to functional and logic programming. A program in Matrix Code is developed incrementally from a specification...
详细信息
Matrix Code gives imperative programming a mathematical semantics and heuristic power comparable in quality to functional and logic programming. A program in Matrix Code is developed incrementally from a specification in pre/post-condition form. The computations of a code matrix are characterized by powers of the matrix when it is interpreted as a transformation in a space of vectors of logical conditions. Correctness of a code matrix is expressed in terms of a fixpoint of the transformation. The abstract machine for Matrix Code is the dual-state machine, which we present as a variant of the classical finite-state machine. (C) 2013 Elsevier B.V. All rights reserved.
C is one of the most popular generally used languages of the 1980's. Its advantages are well known. In writing three books on the language, one of the authors has espoused many of its virtues without adequately co...
详细信息
C is one of the most popular generally used languages of the 1980's. Its advantages are well known. In writing three books on the language, one of the authors has espoused many of its virtues without adequately commenting on its vices. This paper will attempt to redress that balance.
During the software crisis of the 1960s, Dijkstra's famous thesis "goto considered harmful" paved the way for structured programming. This short communication suggests that many current difficulties of p...
详细信息
During the software crisis of the 1960s, Dijkstra's famous thesis "goto considered harmful" paved the way for structured programming. This short communication suggests that many current difficulties of parallel programming based on message passing are caused by poorly structured communication, which is a consequence of using low-level send-receive primitives. We argue that, like goto in sequential programs, send-receive should be avoided as far as possible and replaced by collective operations in the setting of message passing. We dispute some widely held opinions about the apparent superiority of pairwise communication over collective communication and present substantial theoretical and empirical evidence to the contrary in the context of MPI ( Message Passing Interface).
We present through the algorithmic language DHL (Dijkstra-Hehner language), a practical approach to a simple first order theory based on calculational logic, unifying Hoare and Dijkstra's iterative style of progra...
详细信息
We present through the algorithmic language DHL (Dijkstra-Hehner language), a practical approach to a simple first order theory based on calculational logic, unifying Hoare and Dijkstra's iterative style of programming with Hehner's recursive predicative programming theory, getting the "best of the two worlds" and without having to recur in any way to higher-order approaches such as predicate transformers, Hoare logic, fixed-point or relational theory.
The effectiveness of set theoretic concepts for the purpose of software specification is becoming more and more widely recognized. This paper presents an integrated relational methodology for software specification, a...
详细信息
The effectiveness of set theoretic concepts for the purpose of software specification is becoming more and more widely recognized. This paper presents an integrated relational methodology for software specification, and shows its effectivness when applied to a practical example.
The main goal of the extensible set language (ESL) is to construct a translator for a set oriented extensible language which can produce efficient code. The ESL, now under development, uses clusters for extending the ...
详细信息
The main goal of the extensible set language (ESL) is to construct a translator for a set oriented extensible language which can produce efficient code. The ESL, now under development, uses clusters for extending the set oriented language and for mappimg the sets and their operators into base language data structure and operators. The main difficulty in this mapping is the dependency among clusters. The dialogue is a compile time procedure which is part of a cluster. It manipulates data structures and enables each cluster to appear independent. It also enables the user to chose one of a family of data implementations defined by the cluster. Thus the dialogue makes it possible for a data structure to appear as a building block which can be used simply and flexibly. ESL can be distinguished in several parts. One part, the set language (SL), is sublanguage of ESL in which the user writes his application. The ESL compiler gets an ESL program as input and produces a base a language (BL) program or output. The parts of ESL not covered by the union of SL and BL are mixed BL, Sl types, clusters and diagrams, and mappings.
Formal program construction by transformations is a method of software development in which a program is derived from a formal problem specification by manageable, controlled transformation steps which guarantee that ...
详细信息
Formal program construction by transformations is a method of software development in which a program is derived from a formal problem specification by manageable, controlled transformation steps which guarantee that the final product meets the initial specification. This methodology has been investigated in the Munich project CIP (computer-aided, intuition-guided programming). The research includes the design of a wide-spectrum language specifically tailored to the needs of transformational programming, the construction of a transformation system to support the methodology, and the study of transformation rules and other methodological issues. Particular emphasis has been laid on developing a sound theoretical basis for the overall approach. [ABSTRACT FROM AUTHOR]
暂无评论