GDPA  
Refinement Calculus  

A-B-C- D-E-F- G-H-I- J-K-L- M-N-O- P-Q-R- S-T-U- V-W-X- Y-Z

Contents  
  • Identification
  • Observations
  • Classifications
  • Identification

    Refinement Calculus

    Observations

    The Refinement Calculus was described by Ralph Back in his 1978 Ph.D. thesis. This provides a general mathematical theory for the stepwise refinement approach to program construction. The refinement calculus extends the weakest precondition technique of Dijkstra to procedural and data refinement, and can also be used for stepwise refinement of parallel and distributed programs. Algorithms are derived by a series of correctness preserving refinements and program transformations from high-level specifications. The derivation is carried on until a program that meets the stated criteria of efficiency and implementability has been constructed

    Classifications

    Development Phases: Refinement

    GDPA Online Last Updated 01.Jan.2002 Updated by Webmaster Last Revised 01.Jan.2002 Revised by Webmaster