A type system for object models

ABSTRACT

A type system for object models is described that supports subtyping, unions, and overloading of relation names. No special features need be added to the modelling language; in particular, there are no casts, and the meaning of an object model can be understood without mentioning types. A type error is associated with an expression that can be proved to be _irrelevant_, in the sense that it can be replaced by an empty set or relation without affecting the value of its enclosing constraint. Relevance is computed by a simple abstract interpretation.

REFERENCES

• 1: The Alloy Modelling Language and Analyzer_. Papers and tool available at: http://alloy.mit.edu. Software Design Group, Computer Science and Artificial Intelligence Laboratory, MIT, Cambridge, MA.
• 2: Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer and Moshe Y. Vardi. Enhanced Vacuity Detection in Linear Temporal Logic. Computer-Aided Verification, Boulder, Colorado, July 2003.
• 3: R. Duke, G. Rose, and G. Smith. Object-Z: A Specification Language Advocated for the Description of Standards. Technical Report 94-45, Software Verification Research Centre, School of Information Technology, The University of Queensland, December 1994.
• 4: Jonathan Edwards, Daniel Jackson, Emina Torlak and Vincent Yeung. Subtypes for Constraint Decomposition. International Symposium on Software Testing and Analysis, Boston, MA, July 2004.
• 5: Nevin Heintze, Set-based analysis of ML programs, Proceedings of the 1994 ACM conference on LISP and functional programming, p.306-317, June 27-29, 1994, Orlando, Florida, United States
• 6: Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
• 7: Daniel Jackson , Ilya Shlyakhter , Manu Sridharan, A micromodularity mechanism, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 8: Leslie Lamport , Lawrence C. Paulson, Should your specification language be typed, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.502-526, May 1999 [doi>10.1145/319301.319317]
• 9: Response to the UML 2.0 OCL RFP_. Submitters: Boldsoft, Iona, Rational Software Corporation, and Adaptive Ltd. OMG Document ad/2003-01-07. Available at: http://www.klasse.nl/ocl/.
• 10: John Rushby , Sam Owre , Natarajan Shankar, Subtypes for Specifications: Predicate Subtyping in PVS, IEEE Transactions on Software Engineering, v.24 n.9, p.709-720, September 1998 [doi>10.1109/32.713327 ]
• 11: Andy Schürr, New Type Checking Rules for OCL Expressions, Modellierung 2001, Workshop der Gesellschaft für Informatik e. V. (GI), p.91-100, March 28-30, 2001
• 12: J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992
• 13: Jos Warmer , Anneke Kleppe, The object constraint language: precise modeling with UML, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1998
• 14: Information technology -- Z formal specification notation -- Syntax, type system and semantics. ISO Standard ISO/IEC 13568:2002.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

General Terms:
Design, Languages, Theory, Verification

Keywords:
ZOCL, alloy, object models, relational logic, specification languages, type systems, vacuity detection