| | This Article | |
| |
| |
| | Share | |
| |
| |
| | Bibliographic References | |
| |
| |
| | Add to: | |
| |
 Digg
 Furl
 Spurl
 Blink
 Simpy
 Google
 Del.icio.us
 Y!MyWeb
| |
| | Search | |
| |
| |
| | |
Formal Verification of Ada Programs
September 1990 (vol. 16 no. 9)
pp. 1058-1075
The Penelope verification editor and its formal basis are described. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich subset of sequential Ada. Because it generates verification conditions incrementally, Penelope can be used to develop a program and its correctness proof in concert. If an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original sequence of proof steps. Verification conditions are generated by predicate transformers whose logical soundness can be proven by establishing a precise formal connection between predicate transformation and denotational definitions in the style of continuation semantics. Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. It scales up properly, in the sense that one can demonstrate the soundness of decomposing an implementation hierarchically and reasoning locally about the implementation of each node in the hierarchy.
[1] 1058The Programming Language Ada Reference Manual, ANSI/MIL-STD-1815A, 1983.[2] E. R. Anderson, B. Di Vito, and R. M. Hart, "ASOS: Information security for real-time systems," inProc. AFCEA West Intelligence Symp., 1987.[3] E. Astesianoet al., "Draft formal definition of Ada," CRAI, DDC, Tech. Rep., 1987 (Deliverable 7 of the CED MAP project).[4] H. Barringer, J. H. Cheng, and C. B. Jones, "A logic covering undefinedness in program proofs,"Acta Inform., vol. 21, 1984.[5] H.-J. Boehm, "Side-effects and aliasing can have simple axiomatic descriptions,"ACM Trans. Program. Lang. Syst., vol. 7, no. 4, Oct. 1985.[6] R. S. Boyer and J. S. Moore,A Computational Logic Handbook. Boston, MA: Academic, 1988.[7] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: Prentice-Hall, 1976.[8] R. Floyd, "Assigning meaning to programs," inMathematical Aspects of Computer Science XIX. Amer. Math. Soc., 1967, pp. 19-32.[9] R. Gerth, "A sound and complete Hoare axiomatization of the Ada rendezvous," inProc. 9th ICALP(Lecture Notes in Computer Science, vol. 140). New York: Springer-Verlag, 1982, pp. 252-264.[10] J. A. Goguen and R. M. Burstall,Introducing Institutions(Lecture Notes in Computer Science, vol. 164). New York: Springer-Verlag, 1984.[11] D. Good, "Revised report on Gypsy 2.1 (draft)," Univ. Texas. Tech. Rep., July 1984.[12] D. Gries,The Science of Programming. New York: Springer-Verlag, 1981.[13] D. Guaspari, "Formal semantics of two-tiered specifications," Odyssey Research Associates, Tech. Rep. 89-35 (original no. 17-14), Sept. 1989.[14] J. V. Guttag, J. J. Horning, and J. M. Wing, "Larch in five easy pieces," DEC/SRC. Tech. Rep. TR 5, July 1985.[15] C. A. R. Hoare, "An axiomatic basis for computer programming,"Commun. ACM, vol. 12, no. 10, pp. 576-583, 1969.[16] C. A. R. Hoare, "Proof of correctness of data representations,"Acta Inform., vol. 1, no. 1, pp. 271-281, 1972.[17] S. Katz and Z. Manna, "A closer look at termination,"Acta Inform., vol. 5, pp. 333-352, 1975.[18] C. Landwehr, "The rs-232 software repeater problem,"Cipher: Newslett. IEEE Tech. Committee Security and Privacy.[19] D. C. Luckhamet al., "Stanford Pascal verifier user manual," Stanford Univ., Tech. Rep. STAN-C-79-731, Mar. 1979.[20] D. C. Luckham and W. Polak, "Ada exception handling: An axiomatic approach,"ACM Trans. Program. Lang. Syst., vol. 2, no. 2, pp. 225-233, Apr. 1980.[21] D. C. Luckhamet al., "Anna: A language for annotating Ada programs" (Reference Manual), Stanford Univ., Tech. Rep. CSL-84- 261, 1986.[22] C. Marceau and C. D. Harper, "An interactive approach to Ada verification," inProc. 12th NBS/NCSC Nat. Computer Security Conf., MBS/NCSC, Oct. 1989.[23] D. R. Musser, "Abstract data type specifications in the AFFIRM system," inProc. Specifications of Reliable Software, Apr. 1979, pp. 47-57.[24] G. Nelson and D. C. Oppen, "Simplification by cooperating decision procedures,"ACM Trans. Program. Lang. Syst., vol. 1, no. 2, pp. 245-257, Oct. 1979.[25] W. Polak, "Program verification based on denotational semantics," inConf. Rec. Eighth Annu. ACM Symp. Principles of Programming Languages, 1981.[26] W. Polak, "Predicate transformer semantics for Ada," Odyssey Research Associates, Tech. Rep. 89-39 (original no. 17-12), Sept. 1989.[27] W. Polak, "A technique for defining predicate transformers," Odyssey Research Associates, Tech. Rep. 89-53 (original no. 17-4), 1989.[28] T. Redmond, "Simplifier description," Aerospace, Tech. Rep. ATR- 86A (8554)-2, Nov. 1987.[29] T. Reps and B. Alpern, "Interactive proof checking," inConf. Rec. Eleventh Annu. ACM Symp. Principles of Programming Languages, Salt Lake City, UT, Jan. 1984, pp. 36-45.[30] T. W. Reps and T. Teitelbaum,The Synthesizer Generator: A System For Constructing Language-Based Editors. New York: Springer-Verlag, 1988.[31] O. Schoett, "Data abstraction and the correctness of modular programming," Ph.D. dissertation, Univ. Edinburgh, Rep. CST-42-87, 1987.[32] E. Schonberg and B. Siritzky, "Adasem, static semantics for Ada," Dep. Comput. Sci., Courant Inst. Math. Sci., New York Univ., Tech. Rep., 1984.[33] R. L. Schwartz, "An axiomatic treatment of Algol68 routines," inProc. Sixth Int. Conf. Automata, Languages and Programming. New York: Springer-Verlag, 1979.[34] J. M. Wing, "Writing Larch interface language specifications,"ACM Trans. Program. Lang. Syst., vol. 9, no. 1, pp. 1-24, Jan. 1987.[35] S. Yemini and D. M. Berry, "An axiomatic treatment of exception handling in an expression-oriented language,"ACM Trans. Program. Lang. Syst., vol. 9, no. 3, July 1987.
Index Terms:
Ada programs; Penelope verification editor; formal basis; prototype system; interactive development; correctness proof; predicate transformers; logical soundness; interface languages; Ada; program verification; software engineering.
Citation:
D. Guaspari, C. Marceau, W. Polak, "Formal Verification of Ada Programs," IEEE Transactions on Software Engineering, vol. 16, no. 9, pp. 1058-1075, Sept. 1990, doi:10.1109/32.58790
