摘要
提出一种支持程序开发的结构化方法．该方法以一种简单的问题分解策略为基础，比Ｗｉｒｔｈ－Ｄｉｊｋｓｔｒａ的自顶向下逐步求精方法更利于面向目标的程序设计．由该方法可知，一个程序可经一系列求精而开发出来，每一步求精都能为相应的最弱前置条件序列建立后置条件．这种策略使情况分析减少到极限，简化了结构化程序的证明，并保证了程序结构和数据结构之间的对应．
This paper presentes a constructive method of program development. It is based on a simple strategy for problem decomposition that is claimed to be more supportive of goal-oriented programming than the Wirth-Dijkstra top-down refinement method. With the method,a program is developed by makeing a sequeue of refinements,each of which can establish the postcondition for a corresponding sequence of weaker preconditions. The strategy can minimize case analysis,simplefy constructive program proof,and ensure a correspondence between program structure and data structure.
关键词
面向目标
后置条件
软件开发
逐步求精
formal specification
goal-oriented programming
invarants
postconditions
program derivation
top-town refinement
weakest preconditions
