由规格说明到排序算法

From Specification to Sorting Algorithms

本文给出由程序的规格说明变换出程序的一种系统化方法的新概念.对规格说明进行不同的变换可得到不同的不变式形式.这些不变式通过计算最弱前置条件给出了多种相应算法的框架。本文以若干著名的排序算法例示了以上的概念和方法。

This paper gives some new ideas, which is that transformations on a program specification provide a systematic method for programming .Different transformations on the specification can give new and al ernative forms of invariants. These invariant can provide the framework for the transformation of a variety of algorithms by use of weakest precondition techniques. This paper gives some well-known sorting algorithms to be transform from original program specification to demonstrate above ideas and method.