Program checking

ABSTRACT

In languages such as Pascal, the programmer can arrange to have the compiler check such things as the range of the value of a variable only by defining a new type or sub-type. I have investigated how more powerful checking facilities might be provided if they were divorced from the type machinery, and also if the necessary language constructs were designed independent of what any particular compiler would check at compile-time. The first part of the project is the language design. An important goal is that the programmer can have checked as little or as much as he cares, and that it is not necessary for the programmer to specify complete input and output specifications for the program. My work falls short of program verification not only because I wanted to be able to check a program quickly, but also because I was unwilling to force the programmer to specify the program in that much detail. Current program verification systems, such as that of Constable [Constable and Johnson, 1978] seem to require that the programmer write the program twice: once as a program and again as a proof.

REFERENCES

• 1: Constable, Robert L. and Scott D. Johnson, "PL/CV2 Program verifier reference manual", Computer Science Department, Cornell University, March, 1978
• 2: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 3: Alan Demers , James Donahue , Glenn Skinner, Data types as values: polymorphism, type-checking, encapsulation, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.23-30, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512764]
• 4: Habermann, A. N., "Critical comments on the programming language PASCAL," Acta Informatica 3 (1973), 47-57.
• 5: Gary A. Kildall, A unified approach to global program optimization, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-206, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512945]
• 6: B. W. Lampson , J. J. Horning , R. L. London , J. G. Mitchell , G. J. Popek, Report on the programming language Euclid, ACM SIGPLAN Notices, v.12 n.2, p.1-79, February 1977 [doi>10.1145/954666.971189]
• 7: B Liskov , E Moss , A Snyder , R Atkinson , J C. Schaffert , T Bloom , R Scheifler, CLU reference manual, Springer-Verlag New York, Inc., New York, NY, 1984
• 8: Mitchell, James and Ben Wegbreit, "Schemes: A High Level Data Structuring Concept," Xerox Palo Alto Research Center, CSL-77-1, January 1977.
• 9: Wegbreit, Ben, "Property extraction in well-founded property sets", IEEE Transactions on Software Engineering, SE-1, 3, September 1975.
• 10: Wegbreit, Ben, "Constructive Methods in Program Verification", Xerox PARC, May 1976.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Design languages

General Terms:
Design, Languages, Verification