A Theory-Based Representation for Object-Oriented Domain Models.
AbstractFormal software specification has long been touted as a way to increase the quality and reliability of software; however, it remains an intricate, manually intensive activity. An alternative to using formal specifications directly is to translate graphically based, semiformal specifications into formal specifications. However, before this translation can take place, a formal definition of basic object-oriented concepts must be found. This paper presents an algebraic model of object-orientation that defines how object-oriented concepts can be represented algebraically using an object-oriented algebraic specification language O-Slang. O-Slang combines basic algebraic specification constructs with category theory operations to capture internal object class structure, as well as relationships between classes.
INTRODUCTION
As the field of software engineering continues to evolve toward a more traditional engineering dis-
cipline, a concept that is emerging as important to this evolution is the use of formal specifications,
the representation of software requirements by a formal language [1],[2]. Such a representation
has many potential benefits, ranging from improvement of the quality of the specification itself
to the automatic generation of executable code. While some impressive results have emerged
from the utilization of formal specifications [3],[4], the development of formal specifications to
represent a user's requirements is still a difficult task. This has restricted adoption of formal
specifications by practitioners.
On the other hand, an approach to requirements modeling that has been gaining acceptance
is the use of object-oriented methods. Initially introduced as a programming paradigm, its application
has been extended to the entire software lifecycle. This informal approach, consisting
of graphical representations and natural language descriptions, has many variations, but Rum-
baugh's Object Modeling Technique (OMT) is typical, and perhaps the most widely referenced [5].
In OMT, three models are combined to capture the essence of a software system. The object
model captures the structural aspects of the system by defining objects, their attributes, and the
relationships (associations) between them. The behavior of the system is captured by the other
two models. The dynamic model captures the control flow as a classical state-transition model,
or statechart, while the functional model represents the system calculations as hierarchical data
flow diagrams and process descriptions. All three models are needed to capture the software
system's requirements, although for a given system one or two of the models may be of lesser
importance, or even omitted.
While systems such as KIDS [3] and Specware [6] have been making progress in software
synthesis, research in the acquisition of formal specifications has not been keeping pace. Formal
specification of software remains an intricate, manually intensive activity. Problems associated
with specification acquisition include a lack of expertise in mathematical and logical concepts
among software developers, an inability to effectively communicate formal specifications with
end users to validate requirements, and the tendency of formal notations to restrict solution
creativity [7]. Fraser et. al., suggest an approach to overcoming these problems via parallel
refinement of semi-formal and formal specifications. In a parallel refinement approach, designers
develop specifications using both semi-formal and formal representations, successively refining
both representations in parallel [7].
Fig. 1 shows our concept of a parallel refinement system for formal specification development.
In this system, a domain engineer would use a graphically-based object-oriented interface to
specify a domain model. This domain model would be automatically translated into formal
Class Theories stored in a library. A user knowledgeable in the domain would then use the
graphically-based object-oriented interface to refine the domain model into a problem specific
formal Functional Specification. Finally, a software engineer would map the Functional Specification
to an appropriate formal Architecture Theory, generating a specification capable of being
transformed to code by a system such as Specware.
Bailor Approved
System
Specifications
Specification Structuring
Domain Engineering Specification Generation
Object-Oriented User Interface
Specification Acquisition Mechanism
Domain
Knowledge
Domain Theory
Composition
Subsystem
Class
Theories
Theory Library (Abstract Types)
Problem
Requirements
Architecture
Theories
Specification
Generation/Refinement
Subsystem
Architecture
Matching
Subsystem
Functional
Specifications
Design
Decisions
Non-Functional
Functional

Figure

1: Parallel Refinement Specification Acquisition Mechanism
A critical element for the success of such a system is the definition of a formal representation
that captures all important aspects of object-orientation, along with a formal represention of the
syntax and semantics of the informal model and a mapping for ensuring the full equivalence of the
informal and formal models. While formal representation of the informal model has been done
in bits and pieces [8],[9],[10], a full, consistent, integrated formal object model does not exist.
This paper describes a method for fully representing an object-oriented model using algebraic
theories [11]. An algebraic language, O-Slang, is defined as an extension of Kestrel Institute's
Slang [12]. O-Slang not only supports an algebraic representation of objects, but allows the
use of category theory operations such as morphisms and colimits to combine primitive object
specifications to form more complex aggregates, and to extend object specifications to capture
multiple inheritance [13]. Using this formal representation along with formal transformations
from the informal model, we have demonstrated the automatic generation of formal algebraic
specifications from commercially available object oriented CASE tools.
The remainder of the paper is organized as follows. Section 2 discusses related work and Section
3 presents basic algebraic and category theory concepts. Section 4 introduces the basic object
model while Sections 5 through 7 describe inheritance, aggregation, and object communication
in more detail. Finally, Section 8 discusses our contributions and plans for the future.
Related Work
There have been a number efforts designed to incorporate object-oriented concepts into formal
specification languages. MooZ [14] and Object-Z [15] extend Z by adding object-oriented structures
while maintaining its model-based semantics. Z++ [16] and OOZE [17] also extend Z but
provide semantics based on algebra and category theory. Although these Z extensions provide
enhanced structuring techniques, they do not provide improved specification acquisition meth-
ods. FOOPS [18] is an algebraic, object-oriented specification language based on OBJ3 [19].
Both FOOPS and OBJ3 focus on prototyping, and provide little support for specification acqui-
sition. Some research has been directed toward improving specification acquisition by translating
object-oriented specifications into formal specifications [10]; however, these techniques are based
on Z and lack a strong notion of refinement from specification to code.
3 Theory Fundamentals
Theory-based algebraic specification is concerned with (1) modeling system behavior using algebras
(a collection of values and operations on those values) and axioms that characterize algebra
behavior, and (2) composition of larger specifications from smaller specifications. Composition
of specifications is accomplished via specification building operations defined by category theory
constructs [20]. A theory is the set of all assertions that can be logically proved from the axioms of
a given specification. Thus, a specification defines a theory and is termed a theory presentation.
In algebraic specifications, the structure of a specification is defined in terms of sorts, abstract
collections of values, and operations over those sorts. This structure is called a signature. A
signature describes the structure of a solution; however, a signature does not specify semantics.
To specify semantics, the definition of a signature is extended with axioms defining the intended
semantics of signature operations. A signature with associated axioms is called a specification.
An example of a specification is shown in Figure 2.
spec Array is
sorts E, I, A
operations
apply
axioms 8 E)
(i

Figure

2: Array specification
A specification allows us to formally define the internal structure of object classes (attributes
and operations); however, they do not provide the capability to reason about relationships between
object classes. To create theory-based algebraic specifications that parallel object-oriented
specifications, the ability to define and reason about relationships between theories, similar to
those used in object-oriented approaches (inheritance, aggregation, etc.), must be available. Category
theory is an abstract mathematical theory used to describe the external structure of various
mathematical systems [21] and is used here to describe relationships between specifications.
A category consists of a collection of C-objects and C-arrows between objects such that (1) there
is a C-arrow from each object to itself, (2) C-arrows are composable, and (3) arrow composition
is associative. An obvious example is the category Set where "C-objects" are sets and "C-
arrows" are functions between sets. However, of greater interest in our research is the category
Spec. Spec consists of specifications as the "C-objects" with specification morphisms as the "C-
arrows". A specification morphism, oe, is a pair of functions that map sorts (oe S
operations
spec Finite-Map is
sorts M, D, R
operations
apply
axioms 8

Figure

3: Finite map specification
(oe\Omega ) from one specification to compatible sorts and operations of a second specification such
that the axioms of the first specification are theorems of the second specification. Intuitively,
specification morphisms define how one specification is embedded in another. An example of a
morphism from array to finite-map (Figure 3) is shown below.
apply 7! applyg
Specification morphisms comprise the basic tool for defining and refining specifications. Our
toolset can be extended to allow the creation of new specifications from a set of existing spec-
ifications. Often two specifications derived from a common ancestor specification need to be
combined. The desired combination consists of the unique parts of two specifications and some
"shared part" common to both specifications (the part defined in the shared ancestor specifica-
tion). This combining operation is a colimit.
Conceptually, the colimit is the "shared union" of a set of specifications based on the morphisms
between the specifications. These morphisms define equivalence classes of sorts and operations.
For example, if a morphism, oe, from specification A to specification B maps sort ff to sort fi,
then ff and fi are in the same equivalence class and thus become a single sort in the colimit
specification of A, B, and oe. The colimit operation creates a new specification, the colimit
specification, and a specification morphism from each specification to the colimit specification.
An example showing the relationship between a colimit and multiple inheritance is provided in
Section 5.
From these basic tools (morphisms and colimits), we can construct specifications in a number of
ways [20]. We can (1) build a specification from a signature and a set of axioms, (2) form the union
of a set of specifications via a colimit, (3) rename sorts or operations via a specification morphism,
and (4) parameterize specifications. Many of these methods are useful in translating object-oriented
specifications into theory-based specifications. Detailed semantics of object-oriented
concepts using specifications and category theory constructs are presented next.
4 Object Classes
The building block of object-orientation is the object class which defines the structure of an object
and its response to external stimuli based its current state. Formally defined in Section 4.1 as
a class type, a class is a template from which individual object instances can be created. Fig. 4
shows a specification of a banking account class in O-Slang.
4.1 Class Structure
In our theory-based object model, we capture the structure of a class as a theory presentation,
or algebraic specification, as follows.
class type, C, is a signature,
hS;\Omega i and a set of
axioms, \Phi, over \Sigma (i.e., a theory presentation, or specification) where
S denotes a set of sorts including the class sort
\Omega denotes a set of functions over S
\Phi denotes a set of axioms over \Sigma
Sorts in S are used to describe collections of data values used in the specification. In O-Slang
a distinguished sort, the class sort, is the set of all possible objects in the class. In an algebraic
sense, this is really the set of all possible abstract value representations of objects in the class.
Functions
in\Omega are classified in O-Slang syntax as attributes, methods, state-attributes, states,
class Acct is
import Amnt, Date
class sort Acct
sorts Acct-State
operations
attributes
state-attributes
methods
create-acct
states
events
new-acct
axioms
state uniqueness and invariant axioms
operation definitions
method definitions
event definitions
8 (a: Acct, x: Amnt) acct-state(a)=ok
8 (a: Acct, x: Amnt) acct-state(a)=overdrawn
end-class

Figure

4: Object Class
events, and operations. Attributes are defined implicitly by visible functions which return specific
data values. In Fig. 4, the functions date and bal are attributes. Methods are non-visible functions,
invoked via visible events, that modify an object's attribute values. A method's domain includes
an object, along with additional parameters, while the return value is always the modified object.
In Fig. 4, the functions create-acct, credit and debit are methods. The semantics of functions,
as well as invariants between class attribute values, are defined using first order predicate logic
axioms. In general, axioms define methods by describing their effects on attribute values as in
the following example.
4.2 Class Behavior
States. In our model, a state is a partition of the cross-product of an object's attribute values.
For example, a bank account might be partitioned into an ok and an overdrawn state based on
a partitioning of its balance values. Formally, a class type has at least one state sort (multiple
state sorts allow modeling concurrent state models and substate models), a set of states which
are elements in a state sort (defined by nullary functions), a state attribute defined over each
state sort as a function which returns the current state of an object, and a set of state invariants,
axioms that describe constraints on class attributes that must hold true while in a given state.
In our object model, we separate state attributes from normal attributes to capture the notion
of an object's abstract state as might be defined in an statechart. The values of state attributes
of define an object's abstract state while the values of normal attributes define an object's true
state. In Fig. 4, the class state sort is Acct-State, the class state attribute is acct-state, the state
constants are ok and overdrawn, and the state invariants are
These axioms state that when the balance of an account is greater than or equal to zero, the
account must be in the ok state; however, when the balance of the account becomes less than zero,
the state must become overdrawn. While it is tempting to replace the implication operators with
equivalence operators, doing so would unnecessarily restrict subclasses derived from this class as
defined in Section 5. Additionally, the axiom
ok 6= overdrawn
ensures correct interpretation of the specification that states ok and overdrawn are distinct.
Events. Events are visible functions that allow objects to communicate with each other and
may directly modify state attributes. We present a more detailed discussion of the specificaiton
of this communication between objects in Section 7. As a side effect, receipt of an event may
cause the invocation of methods or the generation of events sent to other objects. Events are
distinct from methods to separate control from execution. This separation keeps us from having
to embed state-based control information within methods. Each class has a new event which
triggers the create method and initializes the object's state attributes. In Fig. 4, the functions
new-acct, deposit and withdrawal are events. The effect of these events on the class behavior,
which can be represented by the statechart in Fig. 5, is defined by a set of axioms similar to the
following axiom from Fig. 4.
OK overdrawn
deposit(a,x)/credit(a,x)
new-acct(d)

Figure

5: Account Statechart
Class Operations. Operations are visible functions that are generally used to compute derived
attributes and may not directly modify attribute values. In Fig. 4, the function acct-attr-equal is
an operation. Similar to methods and events, the semantics of operations are defined using first
order predicate logic axioms.
Inheritance
Class inheritance plays an important role in object-orientation; however, the correct use of inheritance
is not uniformly agreed upon. In our work we have chosen to use a strict form of
inheritance that allows a subclass object to be freely substituted for its superclass in any situa-
tion. This subtype interpretation was selected to simplify reasoning about the class's properties
and to keep it closely related to software synthesis concepts [6]. We believe the advantages of
strict inheritance outweight its disadvantages in our research since most arguments favoring a
less strict approach to inheritance - such as polymorphism and overloading - are much more
germane to implementation than to specification. Thus, as a subtype, a subclass may only extend
the features of its superclass. Liskov defines these desired effects as the "substitution property"
[22]:
If for each object
of type S there is an object
of type T such that for all programs P
defined in terms of T the behavior of P is unchanged when
is substituted for
, then S
is a subtype of T .
The only way to ensure the substitution property holds in all cases is to ensure that the
effects of all superclass operations performed on an object are equivalent in the subclass and the
superclass. To achieve this, inheritance must provide a mapping from the sorts, operations, and
attributes in the superclass to those in the subclass that preserve the semantics of the superclass.
This is the basic definition of a specification morphism (extended for O-Slang to map class-
sorts to class-sorts, attributes to attributes, methods to methods, etc.) and provides us a formal
definition of inheritance [13].
Specification morphisms map the sorts and operations of one algebraic specification into the
sorts and operations of a second specification such that the axioms in the first specification are
theorems in the second specification [13]. Thus, in essence, a specification morphism defines an
embedding of functionality from one specification into a second specification.
class D is said to inherit from a class C, denoted
there exists a specification morphism from C to D and the class sort of D is a sub-sort of the
class sort of C (i.e., D cs
provides a concise, mathematically precise definition of inheritance and ensures
the preservation of the substitution property as stated in Theorem 1 [11].
Theorem 1 Given a specification morphism, oe : C ! D, between two internally consistent
classes C and D such that D cs
, the substitution property holds between C and D.
Since we assume user defined specifications are initially consistent, we can ensure consistency
in a subclass as long as the user does not introduce new axioms in the subclass that redefine how
a method defined in the superclass affects an attribute also defined in the superclass.
An example of single inheritance using a subclass of the ACCT class is shown in Fig. 6. The
import statement includes all the sorts, functions, and axioms declared in the ACCT class directly
into the new class while the class sort declaration SAcct ! Acct states that SAcct is a sub-sort
of Acct, and as such, all functions and axioms that apply to an Acct object apply to a SAcct
object as well. A statechart for SACCT is shown in Fig. 7. The import operation defines a
specification morphism between ACCT and SACCT while the sub-sort declaration completes
the requirements of Definition 2 for inheritance. Therefore, SACCT is a valid subclass of ACCT
and the substitution property holds.
5.1 Multiple Inheritance
Multiple inheritance requires a slight modification to the notion of inheritance as stated in
Definition 2. The set of superclasses must first be combined via a category theory colimit
operation and then used to "inherit from".
Based on specification morphisms, the colimit operation composes a set of existing specifications
to create a new colimit specification [21]. This new colimit specification contains all the
sorts and functions of the original set of specifications without duplicating the "shared" sorts and
functions from a common "ancestor" specification. Conceptually, the colimit of a set of specifications
is the "shared union" of those specifications. Therefore, the colimit operation creates a
new specification, the colimit specification, and a morphism from each specification to the colimit
specification.
Definition 3 Multiple Inheritance - A class D multiply inherits from a set of classes fC 1 .
g if there exists a specification morphism from the colimit of fC 1 . C n
g to D such that the
class sort of D is a sub-sort of each of the class sorts of fC 1 . C n
g.
This definition states that all sorts and operations from each superclass map to sorts and
operations in the subclass such that the defining axioms are logical consequences of the axioms
class SAcct is
import Acct, Rate
class
operations
attributes
rate
methods
create-sacct
events
new-sacct
compute-interest : SAcct, Date ! SAcct
axioms 8 (d: Date, r: Rate, a, a1: SAcct)
operation definitions
method definition
8 (s: SAcct, a: Amnt)
8 (s: SAcct, a: Amnt)
event definitions
end-class

Figure

Savings Class
OK overdrawn
deposit(a,x)/credit(a,x)
rate-change(a,d,r)
rate-change(a,d,r)
compute-interest(a,d)
/int(a,d)

Figure

7: Savings Account Statechart
of the subclass. This implies that all operations defined in a superclasses are applicable in the
subclass as well. This definition ensures that the subclass D inherits, in the sense of Definition
2, from each superclass in fC 1 . C n g as shown in Theorem 2 below [11].
Theorem 2 Given a specification morphism from the colimit of fC 1 . C n g to D such that the
class sort of D is a sub-sort of each of the class sorts of fC 1 . C n g, the substitution property
holds between D and each of its superclasses fC 1 . C n g.
It is important to note that Definition 3 only ensures valid inheritance when the axioms defining
each operation in the superclass specifications fC 1 . C n
are complete. Failure to completely
define operations can result in an inconsistent colimit specifications [11].
We can use multiple inheritance to combine the features of a savings account with those of
a checking account, CACCT, as defined in Fig. 8. To compute the resulting class, the colimit
of the classes ACCT, SACCT, CACCT, and morphisms from ACCT to SACCT and CACCT is
computed as shown in Fig. 9, where an arrow labeled with an "i" represents an import morphism
and a "c" represents a morphism formed by the colimit operation. A simple extension of the
colimit specification with the class sort definition
Comb-Acct ! SAcct; CAcct
yields the desired class where Comb-Acct is a subclass of both SAcct and CAcct, as denoted by
the ! operator in the class sort definition. Fig. 10 shows the "long" version of the combined
specification signature with all the attributes, methods, and events inherited by the Comb-Acct
class (axioms are omitted for brevity).
class CAcct is
import Acct class sort CAcct ! Acct
operations
attributes
check-cost
methods
create-cacct
set-check-cost : CAcct, Amnt ! CAcct
events
new-cacct
change-check-cost : CAcct, Amnt ! CAcct
axioms 8 (a: CAcct, x: Amnt)
axioms omitted
end-class

Figure

8: Checking Class
SAcct CAcct
Acct
Comb-Acct
c
c
c

Figure

9: Colimit of Accounts
class Comb-Acct is
import SAcct, CAcct
class
sorts Acct-State
operations
attributes
rate
check-cost
state-attributes
methods
create-acct Comb-Acct
create-sacct Comb-Acct
create-cacct Comb-Acct
create-comb-acct Comb-Acct
Comb-Acct
Comb-Acct
Comb-Acct
Comb-Acct
set-check-cost Comb-Acct
Comb-Acct
states
events
new-acct Comb-Acct
new-sacct Comb-Acct
new-cacct Comb-Acct
new-comb-acct Comb-Acct
Comb-Acct
Comb-Acct
Comb-Acct
compute-interest Comb-Acct
change-check-cost Comb-Acct
Comb-Acct
axioms 8 (a: CAcct, x: Amnt)
axioms omitted

Figure

10: Combined Account Signature
6 Aggregation
Aggregation is a relationship between two classes where one class, the aggregate, represents an
entire assembly and the other class, the component, is "part-of" the assembly. Not only do aggregate
classes allow the modeling of systems from components, but they also provide a convenient
context in which to define constraints and associations between components. Aggregate class
behavior is defined by that of its components and the constraints between them. Thus aggregates
impose an architecture on the domain model and specifications derived from it.
Components of an aggregate class are modeled similarly to attributes of a class through the
concept of Object-Valued attributes. An object-valued attribute is a class attribute whose sort
type is a set of objects - the class-sort of another class. Formally, they are specification functions
that take an object and return an external object or set of objects. The effects of methods on
object-valued attributes are similar to those for normal attributes. However, instead of directly
specifying a new value for an object-valued attribute, an event is sent to the object stored in the
object-valued attribute. We can formally define an aggregate using the colimit operation and
object-valued attributes.
class C is an aggregate of a set of component classes, fD 1 ::D n g,
if there exists a specification morphism from the colimit of fD 1 ::D n g to C such that C has at
least one corresponding object-valued attribute for each class sort in fD 1 ::D n
g.
An aggregate class combines a number of classes via the colimit operation to specify a system
or subsystem. The colimit operation also unifies sorts and functions defined in separate classes
and associations to ensure that the associations actually relate two (or more) specific classes. To
capture a domain model within a single structure, we can create a domain-level aggregate. To
create this aggregate, the colimit of all classes and associations within the domain is taken.
6.1 Aggregate Structure
An aggregate consists of a number of classes and provides a convenient means to define additional
constructs and relationships. These constructs include class sets, individual components, and
associations.
6.1.1 Class Set
A class type definition specifies a template for creating new instances. In order to manage a set
of objects in a class, a class set is created for each class defined.
class set is a class whose class sort is a set of objects from a
previously defined object class, C. A class set includes a "class event" definition for each event
in C such that the reception of a class event by a class set object sends the corresponding event
in C to each object of type C contained in the class set object. If the class C is a subclass of
then the class set of C is a subclass of the class sets of D 1 :::D n .
The class set creates a class type whose class sort is a set of objects and defines some basic
functions on that set. For example, in Fig. 11 ACCT-CLASS imports the ACCT class specifica-
class Acct-Class is
contained-class ACCT
class sort Acct-Class
events
axioms
end-class

Figure

11: O-Slang Class Set Specification
tion and adds additional "class" events. These class events mirror the "object" events defined in
the class type and distribute the event invocation to each object in the class set. The resulting
specification is effectively a set of Acct objects. Using the category theory colimit operation, a
class type specification can be combined with a basic SET specification to automatically derive
the class set specification.
6.1.2 Specification of Components
Components may have either a fixed, variable, or recursive structure. All three structures use
object-valued attributes to reference other objects and define the aggregate. The difference
between them lies in the types of objects that are referenced and the functions and axioms
defined over object-valued attributes. In a fixed configuration, once an aggregate references a
particular object, that reference may not be changed. The ability of an aggregate object to
change the object references of its object-valued attributes is determined by whether a method
exists, other than the initialization method, to modify the object-valued attribute. If no methods
modify any object-valued attributes then the aggregate is fixed. If methods do modify the object-
valued attributes, then the aggregate is variable. A recursive structure is also easily represented
using object-valued attributes. In this case, an object-valued attribute is defined in the class
type that references its own class sort.
6.1.3 Associations
Associations model the relationships between an aggregate's components. We define a link as
a single connection between object instances and an association as a group of such links. A
link defines what object classes may be connected along with any attributes or functions defined
over the link. Link attributes and link functions are those that do not belong to any one of the
objects involved, but exist only when there is a link between objects. Formally, associations are
represented generically as a specification that defines a set of individual links. A link defines
a specification that uses object-valued attributes to reference individual objects from two or
more classes. Links may also define link attributes or functions in a manner identical to object
classes. Basically, a link is a class whose class-set is an association while an association is a set
of links. Associations with more than two classes are handled in a similar manner by simply
adding additional object-valued attributes.
Definition 6 Link A link is an object class type with two or more object-valued attributes.
Definition 7 Association An association is the class set of a link specification.
Multiplicity is defined as the number of links of an association in which any given object may
participate. For a binary association, an image operation is defined for each class in the associ-
ation. The image operation returns a set of objects with which a particular object is associated
and is used to define multiplicity constraints as shown in Fig. 12. For binary associations, we
allow five categories of association multiplicities: exactly one, many, optional, one or more, or
numerically specified. True ternary or higher level associations are relatively rare; however, they
exactly one 7!
many 7!
optional 7!
one or more 7!
numerically specified 7!
numerically specified 7!

Figure

12: Association Multiplicity Axioms
can be modeled using an association class. In a ternary association, the image operation returns
a set of object tuples associated with a given object. Since the output is a set of tuples, the same
multiplicity axioms shown in Fig. 12 apply.
6.1.4 Banking Example
An example of a link specification between a class of customers CUST (not illustrated) and the
ACCT class to associate customers with their accounts is shown in Fig. 13. The CA-Link link
specification can relate objects from the two classes without embedding internal references into
the classes themselves. Although the names of the object-valued attributes and sorts correspond
to the CUSTOMER and ACCT classes, the link specification does not formally tie the classes
together. This relationship is actually formalized in the aggregate specification. The association
between the ACCT class and the CUSTOMER class is shown in Fig. 14.
The CUST-ACCT class defines a set of CA-Link objects while its axioms define the multiplicity
relationships between accounts and customers, in this case exactly one customer per account while
each customer may have one or more accounts.
The CUSTOMER, ACCT, and CUST-ACCT classes are then combined to form an aggregate
BANK. The sorts from CUST and CUST-ACCT and the sorts from ACCT and CUST-ACCT
are unified via specification morphisms that define their equivalence as shown in Fig. 15. The
actual specification of the aggregation colimit BANK-AGGREGATE is not shown, but is further
refined into the aggregate specification for BANK seen in Fig. 16. The SET specification is used
to unify sorts while the INTEGER specification ensures only a single copy of integers is included.
Three copies of the SET specification are included since each class requires a unique set.
Once the BANK-AGGREGATE specification is computed, the CUST-ACCT association actually
associates the CUSTOMER class to the ACCT class. New functions and axioms can
link CA-Link is
class sort CA-Link
sorts Customer, Account
operations
attributes
customer
account
methods
events
axioms
operation definition
create method definition
8 (c: Customer, a: Account)
new event definition
8 (c: Customer, a: Account)
ca-link-attr-equal(new-ca-link(c,a), create-ca-link(c,a))
end-link

Figure

13: Customer Account Link
association Cust-Acct is
link-class CA-Link
class sort Cust-Acct
sorts Accounts, Customers
methods
image : Cust-Acct, Customer ! Accounts
Customers
events
new-cust-acct Cust-Acct
axioms
% multiplicity axioms
new event definition
. definition of image operations .
end-association

Figure

14: Cust-Acct Association
Acct-Class Cust-Class
Cust-Acct
Bank-Aggregate
c c
Integer
c
Bank

Figure

15: Aggregation Composition
class Bank is
import
class sort Bank
attributes
Cust-Acct
methods
aggregate methods defined here
update-accts
update-cust-acct Cust-Acct
events
start-account
axioms
definition of aggregate methods in terms of components here
invariants
% definition of operations
8 (b: Bank, a: Address, an: Acct-No, c: Customer)
% definition of methods
8 (b, b1: Bank, an: Acct-No, c: Customer)
add-account(b, c,
date built in
% definition of events
attr-equal(new-bank(), create-bank());
8 (b:Bank, an:Acct-No, c:Customer) attr-equal(start-account(b,c,an),add-account(b,c,an));
8 (b: Bank, an: Acct-No, c: Customer, am: Amount)
8 (b: Bank, an: Acct-No, c: Customer, am: Amount)
end-class

Figure

Aggregate Specification
be added to an extension of colimit specification, the BANK class type specification, shown in
Fig. 16, to describe aggregate-level interfaces and aggregate behavior based on component events
and methods.
6.2 Aggregate Behavior
Once an aggregate is created via a colimit operation, further specification is required to make
the aggregate behave in an integrated manner. First, new aggregate level functions are defined
to enable the aggregate to respond to external events. Then, constraints between aggregate
components are specified to ensure that the aggregate does not behave in an unsuitable or
unexpected manner. Finally, local event communication paths are defined. The definition of
new functions and constraints is discussed in this section while communication between objects
is discussed in Section 7.
6.2.1 Specification of Functionality
In an aggregate, components work together to provide the desired functionality. Functional
decomposition, often depicted using data flow diagrams (DFDs), is used to break aggregate-level
methods into lower-level processes. Processes defined in the functional model are mapped to
events and attributes defined in the aggregate components through aggregate-level axioms.
An example is shown by the data flow diagram in Fig. 17 for the aggregate method add-account,
used to implement aggregate event start-account. The make-deposit and make-withdrawal events
map directly to component events and do not require further functional decomposition.
The add-account process adds an account for an established customer and is defined in terms
of operations defined directly in the bank specification (Figure 16) or included into the bank
specification via the bank aggregate specification from the customer-account link specification

Figure

and the account specification (Figure 4). The following axiom defines add-account
in terms of these subprocesses and data flows as depicted in the data flow diagram.
add-account
customer
new-
ca-link
new-
account
acct
customer
acct
update-
cust-acct
Cust-Acct-Assoc
cust-acct
update-
accts
acct
cust-acct

Figure

17: Bank Aggregate Functional Decomposition
assume date is built in
The add-account method has two parameters, the bank object, b, plus an existing customer object
as shown in the data flow diagram, and returns the modified bank object, b1. The add-account
method is defined by its subprocesses. First, a new account acct is created by invoking the
new-acct process. This is passed to the update-accts process which stores the new account in the
account class, and to the new-ca-link process, along with the customer, which returns a cust-acct
link. Finally, the new cust-acct link is passed to the update-cust-acct process which stores it in
the cust-acct association. The new-acct and new-ca-link processes are the events defined in the
Acct class and the CA-Link association respectively and are already available via the aggregate.
The update-accts and update-cust-acct processes could already exist as part of the account class
and cust-acct association, but as shown here are defined in the aggregate specification.
6.2.2 Specification of Constraints Between Components
In an aggregate, component behavior must often be constrained if the aggregate is to act in an
integrated fashion. Generally, these constraints are expressed by axioms defined over component
attributes. Because the aggregate is the colimit of its components, the aggregate may access
components directly and define axioms relating various component attributes.
Engine Wheel
TransmissionDrives
AutomobileRPMs Conversion-Factor RPMs
Connected

Figure

Automobile Aggregate Functional Decomposition
A simplified automobile object diagram is shown in Fig. 18. The object diagram contains one
engine with an RPMs attribute, one transmission with a Conversion-Factor attribute, and four
wheels, each with an RPMs attribute. Two relationships exist between these objects, Drives, that
relates the transmission to exactly two wheels, and Connected, that relates two wheels (probably
by an axle). Obviously, there are a number of constraints implicit in the object diagram that
must be made explicit in the aggregate. First, the RPMs of the engine, Conversion-Factor of the
transmission, and RPMs of the wheels are all related. Also, the wheels driven by the transmission
must be "connected," and all "connected" wheels should have the same RPMs. The axiom
defines the relationship between the RPMs of the wheels driven by the transmission, the transmission
conversion-factor and the engine RPMs. In this case, wheel-obj is an object valued attribute
of a drives link that points to the two wheels connected to the transmission. The axiom
ensures that the two wheels connected by a connected link have the same RPMs values (here
wheel1 and wheel2 are the object valued attributes of the link). The final constraint, that the
two wheels driven by the transmission be connected, is specified implicitly in the specification of
the create-automobile method. After the transmission and wheel objects (w1, w2, w3, and w4)
are created in lines 1 through 5, drives and connected links are created and defined to ensure the
appropriate constraints are met in lines 6 through 9. Finally in line 10, the engine is created and
inserted into the automobile aggregate.
Because wheels w1 and w2 are associated with the transmission via the drives association in
the line 6, they are also associated together via the connected association in line 8. Thus, the
constraint is satisfied whenever an automobile aggregate object is created.
7 Object Communication
At this point our theory-based object model is sufficient for describing classes, their relationships,
and their composition into aggregate classes; however, how objects communicate has not yet been
addressed. For example, suppose the banking system described earlier has an ARCHIVE object
which logs each transaction as it occurs. Obviously, the ARCHIVE object must be told when a
transaction takes place. In our model, each object is aware of only a certain set of events that
it generates or receives. From an object's perspective, these events are generated and broadcast
to the entire system and received from the system. In this scheme, each event is defined in a
separate event theory as shown in Fig. 19.
An event theory consists of a class sort, parameter sorts, and an event signature that are
mapped via morphisms to sorts and events in the generating and receiving classes. If an event is
being sent to a single object then the event theory class sort is mapped to the class sort of that
event Archive-Withdrawal is
class sort Archive
sorts Acct, Amnt
events
Archive
end-class

Figure

19: Event Theory
object class. However, if the event theory class sort is mapped to the class sort of a class set then
communication may occur with a set of objects of that class. The other sorts in an event theory
class are the sorts of event parameters. The final part of an event theory, the event signature,
is mapped to a compatible event signature in the receiving class. The colimit of the classes, the
event theory, and the morphisms unify the event and sorts such that invocation of the event in
the generating class corresponds an invocation of the actual event in the receiving class.
To incorporate an event into the original ACCT class, the ARCHIVE-WITHDRAWAL event
theory specification is imported into the ACCT class and an object-valued attribute, archive-obj,
is added to reference the archival object. The axioms defining the effect of the withdrawal event
are modified to reflect the communication with the ARCHIVE object as shown below.
Basically, the axioms state that when a withdrawal event is received, the value of the archive-obj
is modified by the archive-withdrawal event defined in the event theory specification. Thus the
ACCT object knows it communicates with some other object or objects; however, it does not
know who they are. With whom an object communicates (or, for that matter, if the object
communicates at all) is determined at the aggregate-level where the actual connections between
communicating components are made.
The modified BANK aggregate diagram that includes the ARCHIVE-WITHDRAWAL event
theory and an ARCHIVE-CLASS specification is shown in Fig. 20. The colimit operation includes
morphisms from ARCHIVE-WITHDRAWAL to ACCT-CLASS and ARCHIVE-CLASS
that unify the sorts and event signature in ACCT-CLASS with the sorts and event signature of
ARCHIVE-CLASS. This unification creates the communication path between account objects
and archive objects.
Acct-Class Cust-Class
Cust-Acct
Bank
Archive-Withdrawal
Archive-Class
c
c

Figure

20: Bank Aggregate with Archive
Communicating with objects from multiple classes requires the addition of another level of
specification which "broadcasts" the communication event to all interested object classes. The
class sort of a broadcast theory is called a broadcast sort and represents the object with which the
sending object communicates. The broadcast theory then defines an object-valued attribute for
each receiving class. Fig. 21 shows an example of the ARCHIVE-WITHDRAWAL-MULT event
theory modified to communicate with two classes. In this case, the ARCHIVE-WITHDRAWAL
theory is used to unify the ARCHIVE-WITHDRAWAL-MULT with the ACCOUNT class as well
as the other two classes. A simplified version of the colimit diagram specification is shown in
Fig. 22.
Multiple receiver classes add a layer of specification; however, multiple sending classes are
handled very simply. The only additional construct required is a morphism from each sending
class to the event theory mapping the appropriate object-valued attribute in the sending class
to the class sort of the event theory and the event signature in the sending class to the event
signature in the event theory.
event Archive-Withdrawal-Mult is
class sort Archive
sorts Amnt, Acct, X, Y
attribute
events
Archive
axioms
8 (a: Archive, ac: Acct, am: Amnt)
end-class

Figure

21: Broadcast Theory
Acct-Class Cust-Class
Cust-Acct
Bank
Archive-Class
Printer-Class
Archive-Withdrawal-Mult
c c
c
c c
Archive-
Archive-
Archive-
c
c
c
c

Figure

22: Aggregate Using a Broadcast Theory
7.1 Communication Between Aggregate and Components
Communication between components is handled at the aggregate level as described above. How-
ever, when the communication is between the aggregate and one of its components, the unification
of object-valued attributes and class sorts via event theories does not work since the class sort
of the aggregate is not created until after the colimit is computed. The solution requires the use
of a sort axiom that equivalences two sorts as shown below:
Using the bank example discussed above, assume the archive-withdrawal event is also received by
the Bank aggregate. The archive-withdrawal event theory is included in the Account class type
and, by the colimit operation, the Bank aggregate. To enable the Bank aggregate to receive the
archive-withdrawal event, a sort-axiom is used in the Bank specification to equivalence the Bank
sort of the aggregate with the Archive sort from the event theory as shown below.
Archive
Use of the sort axiom unifies the Bank sort and the Archive sort and thus the signatures of the
archive-withdrawal events defined in the event theory and the Bank aggregate become equivalent.
Communication from the aggregate to the components, or subcomponents, is much simpler.
Since the aggregate includes all the sorts, functions, and axioms of all of its components and
subcomponents via the colimit operations, the aggregate can directly reference those components
by the object-valued attributes declared either in itself or its components. Because an aggregate
is aware of its configuration, determining the correct object-valued attribute to use is not a
problem.
8 Discussion of Results and Future Efforts
8.1 Object Model
Our research establishes a formal mathematical representation for the object-oriented paradigm
within a category theory setting. In our theory-based object model, classes are defined as theory
presentations or specifications and the basic object-oriented concepts of inheritance, aggregation,
association, and inter-object communication are formally defined using category theory opera-
tions. While some work formalizing aspects of object-orientation exists [23],[8],[18],[24], [25], ours
is the first to formalize all the important aspects of object-orientation in a cohesive, computationally
tractable framework. In fact, our formalization of inheritance, aggregation, and association,
provides techniques for ensuring the consistency of object-oriented specifications based on the
composition process itself.
The completeness of our integrated model allows the capture of any object-oriented model as a
formal specification. Furthermore, the algebraic language O-Slang allows for straight-forward
translation into existing algebraic languages such as Slang or Larch for further transformation
into executable code. Thus this model provides a bridge from existing informal CASE tools
to existing formal specification languages, tying the ease of use of the former to the technical
advantages of the latter.
8.2 Application of Object Model
To show the applicability of the theory-based object model, we developed a proof of concept
parallel-refinement specification acquisition system. This system used a commercially available,
OMT-based, object-oriented CASE tool to capture the informal specification. This included
graphical representation of the object, dynamic, and functional models along with textual input
in the form of method definitions and class-level constraints (neither of these have a graphical
format defined in OMT and are generally easier to define directly using first-order axioms).
The output from the user-interface was then parsed and translated into O-Slang based on
the theory-based object model. The translation from graphically-based input to O-Slang was
completely automated.
Two complete object-oriented domain models were developed using this system: a school
records database and a fuel pumping station. These domains were chosen to demonstrate the
wide diversity of domains, stressing both functional and dynamic aspects, supported by this
model. In total, over 37 classes, including 76 methods and operations, 89 attributes, 5 aggregates,
events, and 7 associations were specified. These domain models were sufficiently large and
diverse to demonstrate the application of the theory-based model to support realistic problem
domains.
8.3 Future Plans
The definition of theory-based models that can be mapped 1:1 to an informal representation
provides the necessary framework for a parallel refinement system for specification development
as shown in Fig. 1. Our theory-based object model allows for the development of a domain
model as a library of class theories. This O-Slang representation can next be transformed
into a Slang specification in a straightforward manner to allow the full use of the Specware
development system. The Specware system has already demonstrated the ability to generate
executable code from algebraic specifications. Thus the technology now exists to transform
informal object-oriented models to correct executable code.
While the class theories can be translated into code, the desired approach is to treat them
as a full domain model. From this, a specific specification can be developed for input to design
processing. Thus the next step is the development of the specification generation/refinement
subsystem in Fig. 1, an "elicitor-harvester" that will elicit requirements from a user by reasoning
over the domain model and harvesting components of the domain model to build the desired
specification. The ability to map between an informal model and the theory-based object model
will allow the user to interface with the system using a familiar informal representation, while
the formal model can support the reasoning needed to guide the user as well as assuring that the
harvested specification remains consistent with the constraints of the domain model.

Acknowledgments

This work has been supported by grants from Rome Laboratory, the National Security Agency,
and the Air Force Office of Scientific Research.



--R

"Report on a Knowledge-Based Software Assistant,"
"Software Engineering in the Twenty-First Century,"
"KIDS - A Semi-automatic Program Development System,"
"Transformational Approach to Transportation Scheduling,"

"Diagrams for Software Synthesis,"
"Strategies for Incorporating Formal Speci- fications,"
"A Formal Semantics for Object Model Diagrams,"
"Statecharts: A Visual Formalism for Complex Systems,"
"Teaching formal extensions of informal-based object-oriented analysis methodologies,"
Formal Transformations from Graphically-Based Object-Oriented Representations to Theory-Based Specification
Kestrel Institute
"Some Fundamental Algebraic Tools for the Semantics of Computation Part I: Comma Categories, Colimits, Signatures and Theories,"
"Specifying a Concept-recognition System in Z++,"
"Object-Z: An Object-Oriented Extension to Z,"
"A Comparative Description of Object-Oriented Specification Languages,"
"Specification in OOZE with Examples,"
"Unifying Functional, Object-Oriented and Relational Programming with Logical Semantics,"
"Introducing OBJ3,"
"Algebraic Specification: Syntax, Semantics, Structure,"
"Category Theory Definitions and Examples,"
"Data Abstraction and Hierarchy,"
"Practical Consequences of Formal Defintions of Inheritance,"
"An Algebraic Theory of Object-Oriented Systems,"
"Modelling Multiple Inheritance with Colimits,"
--TR

--CTR
Ana Mara Funes , Chris George, Formalizing UML class diagrams, UML and the unified process, Idea Group Publishing, Hershey, PA,
software engineering;domain models;transformation systems;formal methods