Algorithms that deal with arrays in a complicated fashion are either explained informally in terms of pictures, explained more formally but with overwhelming details, or not explained at all. An attempt is made to pr...
详细信息
Algorithms that deal with arrays in a complicated fashion are either explained informally in terms of pictures, explained more formally but with overwhelming details, or not explained at all. An attempt is made to present some notations and concepts to make the development and proof of one such algorithm more appealing and convincing. The algorithm is developed for the in-situ inversion of a cyclic permutation represented in an array. The ring is introduced as a suitable representation of a cyclic permutation since conventional representations of cyclic permutations are not suited to manipulative needs. For the sake of manageability, few elements of rings should have a name, in contrast to the conventional notations for rings in which each element is named and in which even a simple rule becomes awkward to formulate. The exercise confirms that, in designing algorithms, the development of adequate mathematical notations is a key issue that is hardly addressed by traditional mathematics.
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.
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.
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.
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).
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 extensible set language (ESL) uses clusters for extending the set oriented language and for mapping the sets and their operators into base language data structure and operators. The main difficulty in this mapping...
详细信息
The extensible set language (ESL) uses clusters for extending the set oriented language and for mapping the sets and their operators into base language data structure and operators. The main difficulty in this mapping is the dependency among clusters, i.e., the use of one data structure requires the modification or the constraint of another. 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 choose one of a family of data implementations defmed 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.
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]
暂无评论