A phased programming paradigm

ABSTRACT

Correctness and efficiency are both legitimate concerns in program development. Through an extended example we present a multi-phase paradigm which encourages early algorithms to be abstract and maximally nondeterministic in the spirit of Dijkstra's guarded commands [4] but which caters equally for correctness, termination, data representation, efficiency and practical implementation in a low level language.

REFERENCES

• 1: E. W. Dijkstra, "Notes on Structured Programming" in Structured P.r.ogrammin..g by Dahl, Dijkstra and Hoare, Academic press, 1972.
• 2: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 3: C. A. R. Hoare and N. Wirth, "An axiomatic definition of the programming language Pascal", Acta Informatica 2(1973), pp. 335-355.
• 4: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 5: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 6: Jon Louis Bentley, Writing Efficient Programs, Prentice Hall PTR, Upper Saddle River, NJ, 1982
• 7: Donald E. Knuth, The art of computer programming, volume 3: (2nd ed.) sorting and searching, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1998

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.10 Design**
            Subjects: Methodologies**; Representation**
      D.2.8 Metrics
          Subjects: Performance measures

General Terms:
Design, Verification