递归程序变换成非递归程序的方法

本文讨论将高级语言编写的递归程序自动地变换成非递归程序的变换规则和变换算法。     

递归程序变换及其实验

递归程序变换是软件自动化研究中程序变换途径的一种方法。本文介绍了递归程序等价变换的一系列模式以及根据递归程序变换基本思想而构造的人-机交互实验系统XDPTS的梗概。     

递归程序的非递归化

数学上早已证明：所有的递归算法都可以转化为迭代或循环算法。本文从分析递归程序特点出发．讨论了怎样利用迭代和堆栈来消除程序中的递归,从而提高程序的执行效率。     

关于递归程序变换模式的设计方法

本文提出递归程序变换模式的一般设计方法，并以具体示例说明之。此外，还对递归程序变换的有关问题作了讨论。     

数据结构下的程序递归算法设计及应用

在数据结构基础上使用程序递归算法设计是目前进行软件开发应用最广泛的方法.使用递归算法进行程序编写可以减少很多操作细节,从而简化程序编写,而且递归算法结构简单且清晰,易读性比较强,最大的优势递归算法正确率高、验证比较方便.对递归程序算法的应用进行了分析,并探讨了递归算法的实现策略.     

线性递归Da taL og 程序优化算法

提出了线性齐次ＤａｔａＬｏｇ逻辑程序的概念,并为该类程序设计了一个优化的求解算法。在此基础上提出了求解一般线性ＤａｔａＬｏｇ程序的优化算法,该算法利用带有的约束条件的递归调用方法,将线性ＤａｔａＬｏｇ程序求解问题变换成齐次程序的求解问题。算法简单,易于实现,可应用于任何线性ＤａｔａＬｏｇ程序的求解。     

用VB编写递归程序

讨论了递归算法的基本概念和原理,使用VB,给出了设计编写递归程序的方法。     

基于递归程序到非递归程序转换的实现

基于递归程序时空性能不好的缺点,提出了用非递归方法来解决递归问题的实现方法.     

递归Prolog程序终止问题的探讨

本文用Ｐｒｏ图的方法讨论了递归Ｐｒｏｌｏｇ程序的终止问题。其中包括Ｐｒｏ图的概念和Ｐｒｏ图的状态序列及递归程序的终止问题。使用本文的方法可为调试程序提供足够的启示。     

递归问题的非递归实现方法研究与应用

使用非递归方式实现递归问题的算法程序,不仅可以节省存储空间,而且可以极大地提高算法程序的执行效率。本文给出了两种将递归问题的递归算法转换成非递归算法的有效方法,并以具体实例加以说明。     

Building program construction and verification tools from algebraic principles

We present a principled modular approach to the development of construction and verification tools for imperative programs, in which the control flow and the data flow are cleanly separated. Our simplest verification tool uses Kleene algebra with tests for the control flow of while-programs and their standard relational semantics for the data flow. It is expanded to a basic program construction tool by adding an operation for the specification statement and one single axiom. To include recursive procedures, Kleene algebras with tests are expanded further to quantales with tests. In this more expressive setting, iteration and the specification statement can be defined explicitly and stronger program transformation rules can be derived. Programming our approach in the Isabelle/HOL interactive theorem prover yields simple lightweight mathematical components as well as program construction and verification tools that are correct by construction themselves. Verification condition generation and program construction rules are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving. A number of examples shows our tools at work.     

最小生成树算法的PAR方法形式化推导

采用PAR方法通过功能归约变换，形式化推导出可读性好、效率高的递推的最小生成树算法，简化了算法程序设计和正确性证明的过程，有效提高了算法程序设计自动化、规范化的程度及其正确性。该文给出的相关算法在PAR平台通过自动转换系统转换成可执行语言程序并运行通过。     

Formal program construction by transformations-computer-aided,intuition-guided programming

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     

Parallelization of divide-and-conquer in the Bird-Meertens formalism

An SPMD parallel implementation schema for divide-and-conquer specifications is proposed and derived by formal refinement (transformation) of the specification schema. The specification is in the form of a mutually recursive functional definition. In a first phase, a parallel functional program schema is constructed which consists of a communication tree and a functional program that is shared by all nodes of the tree. The fact that this phase proceeds by semantics-preserving transformations in the Bird-Meertens formalism of higher-order functions guarantees the correctness of the resulting functional implementation. A second phase yields an imperative distributed message-passing implementation of this schema. The derivation process is illustrated with an example: a two-dimensional numerical integration algorithm.Parts of this paper were presented at the International Parallel Processing Symposium, Mexico, 1994 [GoL94] and at the World Transputer Congress, Italy, 1994 [Gor94]     

序列折半划分问题的形式化推导

形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序。针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序。为解决上述问题,提出了一种新的序列折半划分问题的形式化推导方法。该方法基于分划递推的核心思想,应用规约变换技术对问题规约进行变换并严格保证一致性,使得在推导过程中无需交替证明,进而导出递推关系式并得到高可靠性抽象算法程序Apla,最终通过转换工具自动生成可执行程序。实现了从程序规约到具体可执行程序的完整程序求精过程。以2个序列算法为例,验证了该方法的有效性和可行性,对相关问题的形式化推导具有指导意义。     

A logic-based transformation system

In spite of advances in various transformation systems the transformation of a nonmonotonic-logic-based requirements specification into a procedural (imperative) language program has not been investigated. This paper presents a logic-based transformation system that can transform a nonmonotonic-logic-based specification, the Frame-and-Rule Oriented Requirement Specification Language (FRORL), into procedural language programs. We discuss how to handle nonmonotonic inheritance in FRORL and then establish a matrix-based data flow and dependency analysis mechanism to find all the possible data transformation paths in a logic-based specification. Using a newly developed algorithm, we can adjust the execution sequence of a logic-based specification so that the functions included in the logic-based specification can be represented by a sequential procedural language program     

基于Tableau方法的程序综合系统——DTPS

本文简单介绍了基于Ｔａｂｌｅａｕ方法的程序综合系统－ＤＴＰＳ．ＤＴＰＳ系统以定理证明为基础，为构造一个满足程序规约的程序，只需证明的确存在一个满足条件的对象。如果这个证明存在，那么从证明中可抽取出一个满足该程序规约的程序。     

Derivation of data intensive algorithms by formal transformation:the Schnorr-Waite graph marking algorithm

Considers a particular class of algorithms which present certain difficulties to formal verification. These are algorithms which use a single data structure for two or more purposes, which combine program control information with other data structures or which are developed as a combination of a basic idea with an implementation technique. Our approach is based on applying proven semantics-preserving transformation rules in a wide spectrum language. Starting with a set theoretical specification of “reachability”, we are able to derive iterative and recursive graph marking algorithms using the “pointer switching” idea of Schorr and Waite (1967). There have been several proofs of correctness of the Schorr-Waite algorithm, and a small number of transformational developments of the algorithm. The great advantage of our approach is that we can derive the algorithm from its specification using only general-purpose transformational rules, without the need for complicated induction arguments. Our approach applies equally well to several more complex algorithms which make use of the pointer switching strategy, including a hybrid algorithm which uses a fixed length stack, switching to the pointer switching strategy when the stack runs out     

Program Reusability through Program Transformation

How can a program written in pure applicative LISP be reused in a Fortran environment? One answer is by automatically transforming it from LISP into Fortran. In this paper we discuss a practical application of this technique-one that yields an efficient Fortran program. We view this process as an example of abstract programming, in which the LISP program constitutes an abstract specification for the Fortran version. The idea of strategy-a strategy for getting from LISP to Fortran-is basic to designing and applying the transformations. One strategic insight is that the task is easier if the LISP program is converted to ``recursive' Fortran, and then the recursive Fortran program is converted to nonrecursive standard Fortran. Another strategic insight is that much of the task can be accomplished by converting the program from one canonical form to another. Developing a strategy also involves making various implementation decisions. One advantage of program transformation methodology is that it exposes such decisions for examination and review. Another is that it enables optimizations to be detected and implemented easily. Once a strategy has been discovered, it can be implemented by means of rewrite-rule transformations using the TAMPR program transformation system. The transformational approach to program reuse based on this strategy has a measure of elegance. It is also practical-the resulting Fortran program is 25 percent faster than its compiled LISP counterpart, even without extensive optimization.     

Generation of parallel programs from nonprocedural specifications

The paper describes a formalization of the process of transition from a specification in the form of a system of recursive equations on structured data to a parallel program realizing the specification. Formal optimizing transformations of specifications are proposed.Translated from Kibernetika, No. 1, pp. 7–12, January–February, 1990.