From Specification to Program:The Formal Description of Refinement

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.