Some correctness principles for machine language programs and microprograms

ABSTRACT

A machine-language program, or a microprogram implemented in writable control store, may modify itself. In order to prove the correctness of such a program, we must take this into account. Even if the program does not modify itself, we must prove this. Sometimes this may be done by looking at the individual instructions of the program; sometimes it must be tied in with the proof of correctness of the program. We state here, and illustrate by examples, certain principles for proving the correctness of programs and microprograms under these conditions. The principles are extensions to the standard inductive assertion method.

REFERENCES

• 1: Floyd, R. W., Assigning meanings to programs, Proc. Symp. Applied Math. 19 (Mathematical Aspects of Computer Science), American Mathematical Society, Providence, R. I., 1967, pp. 19-32.
• 2: Donald E. Knuth, The art of computer programming, volume 1 (3rd ed.): fundamental algorithms, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1997
• 3: James Cornelius King, A program verifier, 1970
• 4: Deutsch, L. P., An interactive program verifier, Ph.D. Thesis, Department of Computer Science, University of California, Berkeley, May 1973.
• 5: Manna, Z., The correctness of programs, J. Computer and Systems Sci. 3, 2 (1969), pp. 119-127.
• 6: 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]
• 7: Maurer, W. D., Introduction to programming science, Part I: Syntax and semantics of programming languages, Memorandum No. ERL-M368, U. of Calif. (Berkeley), Dec. 1972.
• 8: Maurer, W. D., Introduction to programming science, Part II: Proofs of assertions about programs, Memorandum No. ERL-M394, U. of Calif. (Berkeley), August 1973.
• 9: Ward Douglas Maurer, Induction Principles for Context-Free Languages, Gesellschaft für Informatik e.V., 3. Jahrestagung, p.134-143, October 08-10, 1973
• 10: Knuth, D. E., Semantics of context-free languages, Mathematical Systems Theory 2, 2 (1968), pp. 127-145; correction, Mathematical Systems Theory 5,1 (1971), pp. 95-96.
• 11: McCarthy, J., Towards a mathematical science of computation, Information Processing 19621 (Proc. of IFIP Congress 62), North-Holland, Amsterdam, 1963, pp. 21-28.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.0 GENERAL
      Subjects: Instruction set design (e.g., RISC, CISC, VLIW)

Additional Classification:
  B. Hardware
  B.1 CONTROL STRUCTURES AND MICROPROGRAMMING
      B.1.4 Microprogram Design Aids

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Assertions

General Terms:
Design