摘要
在结构化程序设计方法中,程序的生成过程是自顶向下的设计过程,即通过对其规格说明逐步求精而得。但是这种求精需要带有经验的思维和人的主观意识,可能通向目标,也可能走入歧途。本文试图通过Dijkstra 的最弱前置条件来定义规格说明的演算,从而给出逐步求精的一些形式化法则。
In structured programming,the generation of a program is a top-down design pro-cess.it is obtained by stepwise refining specification.However,the refinement processes are determinedby the programmer's experiences and ideas.In this paper a specification calculus is defined by usingDijkstra's weakest precondition semantics.The extention does this by providing one semantic frameworkfor specifications and programs.Developments begin with a program(a single specification statement)and end with a program(in the executable language).Finally the use of the calculus is illustrated byan example.
出处
《计算机研究与发展》
EI
CSCD
北大核心
1991年第3期23-28,共6页
Journal of Computer Research and Development
