JML's Rich, Inherited Specifications for Behavioral Subtypes







Deposit Papers 


Leavens, Gary T. (2006) JML's Rich, Inherited Specifications for Behavioral Subtypes. Technical Report TR #06--22, Computer Science, Iowa State University.

Full text available as:Adobe PDF


The Java Modeling Language (JML) is used to specify detailed designs for Java classes and interfaces. It has a particularly rich set of features for specifying methods. This paper describes those features, with particular emphasis on the features related to specification inheritance. It shows how specification inheritance in JML forces behavioral subtyping, through a discussion of semantics and examples. It also describes a notion of modular reasoning based on static type information, supertype abstraction, which is made valid in JML by methodological restrictions on invariants, history constraints, and initially clauses and by behavioral subtyping.

Keywords:Supertype abstraction, behavioral subtype, behavioral subtyping, modularity, specification inheritance, method specification refinement, join of method specifications, also, specification case, invariants, JML, Java.
Comments:to appear in Zhiming Liu and He Jifeng (eds), Proceedings, International Conference on Formal Engineering Methods (ICFEM'06), Macao, China}, pages 2-36. Volume 4260 of Lecture Notes in Computer Science, Springer-Verlag, 2006
Subjects:Computer Systems Organization: COMPUTER SYSTEM IMPLEMENTATION: Microcomputers
Software: PROGRAMMING TECHNIQUES (E): Object-oriented Programming
Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Coding Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: PROGRAMMING LANGUAGES: Formal Definitions and Theory (D.2.1, F.3.1-2, F.4.2-3)
Software: PROGRAMMING LANGUAGES: Language Classifications
Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Semantics of Programming Languages (D.3.1)
ID code:00000442
Deposited by:Gary T. Leavens on 11 August 2006
Alternative Locations:

Contact site administrator at: