Richard A. De Millo
Alan J. Perlis
Abstract
It is argued that formal verifications of programs, no matter how obtained, will not play the same key role in the development of computer science and software engineering as proofs do in mathematics. Furthermore the absence of continuity, the inevitability of change, and the complexity of specification of significantly many real programs make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language design.
- 1 Baker, F.T. Chief programmer team management of production programming. IBM Syst. J. 11, 1 (1972), 56-73.Google Scholar
Digital Library
- 2 Cohen, P.J. The independence of the continuum hypothesis. Proc. Nat. Acad. Sci., USA. Part I, vol. 50 (1963), pp. 1143-1148; Part II, vol. 51 (1964), pp. 105-110.Google Scholar
- 3 Davis, P.J. Fidelity in mathematical discourse: Is one and one really two? The Amer. Math. Monthly 79, 3 (1972), 252-263.Google ScholarCross Ref
- 4 Bateman, P., and Diamond, H. John E. Littlewood (1885-1977): An informal obituary. The Math. lntelligencer 1, l (1978), 28-33.Google Scholar
- 5 Gelerenter, H., et al. The discovery of organic synthetic roots by computer. Topics in Current Chemistry 41, Springer-Verlag, 1973, pp. 113-150.Google Scholar
- 6 George, J. Alan. Computer Implementation of the Finite Element Method. Ph.D. Th., Stanford U., Stanford, Calif., 1971. Google ScholarDigital Library
- 7 Heath, Thomas L. The Thirteen Books of Euclid's Elements. Dover, New York, 1956, pp. 204-219. Google ScholarDigital Library
- 8 Heawood, P.J. Map colouring theorems. Quarterly J. Math., Oxford Series 24 (1890), 322-339.Google Scholar
- 9 Hoare, C.A.R. Quoted in Software Management, C. McGowan and R. McHenry, Eds.; to appear in Research Directions in Software Technology, M.I.T. Press, Cambridge, Mass., 1978.Google Scholar
- 10 Jech, Thomas J. The Axiom of Choice. North-Holland Pub. Co., Amsterdam, 1973, p. 118.Google Scholar
- 11 Kempe, A.B. On the geographical problem of the four colors. Amer. J. Math. 2 (1879), 193-200.Google ScholarCross Ref
- 12 Kolata, G. Bail. Mathematical proof: The genesis of reasonable doubt. Science 192 (1976), 989-990.Google ScholarCross Ref
- 13 Lakatos, Imre. Proofs and Refutations: The Logic of Mathematical Discovery. Cambridge University Press, England, 1976.Google ScholarCross Ref
- 14 Manin, Yu. I. A Course in Mathematical Logic. Springer-Verlag, 1977, pp. 48-51.Google Scholar
- 15 Meyer, A. The inherent computational complexity of theories of ordered sets: A brief survey. Int. Cong. of Mathematicians, Aug. 1974.Google Scholar
- 16 Popek, G., et al. Notes on the design of Euclid. Proc. Conf. Language Design for Reliable Software, SIGPLAN Notices (ACM) 12, 3 (1977), pp. 11-18. Google ScholarDigital Library
- 17 Rabin, M.O. Probabilistic algorithms. In Algorithms and Complexity: New Directions and Recent Results, J.F. Traub, Ed., Academic Press, New York, 1976, pp. 2140.Google Scholar
- 18 Schwartz, J. On programming. Courant Rep., New York U., New York, 1973.Google Scholar
- 19 Stockmeyer, L. The complexity of decision problems in automata theory and logic. Ph.D. Th., M.I.T., Cambridge, Mass., 1974.Google Scholar
- 20 Ulam, S.M. Adventures of a Mathematician. Scribner's, New York, 1976, p. 288.Google Scholar
Recommendations
Planning Proofs of Equations in CCS
Most efforts to automate formal verification of communicating systems have centred around finite-state systems (FSSs). However, FSSs are incapable of modelling many practical communicating systems, including a novel class of problems, which we call ...
Verification of Boolean programs with unbounded thread creation
Most symbolic software model checkers use abstraction techniques to reduce the verification of infinite-state programs to that of decidable classes. Boolean programs [T. Ball, S.K. Rajamani, Bebop: A symbolic model checker for Boolean programs, in: SPIN ...
Checking Program Proofs Made Easy
COMPSAC '95: Proceedings of the 19th International Computer Software and Applications ConferenceTo generate reliable software, it must be shown that a program meets its specifications. This can be done using program verification techniques. Assertions are made about the expected behavior of a program, and intermediate program states are examined ...
Comments