Specification-consistent coordination model for computations
Edgar F. A. Lederer, Romeo A. Dumitrescu · 1998
A new coordination model for computations is presented. It offers increased confidence in the correctness of imperative programs and considerable simplification of imperative programming and debugging. In this model, programs consist of formal specifications of computations by recursive function definitions and explicit mappings (coordinations) of these specifications to imperative programs. The consistency between coordination and specification is guaranteed by a special mechanism, called the consistency checker, during the program's execution. It automatically detects any inconsistency by comparisons against symbolic names associated with values. The formal specification of Gaussian elimination and two coordinations that implement a sequential and a parallel algorithm are used to present the model. 1 INTRODUCTION Imperative programming is widely used for expressing scientific computations. It has the advantage of per- Copyright c fl1998 by the Association for Computing Machinery...