A Theoretical Basis for Stepwise Refinement and the Programming Calculus
A Theoretical Basis for Stepwise Refinement and the Programming Calculus
复制标题
逐步求精和编程演算的理论基础
DOI：
10.1016/0167-6423(87)90011-6
复制
发表时间：
1987
期刊：
影响因子：
--
通讯作者：
Joseph M. Morris
中科院分区：
文献类型：
--
作者：
Joseph M. Morris
提出了对规范、程序和编程的统一处理。处理的基础是向给定的过程语言添加规范语句并定义其语义。因此，扩展语言是一种规范语言，程序被视为规范的子类。定义了对应于‘More Defined’的规格/节目的部分排序。在这种偏序中，通过逐步细化在程序的构造中出现的程序/规范混合形成单调序列。我们展示了Dijkstra的程序派生演算如何对应于构造这个单调序列。因此，将微积分形式化使我们对它所需要的智力活动有了一些洞察，并使我们能够暗示进一步的发展。
A uniform treatment of specifications, programs, and programming is presented. The treatment is based on adding a specification statement to a given procedural language and defining its semantics. The extended language is thus a specification language and programs are viewed as a subclass of specifications. A partial ordering on specifications/programs corresponding to ‘more defined’ is defined. In this partial ordering the program/specification hybrids that arise in the construction of a program by stepwise refinement form a monotonic sequence. We show how Dijkstra's calculus for the derivation of programs corresponds to constructing this monotonic sequence. Formalizing the calculus thus gives some insight into the intellectual activity it demands and allows us to hint at further developments.