高级检索

    从规格说明到程序:逐步求精的形式描述

    From Specification to Program:The Formal Description of Refinement

    • 摘要: 在结构化程序设计方法中,程序的生成过程是自顶向下的设计过程,即通过对其规格说明逐步求精而得。但是这种求精需要带有经验的思维和人的主观意识,可能通向目标,也可能走入歧途。本文试图通过Dijkstra 的最弱前置条件来定义规格说明的演算,从而给出逐步求精的一些形式化法则。

       

      Abstract: 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.

       

    /

    返回文章
    返回