×

Program derivation with verified transformations – a case study. (English) Zbl 0853.68072

Summary: A program development methodology based on verified program transformations is described and illustrated through derivations of a high level bisimulation algorithm and an improved minimum-state DFA algorithm. Certain doubts that were raised about the correctness of an initial paper-and-pencil derivation of the DFA minimization algorithm were laid to rest by machine-checked formal proofs of the most difficult derivational steps. Although the protracted labor involved in designing and checking these proofs was almost overwhelming, the expense was somewhat offset by a successful reuse of major portions of these proofs. In particular, the DFA minimization algorithm is obtained by specializing and then extending the last step in the derivation of the high level bisimulation algorithm.
Our experience suggests that a major focus of future research should be aimed towards improving the technology of machine checkable proofs – their construction, presentation, and reuse. This paper demonstrates the importance of such a technology to the verification of programs and program transformations. We believe that the utility of transformational systems to program development will ultimately rest on a practical program correctness technology.

MSC:

68N15 Theory of programming languages
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

LARCH
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] ADA UK News 6 pp 14– (1985)
[2] , and , Design and Analysis of Computer Algorithms, Addison-Wesley, Reading, Massachusetts, 1974.
[3] and , Algorithmic Language and Program Development, Springer-Verlag, Berlin, 1982. · doi:10.1007/978-3-642-61807-9
[4] and , Models and Ultraproducts, North-Holland, Amsterdam, 1969.
[5] , and , The DevaWEB System, Technical Report 93–39, Technische Universität Berlin, December 1993.
[6] and , VDM’87, Springer-Verlag, Berlin, 1987.
[7] Bloom, Sci. Comput. Programming 24 pp 189– (1995)
[8] and , A Computational Logic, Academic Press, New York, 1979.
[9] Experiences with Software Specification and Verification Using LP, the Larch Proof Assistant, Research Report 93, DEC Systems Research Center, Palo Alto, California, 1992.
[10] and , A transformation system for developing recursive programs, J. ACM 24, No. 1, January 1977, pp. 44–67. · Zbl 0343.68014
[11] , , , and , Type transformation and data structure choice, pp. 126–124 in: Constructing Programs From Specifications, ed., North-Holland, Amsterdam, 1991.
[12] Cai, Sci. Comput. Programming 11 pp 197– (1988/1989)
[13] , and , Computable Set Theory, Clarendon Press, Oxford, 1989.
[14] Cardon, Theoret. Comput. Sci. 19 pp 85– (1982)
[15] and , A laboratory for the study of automating programming, pp. 208–211 in: Proceedings AFIPS 1972 Spring Joint Computer Conference, 1972.
[16] Chen, ACM TODS 1 (1976)
[17] Cocke, CACM 20 pp 850– (1977) · Zbl 0361.68030 · doi:10.1145/359863.359888
[18] and , Programming Languages and Their Compilers, Lecture Notes, Courant Institute, New York University, New York, 1969.
[19] Coquand, Inform. and Comput. 76 pp 95– (1988)
[20] and , Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixed points, pp. 238–252 in: Proceedings Fourth ACM Symposium on Principles of Programming Languages, 1977.
[21] Cousot, Pacific J. Math. 82 pp 43– (1979) · Zbl 0413.06004 · doi:10.2140/pjm.1979.82.43
[22] and , Semantic foundations of program analysis, pp. 303–342 in: Program Flow Analysis, and , eds., Prentice Hall, Englewood Cliffs, New Jersey, 1981.
[23] Obvious logical inferences, pp. 530–531 in: Proceedings of IJCAI 81, 1981.
[24] Davis, Comp. Math. Appl. 5 pp 217– (1979)
[25] A Transformational Approach to the Development and Verification of Programs in a Very High Level Language, Courant Computer Science Report 22, Courant Institute, New York University, New York, November 1980.
[26] TYPOL a Formalism to Implement Natural Semantics, Research Report, INRIA, Sophia Antipolis, France, 1986.
[27] A Discipline of Programming, Prentice Hall, Englewood Cliffs, New Jersey, 1976. · Zbl 0368.68005
[28] Dijkstra, BIT 8 pp 174– (1968)
[29] and , SETL to Ada tree transformations applied, Inform. Software Tech. 29, No. 10, December 1987, pp. 548–557.
[30] , , and , Development of a programming environment for SETL, pp. 21–32 in: Proceedings ESEC 87, and , eds., LNCS Vol. 289, Springer-Verlag, Berlin, 1987.
[31] , , , and , Outline of a tool for document manipulation, pp. 615–620 in: IFIP ’83, North-Holland Elsevier, Amsterdam, 1983.
[32] Determination statique des types pour le langage SETL, Doctoral Dissertation, CNAM, Paris, France, 1989.
[33] Earley, J. Comput. Languages 1 pp 321– (1976)
[34] Fernandez, Sci. Comput. Programming 13 pp 219– (1989/90)
[35] and , Induction variables in very high level languages, pp. 104–112 in: Proceedings Third ACM Symposium on Principles of Programming Languages, January 1976.
[36] Freudenberger, ACM TOPLAS 5 pp 26– (1983)
[37] and , A Guide to LP, the Larch Prover, Research Report 82, DEC Systems Research Center, Palo Alto, California, 1991.
[38] and , eds., Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic, Cambridge University Press, 1993. · Zbl 0779.68007
[39] Gries, Acta Inform. 2 pp 97– (1973)
[40] The Science of Programming, Springer-Verlag, New York, 1981. · Zbl 0472.68003 · doi:10.1007/978-1-4612-5983-1
[41] and , Larch: Languages and Tools for Formal Specification, Springer-Verlag, New York, 1993, with S. Garland, K. Jones, A. Modet, and J. Wing. · doi:10.1007/978-1-4612-2704-5
[42] Harel, CACM 31 pp 514– (1988) · doi:10.1145/42411.42414
[43] Hoare, CACM 12 pp 576– (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[44] An n log n algorithm for minimizing states in a finite automaton, pp. 189–196 in: Theory of Machines and Computations, and , eds., Proceedings International Symposium on Theory of Machines and Computation, Academic Press, New York, 1971. · doi:10.1016/B978-0-12-417750-5.50022-1
[45] Natural Semantics, Research Report, INRIA, Sophia Antipolis, France, 1987.
[46] Kanellakis, Inform. and Comput. 86 pp 43– (1990)
[47] Cantor: A Tutorial and a User’s Guide, Education Report 94/9, Kepler, Paris, 1994.
[48] and , Algorithm Design and Verifiable APTS Transformational Derivations with NAP, Research Report 94/11, Kepler, Paris, 1994.
[49] How to Write a Proof, Technical Report 94, DEC Systems Research Center, Cambridge, Massachusetts, February 1993. · Zbl 1041.00501
[50] A Calculus of Communicating Systems, Lecture Notes in Computer Science, Vol. 92, Springer-Verlag, Berlin, 1980. · doi:10.1007/3-540-10235-3
[51] Milner, Theoret. Comput. Sci. 25 pp 267– (1983)
[52] Finite Automata and the Representation of Events, WADD TR-57-624, Wright Patterson AFB, Ohio, 1957.
[53] Nerode, Proc. Amer. Math. Soc. 9 pp 541– (1958)
[54] 1994, private communication.
[55] Real-time simulation of a set machine on a ram, pp. 69–73 in: Computing and Information, and , eds., Vol. II, Canadian Scholars’ Press, Toronto, May 1989.
[56] Efficient translation of external input in a dynamically typed language, pp. 603–608 in: Technology and Foundations – Information Processing 94, and , eds., Vol. 1 of IFIP Transactions A-51, Conference Record of IFIP Congress 94, North-Holland, Amsterdam, September 1994.
[57] Viewing a program transformation system at work, pp. 5–24 in: Programming Language Implementation and Logic, and , eds., LNCS Vol. 844, Springer-Verlag, Berlin, September 1994, Proceedings Joint 6th International Conference on Programming Language Implementation and Logic Programming (PLILP) and 4th International Conference on Algebraic and Logic Programming (ALP). · doi:10.1007/3-540-58402-1_3
[58] Paige, ACM Trans. Programming Languages and Systems 4 pp 401– (1982)
[59] and , Expression continuity and the formal differentiation of algorithms, pp. 58–71 in: Proceedings 4th ACM Symposium on Principles of Programming Languages, January 1977.
[60] Paige, SIAM J. Comput. 16 pp 973– (1987)
[61] Isabelle: The next 700 theorem provers, pp. 361–386 in: Logic and Computer Science, ed., Academic Press, New York, 1990.
[62] Pepper, Sci. Comput. Programming 9 pp 221– (1987)
[63] and , Korso: A Methodology for the Development of Correct Software, Technical Report 93–36, Technische Universität Berlin, November 1994.
[64] Formal software development in the KIV system, in: KORSO: Methods, Languages, and Tools for the Construction of Correct Software, and , eds., LNCS Vol. 1009, Springer-Verlag, Berlin, 1995.
[65] The KIV-approach to software verification, in: KORSO: Methods, Languages, and Tools for the Construction of Correct Software, and , eds., LNCS Vol. 1009, Springer-Verlag, Berlin, 1995.
[66] , and , Interactive correctness proofs for software modules using KIV, pp. 151–162 in: Compass 95, Proceedings of the 10th Annual Conference on Computer Assurance, 1995.
[67] , , , and , eds., Object-Oriented Modeling and Design, Prentice Hall, Englewood Cliffs, New Jersey, 1991.
[68] Total correctness by local improvement in program transformation, pp. 221–232 in: Proceedings of the 22nd ACM Symposium on Principles of Programming Languages, January 1995.
[69] , and , An automatic technique for selection of data representations in SETL programs, ACM TOPLAS 3, No. 2, April 1981, pp. 126–143. · Zbl 0452.68010
[70] On Programming: An Interim Report on the SETL Project, Installments I and II, New York University, New York, 1974.
[71] Schwartz, CACM 18 pp 722– (1975) · Zbl 0316.68012 · doi:10.1145/361227.361235
[72] Schwartz, J. Comput. Languages 1 pp 161– (1975)
[73] On correct program technology, pp. 120–146 in: Two Papers on Program Verification, Courant Computer Science Report No. 12, Courant Institute, New York University, New York, September 1977.
[74] , , and , Programming with Sets: An Introduction to SETL, Springer-Verlag, New York, 1986. · Zbl 0604.68001
[75] Sharir, ACM TOPLAS 4 (1982)
[76] Measuring SETL Performance, Doctoral Dissertation, Computer Science Department, New York University, 1983.
[77] Mathematical Logic, Addison-Wesley, Reading, Massachusetts, 1967. · Zbl 0149.24309
[78] , , and , Definition 1.1 of the generic development language Deva, Tool Use Research Report 94, Unité d’Informatique, Université Catholique de Louvain, Louvain-la-Neuve, Belgium, 1989.
[79] Kids – a knowledge-based software development system, pp. 129–136 in: Proceedings Workshop on Automating Software Design, AAAI-88, September 1988.
[80] The SETL2 Programming Language, Technical Report 490, Courant Insititute, New York University, New York, 1990.
[81] , and , The Irvine Program Transformation Catalogue, Technical Report, University of California at Irvine, Department of Information and Computer Science, Irvine, California, January 1976.
[82] Taliere: An Interactive System for Data Structuring SETL Programs, Doctoral Dissertation, Department of Computer Science, New York University, 1988.
[83] and , CAI course in axiomatic set theory, pp. 3–80 in: University Level Computer-Assisted Instruction at Stanford: 1968-1980, ed., Stanford University, Institute for Mathematical Studies in the Social Sciences, Stanford, California, 1981.
[84] Tarjan, J. Comput. System Sci. 9 pp 355– (1974) · Zbl 0315.68018 · doi:10.1016/S0022-0000(74)80049-8
[85] Tarski, Pacific J. Math. 5 pp 285– (1955) · Zbl 0064.26004 · doi:10.2140/pjm.1955.5.285
[86] Type Determination for Very High Level Languages, Courant Computer Science Report 3, Courant Institute, New York University, New York, 1974.
[87] A Taxonomy of Finite Automata Minimization Algorithms, Computing Science Note 93/44, Eindhoven University of Technology, Eindhoven, The Netherlands, 1993.
[88] , and , The Generic Development Language Deva, LNCS Vol. 738, Springer-Verlag, Berlin, 1993. · doi:10.1007/3-540-57335-6
[89] Fast Decision of Strong Bisimulation Equivalence Using Partition Refinement, Dissertation for the Licentiate Degree in Computer Science, Chalmers University, Department of Computer Science, Göteborg, Sweden, 1989.
[90] A User Manual for FOL, Technical Report 235.1, Stanford AIM, Stanford, California, 1977.
[91] Modern Structured Analysis, Yourdon Press, New York, 1989.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.