The full version of this information is available.
This paper is available via ftp or via WWW .
This paper addresses the issue of giving a formal semantics to an object-oriented programming and specification language. Object-oriented constructs considered are objects with attributes and methods, encapsulation of attributes, subtyping, bounded type parameters, classes, and inheritance. Classes are distinguished from object types. Besides usual imperative statements, specification statements are included. Specification statements allow changes of variables to be described by a predicate. They are abstract in the sense that they are non-executable. Specification statements may appear in method bodies of classes, leading to abstract classes.
The motivation for this approach is that abstract classes can be used for problem-oriented specification in early stages and later refined to efficient implementations. Various refinement calculi provide laws for procedural and data refinement, which can be used here for class refinement. This paper, however, focuses on the semantics of object-oriented programs and specifications and gives some examples of abstract and concrete classes.
The semantics is given by a translation of the constructs into the type system Fsub, an extension of the simple typed lambda-calculus by subtyping and parametric polymorphism: The state of a program is represented by a record. A state predicate is a Boolean valued function from states. Statements, both abstract and concrete, are represented by predicate transformers. Objects are represented by records of statements (the methods) operating on a record of attributes. Classes are understood as templates for the creation of objects. Classes are represented by records. Inheritance amounts to record overwriting. Subtyping and parametric polymorphism are already provided by Fsub.