Title
Model-based specification
Abstract
Procedures in an imperative programming language are specified by means of a precondi- tion and a postcondition, expressed in the procedure's parameters and any global variables that are referenced. A simple way of looking at methods in object-oriented languages, sug- gested by early implementations, is to regard these as procedures with one special parame- ter that is written before the method name in method calls. This parameter is not explicitly present in the method's definition, but can be retrieved via the keyword this or self. The specification style suggested by this view is the use of pre- and postconditions ex- pressed in both this and the method's explicit parameters. Here the question arises what kind of assertions are permitted about the state of this and other objects among the parame- ters. The simplest way to view object types, as made explicit in Oberon-2 (13), is as a special kind of record types; consistent with such a view is the characterization of object states by means of field (or attribute) values. Indeed, many specification methodologies for object- oriented programs in the literature (for instance (1)) proceed this way. Yet, one might argue that such an approach does not go well with the concepts of in- formation hiding and subtype polymorphism inherent in object-oriented design. It conflicts with information hiding because that principle states that the object's clients should not even be aware of the existence of private fields, let alone be dependent on them for method specifications. It conflicts with subtype polymorphism because the procedure body could at run-time be replaced with a fresh implementation that produces similar observable effects by a completely different set of private fields. Finally, specifications based on field values become patently impossible as soon as one introduces abstract classes or interfaces, which may not have any fields at all.
Year
DOI
Venue
2001
10.1016/S0020-0190(00)00206-4
Inf. Process. Lett.
Keywords
Field
DocType
model-based specification,programming language,object oriented design,object oriented language,object oriented programming,program derivation,information hiding,polymorphism,object orientation,difference set,object oriented
Programming language,Object-orientation,Problem domain,Computer science,Software design pattern,Reference implementation,Formal specification,Theoretical computer science,Language Of Temporal Ordering Specification,Program derivation,Formalism (philosophy)
Journal
Volume
Issue
Citations 
77
2-4
2
PageRank 
References 
Authors
0.41
10
1
Name
Order
Citations
PageRank
Lex Bijlsma1978.84