The transformational programming method of algorithm derivation starts with a formal specification of the result to be achieved, plus some informal ideas as to what techniques will be used in the implementation. The f...
详细信息
The transformational programming method of algorithm derivation starts with a formal specification of the result to be achieved, plus some informal ideas as to what techniques will be used in the implementation. The formal specification is then transformed into an implementation, by means of correctness-preserving refinement and transformation steps, guided by the informal ideas. The transformation process will typically include the following stages: (1) Formal specification (2) Elaboration of the specification, (3) Divide and conquer to handle the general case (4) Recursion introduction, (5) Recursion removal, if an iterative solution is desired, (6) Optimisation, if required. At any stage in the process, sub-specifications can be extracted and transformed separately. The main difference between this approach and the invariant based programming approach (and similar stepwise refinement methods) is that loops can be introduced and manipulated while maintaining program correctness and with no need to derive loop invariants. Another difference is that at every stage in the process we are working with a correct program: there is never any need for a separate "verification" step. These factors help to ensure that the method is capable of scaling up to the development of large and complex software systems. The method is applied to the derivation of a complex linked list algorithm and produces code which is over twice as fast as the code written by Donald Knuth to solve the same problem.
Given a high-level specification and a low-level programming language, our goal is to automatically synthesize an efficient program that meets the specification. In this paper, we present a new algorithmic methodology...
详细信息
ISBN:
(纸本)9781450302036
Given a high-level specification and a low-level programming language, our goal is to automatically synthesize an efficient program that meets the specification. In this paper, we present a new algorithmic methodology for inductive synthesis that allows us to do this. We use Second Order logic as our generic high level specification logic. For our low-level languages we choose small application-specific logics that can be immediately translated into code that runs in expected linear time in the worst case. We explain our methodology and provide examples of the synthesis of several graph classifiers, e. g, linear-time tests of whether the input graph is connected, acyclic, etc. In another set of applications we automatically derive many finite differencing expressions equivalent to ones that Paige built by hand in his thesis [Pai81]. Finally we describe directions for automatically combining such automatically generated building blocks to synthesize efficient code implementing more complicated specifications. The methods in this paper have been implemented in Python using the SMT solver Z3 [dMB].
作者：
Whittle, JNASA
Ames Res Ctr Recom Technol Moffett Field CA 94035 USA Univ Edinburgh
Edinburgh EH8 9YL Midlothian Scotland Napier Univ
Dept Comp Studies Edinburgh EH14 1DJ Midlothian Scotland
Functional programming presents new challenges in the design of programming environments. In a strongly typed functional language, such as ML, much conventional debugging of runtime errors is replaced by dealing with ...
详细信息
Functional programming presents new challenges in the design of programming environments. In a strongly typed functional language, such as ML, much conventional debugging of runtime errors is replaced by dealing with compile-time error reports. On the other hand, the cleanness of functional programming opens up new possibilities for incorporating sophisticated correctness-checking techniques into such environments. C(Y)NTHIA is a novel editor for ML that both addresses the challenges and explores the possibilities. It uses an underlying proof system as a framework for automatically checking for semantic errors such as non-termination. In addition, C(Y)NTHIA embodies the idea of programming by analogy-whereby users write programs by applying abstract transformations to existing programs. This paper investigates C(Y)NTHIA's potential as a novice ML programming environment. We report on two studies in which it was found that students using C(Y)NTHIA commit fewer errors and correct errors more quickly than when using a compiler/text editor approach. (C) 2000 Academic Press.
In the constructive programming community it is commonplace to see formal developments of textbook algorithms. In the algorithm design community, on the other hand, it may be well known that the textbook solution to a...
详细信息
In the constructive programming community it is commonplace to see formal developments of textbook algorithms. In the algorithm design community, on the other hand, it may be well known that the textbook solution to a problem is not the most efficient possible. However, in presenting the more efficient solution, the algorithm designer will usually omit some of the implementation details, thus creating an algorithm gap between the abstract algorithm and its concrete implementation. This is in contrast to the formal development, which usually proceeds all the way to the complete concrete implementation of the less efficient solution. We claim that the algorithm designer is forced to omit some of the details by the relative expressive poverty of the Pascal-like languages typically used to present the solution. The greater expressiveness provided by a functional language would allow the whole story to be told in a reasonable amount of space. In this paper we use a functional language to present the development of a sophisticated algorithm all the way to the final code. We hope to bridge the algorithm gap between abstract and concrete implementations, and thereby facilitate communication between the constructive programming and algorithm design communities. (C) 1999 Elsevier Science B.V. All rights reserved.
What does it mean to say that one program is 'more abstract' than another? What is 'abstract' about an abstract data type? What is the difference between a 'high-level' program and a 'low-l...
详细信息
What does it mean to say that one program is 'more abstract' than another? What is 'abstract' about an abstract data type? What is the difference between a 'high-level' program and a 'low-level' program? In this paper we attempt to answer these questions by formally defining an abstraction relation between programs which matches our intuitive ideas about abstraction. The relation is based on examining the operational semantics of the programs, expressed as a set of traces (sequences of states) from a given initial state to a possible final state.
A theory for the derivation of on-line algorithms is presented. The algorithms are derived in the Bird-Meertens calculus for program transformations. This calculus provides a concise functional notation for algorithms...
详细信息
A theory for the derivation of on-line algorithms is presented. The algorithms are derived in the Bird-Meertens calculus for program transformations. This calculus provides a concise functional notation for algorithms, and a few powerful theorems for proving equalities of functions. The theory for the derivation of on-line algorithms is illustrated with the derivation of an algorithm for finding palindromes. An on-line linear-time random access machine (RAM) algorithm for finding the longest palindromic substring in a string is derived. For the purpose of finding the longest palindromic substring, all maximal palindromic substrings are computed. The list of maximal palindromes obtained in the computation of the longest palindrome can be used for other purposes such as finding the largest palindromic rectangle in a matrix and finding the shortest partition of a string into palindromes.
Highly optimised algorithms are, in general, hard to understand. This is a consequence of the designer's sacrifice of clarity and modularity in favour of efficiency. In this paper we present a formal derivation of...
详细信息
The promotion strategy in transformational programming is a general method for achieving efficiency by exploiting the recursive structure in the dominant term of an algorithmic expression. For it to be carried out suc...
详细信息
An alternative taxonomy (to that of Knuth and others) of sorting algorithms is proposed. It emerges naturally out of a top-down approach to the derivation of sorting algorithms. Work done in automatic program synthesi...
详细信息
An alternative taxonomy (to that of Knuth and others) of sorting algorithms is proposed. It emerges naturally out of a top-down approach to the derivation of sorting algorithms. Work done in automatic program synthesis has produced interesting results about sorting algorithms that suggest this approach. In particular, all sorts are divided into two categories: hardsplit/easyjoin and easysplit/hardjoin. Quicksort and merge sort, respectively, are the canonical examples in these categories. Insertion sort and selection sort are seen to be instances of merge sort and quicksort, respectively, and sinking sort and bubble sort are in-place versions of insertion sort and selection sort. Such an organization introduces new insights into the connections and symmetries among sorting algorithms, and is based on a higher level, more abstract, and conceptually simple basis. It is proposed as an alternative way of understanding, describing, and teaching sorting algorithms. [ABSTRACT FROM AUTHOR]
Interest is increasing in the transformational approach to programming and in mechanical aids for supporting the program development process. Available aids range from simple editorlike devices to rather powerful inte...
详细信息
Interest is increasing in the transformational approach to programming and in mechanical aids for supporting the program development process. Available aids range from simple editorlike devices to rather powerful interactive transformation systems and even to automatic synthesis tools. This paper reviews and classifies transformation systems and is intended to acquaint the reader with the current state of the art and provide a basis for comparing the different approaches. It is also designed to provide easy access to specific details of the various methodologies. [ABSTRACT FROM AUTHOR]
暂无评论