检索结果-内蒙古大学图书馆

THE PROMOTION AND ACCUMULATION STRATEGIES IN transformational programming

ACM TRANSACTIONS ON programming LANGUAGES AND SYSTEMS 1984年第3期6卷 487-504页

作者： BIRD, RS Oxford University

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 successfully, the original problem often has to be generalized by the inclusion of an extra parameter, a technique known as accumulation. These strategies are illustrated by deriving algorithms for two nontrivial problems: (1) determining whether a given digraph is acyclic, and (2) constructing the longest subsequence of a given sequence of vertices that forms a connected path in a given digraph. The derivations also serve to emphasize the usefulness of certain notational devices in applicative expressions, especially infix operators. Not only do such operators enhance the succinctness and readability of expressions, they also allow many transformations to be formulated as algebraic laws about their distributive and other properties. © 1984, ACM. All rights reserved.

关键词： algorithm refinement operators transformational programming

来源：评论

学校读者我要写书评

暂无评论

Evaluating environments for functional programming

引用

INTERNATIONAL JOURNAL OF HUMAN-COMPUTER STUDIES 2000年第5期52卷 847-878页

作者： Whittle, J NASA 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 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.

关键词： functional programming transformational programming structure editors

来源：评论

学校读者我要写书评

暂无评论

Provably correct derivation of algorithms using FermaT

引用

FORMAL ASPECTS OF COMPUTING 2014年第5期26卷 993-1031页

作者： Ward, Martin Zedan, Hussein De Montfort Univ Software Technol Res Lab Leicester LE1 9BH Leics England

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.

关键词： transformational programming Formal methods Software development Algorithm derivation FermaT WSL

来源：评论

学校读者我要写书评

暂无评论

THE DERIVATION OF ONLINE ALGORITHMS, WITH AN APPLICATION TO FINDING PALINDROMES

引用

ALGORITHMICA 1994年第2期11卷 146-184页

作者： JEURING, J Utrecht University TB Utrecht The Netherlands

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.

关键词： DERIVATION OF ONLINE ALGORITHMS transformational programming BIRD-MEERTENS CALCULUS, SEGMENT PROBLEMS THEORY OF LISTS LONGEST PALINDROMIC SUBSTRING MAXIMAL PALINDROMES

来源：评论

学校读者我要写书评

暂无评论

Bridging the algorithm gap: A linear-time functional program for paragraph formatting

引用

SCIENCE OF COMPUTER programming 1999年第1期35卷 3-27页

作者： de Moor, O Gibbons, J Univ Oxford Programming Res Grp Oxford OX1 3QD England Oxford Brookes Univ Sch Comp & Math Sci Oxford OX3 0BP England

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.

关键词： paragraph formatting functional programming algorithm design sparse dynamic programming transformational programming

来源：评论

学校读者我要写书评

暂无评论

A fast pattern matching algorithm derived by transformational and assertional reasoning

引用

Formal Aspects of Computing 1990年第1期2卷 109-122页

作者： Partsch, H.A. Stomp, F.A. Department of Computer Science University of Nijmegen ED Nijmegen 6525 Toernooiveld 1 Netherlands

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 a rather ingenious algorithm, viz., the fast pattern matching algorithm of Boyer and Moore. The development illustrates that transformational programming combined with assertional reasoning provides an appropriate approach for developing and understanding highly optimised algorithms. © 1990 BCS.

关键词： Assertional reasoning Pattern matching Program transformation transformational programming

来源：评论

学校读者我要写书评

暂无评论

A Simple Inductive Synthesis Methodology and its Applications 10

A Simple Inductive Synthesis Methodology and its Application...

引用

Conference on Object Oriented programming Systems, Languages and Applications/SPLASH 2010

作者： Itzhaky, Shachar Gulwani, Sumit Immerman, Neil Sagiv, Mooly Tel Aviv Univ Tel Aviv Israel Univ Massachusetts Amherst MA 01003 USA Stanford Univ Stanford CA 94305 USA

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].

关键词： Languages Performance Finite Differencing High Level Program Inductive Synthesis transformational programming

来源：评论

学校读者我要写书评

暂无评论

AN INVERTED TAXONOMY OF SORTING ALGORITHMS

引用

COMMUNICATIONS OF THE ACM 1985年第1期28卷 96-99页

作者： MERRITT, SM School of Computer Science and Information Systems Pace University Graduate Center NY

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]

关键词： bottom-up top-down transformational programming

来源：评论

学校读者我要写书评

暂无评论

A definition of abstraction

引用

JOURNAL OF SOFTWARE MAINTENANCE-RESEARCH AND PRACTICE 1995年第6期7卷 443-450页

作者： Ward, M Computer Science Department Science Labs South Road Durham DH1 3LE U.K.

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.

关键词： abstraction software maintenance transformations refinement transformational programming

来源：评论

学校读者我要写书评

暂无评论

transformational DERIVATION OF A GARBAGE COLLECTION ALGORITHM

引用

ACM TRANSACTIONS ON programming LANGUAGES AND SYSTEMS 1982年第4期4卷 650-667页

作者： DEWAR, RBK SHARIR, M WEIXELBAUM, E TEL AVIV UNIV SCH MATH SCIIL-69978 TEL AVIVISRAEL

transformational programming is a relatively new programming technique intended to derive complex algorithms automatically. Initially, a set of transformational rules is described, and an initial specification of the problem to be programmed is given. The specification is written in a high-level language in a fairly compact form possibly ignoring efficiency. A number of versions, called transformations, are created by successively applying the transformational rules starting with the initial specification. As an example of the application of this technique to a fairly complex case, a transformational derivation of a variant of a known efficient garbage collection and compaction algorithm from an initial very high-level specification is given. Currently, the techniques are still being developed, and therefore the transformations are derived manually. However, most of the transformations done are of a technical nature and could eventually be automated. © 1982, ACM. All rights reserved.

关键词： formal differentiation garbage collection loop fusion strength reduction transformational programming wide-spectrum languages

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：