Unified Approach for Developing EfficientAlgorithmic Programs

A unified approach called partition-and-recur for developing efficient and correct algorithmic programs is presented.An algorithm(represented by recurrence and initiation)is separated from program,and special attention is paid to algorithm manipulation rather than proram calculus.An algorithm is exactly a set of mathematical formulae.It is easier for formal erivation and proof.After getting efficient and correct algorithm,a trivial transformation is used to get a final rogram,The approach covers several known algorithm design techniques,e.g.dynamic programming,greedy,divide-and-conquer and enumeration,etc.The techniques of partition and recurrence are not new.Partition is a general approach for dealing with complicated objects and is typically used in divide-and-conquer approach.Recurrence is used in algorithm analysis,in developing loop invariants and dynamic programming approach.The main contribution is combining two techniques used in typical algorithm development into a unified and systematic approach to develop general efficient algorithmic programs and presenting a new representation of algorithm that is easier for understanding and demonstrating the correctness and ingenuity of algorithmicprograms.     

A Knowledge-Based Approach to Program Synthesis from Examples

This paper proposes an approach to synthesize functional programs of Backus‘ FP system^[1,2] from input/output instances.Based on a theory of orthogonal expansion of programs^3[,4],the task of program synthesis is expressed in program equations,and fulfilled by solving them according to the knowledge about the equivalence between programs.Some general knowledge of solving program equations with a number of examples are given in the paper.     

Two New Strategies for Developing Loop Invariants and Their Applications

The loop invariants take a very important role in the design,proof and derivation of the algorithmic program.We point out the limitations of the taditional standard strategy for developing loop invariants.and propose two new strategies for proving the existing algorithmic program and developing new ones.The strategies ure recurrence as vehicle and integrate some effective methods of designing algorithms,e.g.Dynamic Porgramming,Greedy and Divide-Conquer,into the recurrence relation of problem solving sequence.This lets us get straightforward an approach for solving a variety of complicated problems,and makes the standard proof and formal derivation of their algorithmic programs possible.We show the method and advantages of applying the strategies with several typical nontivial examples.     

A Standard Model—Theoretic Approach to Operational Semmantics of Recursiv Programs

In this paper we try to introduce a new approach to operational semantics of recursive programs by using ideas in the“priority method”which is a fundamental tool in Recursion Theory.In lieu of modelling partial functions by introducing undefined values in a traditional approach,we shall define a priority derivation tree for every term,and by respecting thr rule“attacking the subtem of the highest priority first”we define transition relations,computation sequences etc.directly based on a standard interpretation whic includes no undefined value in its domain,Finally,we prove that our new approach generates the same opeational semantics as the traditional one.It is also pointed out that we can use our strategy oto refute a claim of Loeckx and Sieber that the opperational semantics of recursive programs cannot be built based on predicate logic.     

程序设计发展综述

从程序设计语言、程序设计方法、程序的集成开发环境等三方面来论述程序设计的发展过程,并指出了未来程序设计发展的三个方向。     

A New Synchronization Algorithm for VHDL-AMS Simulation

VHDL－AMS is the Analog and Mixed-Signal Extensions to VHDL.The paper gives a brief overview of the added features to VHDL.A mixed-signal simulator has been developed based on VHDL-AMS.A new synchronization algorithm is adopted in the simulator.Using the new algorithm the analog kernel does not need to synchronize the digital kernel at each digital event time point.The effciency of the new synchronization algorthm is tested by examples.Simulation results show the newly developed algorithm can speed up the simulation.     

A New Approach to Database Auto-Design by Logic

The database auto-design is an important problem in database research.In this paper we propose some new ideas and an approach called “logic approach” to implement the database auto-design.Given a relational scheme and a set of the functional dependencies for the relation we can obtain all of the functional dependencies and key for the relation and determine the normal form the relation satisfies.     

Formal Derivation of Graph AlgorithmicPrograms Using Partition-and-Recur

In this paper,we derive,by presenting some suitable notations,three typical graph algorithms and corresponding programs using a unified approach,partition-and-recur.We putemphasis on the derivation rather than the algorithms themselves.The main ideas and ingenuity of these algorithms are revealed by formula deduction.Success in these examples gives us more evidence that partition-and-recur is a simple and practical approach and developing enough suitable notations is the key in designing and deriving efficient and correct algorithmic programs.     

Optimizing FORTRAN Programs for Hierarchical Memory Parallel Processing Systems

Parallel loops account for the greatest amount of parallelism in numerical programs.Executing nested loops in parallel with low run-time overhead is thus very important for achieving high performance in parallel processing systems.However,in parallel processing systems with caches or local memories in memory hierarchies,“thrashing problemmay”may arise whenever data move back and forth between the caches or local memories in different processors.Previous techniques can only deal with the rather simple cases with one linear function in the perfactly nested loop.In this paper,we present a parallel program optimizing technique called hybri loop interchange(HLI)for the cases with multiple linear functions and loop-carried data dependences in the nested loop.With HLI we can easily eliminate or reduce the thrashing phenomena without reucing the program parallelism.     

若干算法程序的形式化推导与生成技术研究

PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C 等可执行程序.     

基于递推技术的算法设计方法的应用研究

算法是计算机科学的核心,算法设计对于开发正确、高效的程序至关重要。基于递推技术的算法设计方法通过形式化推导保证算法的可靠性,同时能较好地提高算法程序的效率。本文通过两个实例,详细介绍基于递推技术的算法设计方法形式化推导算法程序的过程。     

循环不变式开发新策略及其应用

循环不变式体现了循环程序的本质特征,在算法程序的开发、证明和推导中具有十分重要的作用。而传统的循环不变式开发策略并没有很好地解决循环不变式开发难的问题。文章在阐述现有策略局限性的基础上,详细阐述了刻画循环不变式本质特征的新定义及基于此定义的开发循环不变式的新策略,并通过三个典型的实例,对开发新策略的具体应用作了比较深入的探索。     

一种高效的算法程序设计方法-PAR方法

利用在长期的算法研究中提出的分划递推法（简称PAR方法）开发了三个问题的算法程序,说明PAR方法不仅为算法设计提供了统一而有效的途径,也为开发循环不变式奠定了基础。     

基于Isabelle定理证明器算法程序的形式化验证

形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值。     

PAR方法在组合游戏上的应用

简述了薛锦云教授所创的PAR方法和组合游戏(Nim)之后,本文运用PAR方法详细推演出解决组合游戏中的一个典型例子(Nim)的算法的数学模型。在此数学模型的基础之上,再次运用PAR方法推演出解决Nim的简短的核心算法。     

常用循环摘要的自动生成方法及其应用

采用形式化方法证明软件的正确性是保障软件可靠性的有效方法,而对循环语句的分析与验证是形式化证明中的关键,对循环语句的处理一直是程序分析与验证中的一个难点问题.本文提出使用循环语句修改的内存和这些内存中存放的新值来描述循环语句的执行效果,并将该执行效果定义为循环摘要.同时,本文提出了一种自动生成循环摘要的方法,可以为操作常用数据结构的循环自动生成循环摘要,包含嵌套循环.此外,基于循环摘要,我们可以自动生成循环语句的规约,包括循环不变式、循环的前置条件以及循环的后置条件.我们已经实现了自动生成循环摘要以及循环规约的方法,并将它们集成到验证工具Accumulator中,实验表明,我们的方法可以有效地生成循环摘要,并生成多种类型的规约,从而辅助软件程序的形式化证明,提高验证的自动化程度和效率,减轻验证人员的负担.