Algebraic specification techniques for parametric types with logic-based constraints

ABSTRACT

Mainstream object-oriented languages now offer capabilities of generic types with bounded type parameters, but they typically do not provide support for specifying semantic requirements on the type parameters' methods beyond conformance of signatures. Regrettably, even object-oriented assertion languages, such as JML, have nontrivial limitations in this regard. Yet many interesting parameterized types require additional semantic features if they are to function as intended. We illustrate the issues with a case study of project scheduling based on the Project Management Institute's generic characterization of task breakdowns. We consider algebraic techniques for instantiating parametric types in such a way that the semantic requirements expressed by logic-based constraints propagate to the instantiating types. These techniques argue for more general bindings of actual type parameters for the formal ones which do not have the restrictions of current programming languages. We show that types equipped with constraints should be viewed as theories, and the bindings as morphisms of types as theories. We translate these software specifications into theories in the PVS specification language. These proposals lead to conclusions about language features for more general, semantic bindings of the actual for the formal type parameters, at least in the assertion languages.

REFERENCES

• 1: Suad Alagić , Mark Royer, Genericity in Java: persistent and database systems implications, The VLDB Journal — The International Journal on Very Large Data Bases, v.17 n.4, p.847-878, July 2008 [doi>10.1007/s00778-006-0042-x]
• 2: S. Alagić, M. Royer, and D. Crews, Temporal verification of Java-like classes, Proceedings of the FTfJP 2006 Workshop, http://www.disi.unige.it/person/AnconaD/FTfJP06/.
• 3: Suad Alagic , Svetlana Kouznetsova, Behavioral Compatibility of Self-Typed Theories, Proceedings of the 16th European Conference on Object-Oriented Programming, p.585-608, June 10-14, 2002
• 4: M. Barnett, K. R. M. Leino, and W. Schulte, The Spec# programming system: an overview, Microsoft Research 2004. Also in Proceedings of CASSIS 2004.
• 5: R. Breu , J. Hartmanis , G. Goos, Algebraic Specification Techniques in Object Oriented Programming Environments, Springer-Verlag New York, Inc., Secaucus, NJ, 1991
• 6: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 7: Kokichi Futatsugi , Joseph A. Goguen , Jean-Pierre Jouannaud , José Meseguer, Principles of OBJ2, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.52-66, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318610]
• 8: Joseph A. Goguen, Types as theories, Topology and category theory in computer science, Oxford University Press, Inc., New York, NY, 1991
• 9: Joseph A. Goguen , Rod M. Burstall, Institutions: abstract model theory for specification and programming, Journal of the ACM (JACM), v.39 n.1, p.95-146, Jan. 1992 [doi>10.1145/147508.147524]
• 10: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java(TM) Language Specification, The (3rd Edition) (Java (Addison-Wesley)), Addison-Wesley Professional, 2005
• 11: John V. Guttag , James J. Horning, Larch: languages and tools for formal specification, Springer-Verlag New York, Inc., New York, NY, 1993
• 12: Andrew Kennedy , Don Syme, Design and implementation of generics for the .NET Common language runtime, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.1-12, June 2001, Snowbird, Utah, United States
• 13: G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cook, P. Muller, and J. Kiniry, JML Reference Manual, 2005, http://www.cs.iastate.edu/leavens/JML/.
• 14: Barbara H. Liskov , Jeannette M. Wing, A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.6, p.1811-1841, Nov. 1994 [doi>10.1145/197320.197383]
• 15: David C. Luckham, Programming with Specifications: An Introduction to Anna, a Language for Specifying ADA Programs, Springer-Verlag New York, Inc., Secaucus, NJ, 1990
• 16: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 17: S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Clavert: PVS Language Reference, SRI International, Computer Science Laboratory, Menlo Park, California, http://pvs.csl.sri.com.
• 18: Project Management Institute, A Guide to Project Management Body of Knowledge, Project Management Institute, 2000.
• 19: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 20: M. Royer, S. Alagić, and D. Dillon, Reflective constraint management for languages on virtual platforms, Journal of Object Technology, Vol. 6, No. 10, 2007.
• 21: Bjarne Stroustrup, The C++ Programming Language, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 22: Jos Warmer , Anneke Kleppe, The Object Constraint Language: Getting Your Models Ready for MDA, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003
• 23: Dachuan Yu , Andrew Kennedy , Don Syme, Formalization of generics for the .NET common language runtime, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.39-51, January 14-16, 2004, Venice, Italy

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.5 Object-oriented Programming
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
      D.2.4 Software/Program Verification
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
JML, PVS, assertions, parametric types, verification theories