Should your specification language be typed

ABSTRACT

Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language without types. This possibility, which has been widely overlooked, offers many advantages. Untyped set theory is simple and is more flexible than any simple typed formalism. Polymorphism, overloading, and subtyping can make a type system more powerful, but at the cost of increased somplexity, and such refinements can never attain the flexibility of having no types at all. Typed formalisms have advantages, too, stemming from the power of mechanical type checking. While types serve little purpose in hand proofs, they do help with mechanized proofs. In the absence of verificaiton, type checking can catch errors in specifications. It may be possible to have the best of both worlds by adding typing annotations to an untyped specification language. We consider only specification languages, not programming languages.

REFERENCES

• 1: Krzysztof R. Apt , Ernst-Rüdiger Olderog, Verification of sequential and concurrent programs (2nd ed.), Springer-Verlag New York, Inc., Secaucus, NJ, 1997
• 2: BARRAS, B., BOUTIN, S., CORNES, C., COURANT, J., FILLIBTRE, J.-C., GIMINEZ, E., HERBELIN, H., HUET, G., MUQOZ, C., MUaTHY, C., PAaENT, C., PAULIN-MOHRING, C., SAOBI, A., AND WERNER, B. 1997. The Coq proof assistant reference manual : Version 6.1. Technical Report RT-0203 (May), INRIA-Rocquencourt. Version 5.8.
• 3: Robert S. Boyer , J. Strother Moore, A computational logic handbook, Academic Press Professional, Inc., San Diego, CA, 1988
• 4: K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 5: R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• 6: COQUAND, T. 1990. Metamathematical investigations of a calculus of constructions. In P. ODIFREDDI (Ed.), Logic and Computer Science, pp. 91-122. Academic Press.
• 7: DE BRUIJN, N. G. 1995. On the roles of types in mathematics. In P. DE GROOTE (Ed.), The Curry-Howard isomorphism, pp. 27-54. Academia.
• 8: DUMMETT, M. 1977. Elements of Intuitionism. Oxford University Press.
• 9: Urban Engberg , Peter Grønning , Leslie Lamport, Mechanical Verification of Concurrent Systems with TLA, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.44-55, June 29-July 01, 1992
• 10: FARMER, W. M. 1990. A partial functions version of church's simple theory of types. Journal of Symbolic Logic 55, 3, 1269-1291.
• 11: Kathleen Fisher , John C. Mitchell, The development of type systems for object-oriented languages, Theory and Practice of Object Systems, v.1 n.3, p.189-220, Fall 1995
• 12: FITZGERALD, J. S., LARSEN, P. G., BROOKES, T. M., AND GREEN, M. A. 1995. Developing a security-critical system using formal and conventional methods. In M. HINCHEY AND J. P. BOWEN (Eds.), Applications of Formal Methods, pp. 333-356. Prentice-Hall.
• 13: S. J. Garland , J. V. Guttag, An overview of LP, the larch power, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.137-151, January 1989
• 14: G(SDEL, K. 1983. Russell's mathematical logic. In P. BENACERRAF AND H. PUTNAM (Eds.), Philosophy of Mathematics: Selected Readings (2nd ed.). Cambridge University Press. First published in 1944.
• 15: M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993
• 16: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 17: David Gries , Fred B. Schneider, A logical approach to discrete math, Springer-Verlag New York, Inc., New York, NY, 1993
• 18: C. A. Gunter , D. S. Scott, Semantic domains, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 19: GUTTAG, J. V. AND HORNING, J. J. 1978. The algebraic specification of abstract data types. Acta Informatica 10, 27-52.
• 20: HALMOS, P. R. 1960. Naive Set Theory. Van Nostrand.
• 21: Eric C. R. Hehner, Predicative programming Part II, Communications of the ACM, v.27 n.2, p.144-151, Feb. 1984 [doi>10.1145/69610.357990]
• 22: Paul Hudak , Simon Peyton Jones , Philip Wadler , Brian Boutel , Jon Fairbairn , Joseph Fasel , María M. Guzmán , Kevin Hammond , John Hughes , Thomas Johnsson , Dick Kieburtz , Rishiyur Nikhil , Will Partain , John Peterson, Report on the programming language Haskell: a non-strict, purely functional language version 1.2, ACM SIGPLAN Notices, v.27 n.5, p.1-164, May 1992 [doi>10.1145/130697.130699]
• 23: HUET, G. 1997. Re: types and extremism. Email to Leslie Lamport. Internet message sent on April 25, 1997 23:11:37 MET DST, number [e-mail].
• 24: KAUFMANN, M. AND MOORE, J. S. 1996. ACL2: An industrial strength version of Nqthm. In Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS-96), pp. 23-34. IEEE Computer Society Press.
• 25: LAM, S. S. AND SHANKAR, A. U. 1984. Protocol verification via projections. IEEE Transactions on Software Engineering SE-10, 4 (July), 325-342.
• 26: LEISENRING, A. C. 1969. Mathematical Logic and Hilbert's c-Symbol. Gordon and Breach, New York.
• 27: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 28: Thomas F. Melham, Automating recursive type definitions in higher order logic, Current trends in hardware verification and automated theorem proving, Springer-Verlag New York, Inc., New York, NY, 1989
• 29: MILNER, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348-375.
• 30: MITCHELL, J. C. 1991. Type inference with simple subtypes. Journal of Functional Programruing 1, 3 (July), 245-285.
• 31: Greg Nelson, Systems programming with Modula-3, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 32: OWRE, S. 1998. PVS 2.1 patches (2.417). Email to [e-mail]. Internet message sent on Sat, Feb 7, 1998 02:53:40 -0800, number [e-mail].
• 33: Sam Owre , John Rushby , Natarajan Shankar , Friedrich von Henke, Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS, IEEE Transactions on Software Engineering, v.21 n.2, p.107-125, February 1995 [doi>10.1109/32.345827 ]
• 34: Lawrence C. Paulson, Verifying the unification algorithm in LCF, Science of Computer Programming, v.5 n.2, p.143-169, June 1985
• 35: Lawrence C. Paulson, Set theory for verification. I: from foundations to functions, Journal of Automated Reasoning, v.11 n.3, p.353-389, Dec. 1993 [doi>10.1007/BF00881873]
• 36: Lawrence C. Paulson, A Fixedpoint Approach to Implementing (Co)Inductive Definitions, Proceedings of the 12th International Conference on Automated Deduction, p.148-161, June 26-July 01, 1994
• 37: PAULSON~ L. C. 1994b. Isabelle: A Generic Theorem Prover. Springer. LNCS 828.
• 38: PAULSON~ L. C. 1995. Set theory for verification: II. Induction and recursion. Journal of Automated Reasoning 15, 2, 167-215.
• 39: Lawrence C. Paulson, ML for the working programmer (2nd ed.), Cambridge University Press, New York, NY, 1996
• 40: Art Quaife, Automated deduction in von Neumann-Bernays-Go¨del set theory, Journal of Automated Reasoning, v.8 n.1, p.91-147, Feb. 1992
• 41: SCOTT~ D. 1979. Identity and existence in intuitionistic logic. In M. P. FOURMAN (Ed.), Applications of Sheaves, pp. 660-696. Springer. Lecture Notes in Mathematics 753.
• 42: Simon Thompson, Type theory and functional programming, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1991
• 43: P. Wadler , S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.60-76, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75283]
• 44: WHITEHEAD~ A. N. AND RUSSELL~ B. 1962. Principia Mathematica. Cambridge University Press. Paperback edition to *56, abridged from the 2nd edition (1927).
• 45: Andrew K. Wright , Robert Cartwright, A practical soft type system for scheme, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.1, p.87-152, Jan. 1997 [doi>10.1145/239912.239917]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

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

General Terms:
Verification

Keywords:
set theory, specification, types