Toward a theory of correct set algorithms

ABSTRACT

A structured pseudocode containing only eight primitive instructions is described for expressing algorithms about sets, relations, functions, natural numbers, algebras, graphs, etc. The language has been used to treat algorithms in courses on discrete mathematics. In the language, algorithms that compute set-theoretic predicates are distinguished from algorithms that compute set operators. Also, algorithms are distinguished from the specifications of algorithms and formal proofs of correctness serve to interrelate the two. Finally, specifications are allowed within statements to invoke subalgorithms. To illustrate the approach, a representative number of set algorithms are given and proved correct including the topological sorting algorithm.

REFERENCES

• 1: J. L. Kelley, I~eneral Top..ELQI gy, Van Nostrand, Princeton, New Jersey, 1955 (appendix).
• 2: P. Suppes, Axiomatic Set Theory, Van Nostrend, Princeton, New Jersey, 1960.
• 3: T. G. Windeknecht, Mathematical Foundations Of Computer Science(Theorems, Pro~f~,_~ Algorithms)., (submitted for publication), 1987.
• 4: J. T. Schwartz , R. B. Dewar , E. Schonberg , E. Dubinsky, Programming with sets; an introduction to SETL, Springer-Verlag New York, Inc., New York, NY, 1986
• 5: T. G. Windeknecht, "An Introduction To Set Algorithms," Technical Report No. TR-CSE-87-10, Oakland University, Rochester, Michigan 48063, October 1987.

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

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

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Set theory

General Terms:
Algorithms, Design, Performance, Reliability, Theory, Verification