3 Specificarea formalã a obiectelor

3 Formal object specification

The importance and the role of abstract data-types (ADT) in the object model is unanimously accepted. Meanwhile, even if it is generally asserted that a class represents a possible implementation of an ADT, this aspect is exploited only marginally by the OOL. For almost all of these languages, the ADT specification borders to the signature of the interface operations, possibly accompanied by an informal description. On the other hand, even if the virtues of formal specifications have been proved in practice, and some of them mathematically demonstrated, their integration in the OOL has been made very timidly. The specification of an ADT always assumes the formal specification of the behavior. This is why we have studied some formal-specification techniques and the automatic translation of the specifications in a programming language. Chapter 3 presents the relation object model - formal specification, the advantages of formal algebraic specifications, the conclusions we have reached after specifying a data-structure "library" and a few applications.

3.1 The Object Model, a fruitful framework for using Formal Specifications

The use in a common framework of functional type formal descriptions and of the concepts promoted by the object model is possible and profitable.[Goguen87]. It represents one of the important features of the object model.

The mathematical tools used for this purpose are the ordered-sorted algebras and the category-theory. The purpose proposed - the effective use of the benefices that can be offered by making a symbiosis between the formal specification and the heuristic methods that have proved their viability in implementing the object model.

The notions of specification and implementation are relative because both concerns the realization of some descriptions. Having a class description, it is difficult to distinguish its role: specification or implementation. This depends primarily on the level in which the specification is used in the software development process.

Figure 3.1 The relationships between specification and integration techniques [Breu92]

Some languages have tried to promote a convergence of specification and implementation. From the specification languages family we can name FOOPS among the most representative ones[Rappanotti92]. In the specification-implementation language family, Eiffel is without doubt the most worthy. Even if between the two there are quite a few differences, they also have common features. First of all, both are labeled specification, design and implementation languages. FOOPS stresses specification and design aspects, while Eiffel concentrates mainly upon design and implementation.

The algebraic approach and the use of the object specification techniques by the means of the Hoare demonstration systems (promoted by Eiffel) represent two different specification techniques. The demonstration techniques specify the objects behavior by predicates which describe:

the class invariants,

the methods pre-conditions and post-conditions.

Predicates are given in the terms of object attributes, so they depend on data representation. The relationships between state (independent or dependent) specification techniques and the implementation techniques are presented in figure 3.1.

As the notion of implementation is based on a semantic relation between models, it is independent from the style chosen for object description. It can be applied in the case of an objects axiomatic description (like in FOOPS, for example), as well as in the case of an algorithmic description (like in OOL).

The FOOPS related consideration takes into account first of all the following criteria requested for the specification languages when using formal techniques, presented in [Lano94]:

the formal (mathematical) definition of the semantics;

a practical reasoning system based on this semantic;

a "refining" system which would permit the translation of the specifications in executable code, preferably in a compositional manner.

FOOPS satisfies all the three before mentioned criteria. Our research concentrates upon the efficiency of the translation process of the specifications in executable code (written in an OOL of which the use is far wider than that of the specification language), as well as upon the checking possibilities offered by the specification language.

Among the benefits which can be obtained from the use of formal specifications we can mention:

the behavior checking possibilities and the conformity achieved between specification and implementation;

an increased independence between the class behavior description and its structure;

the possibility of automatically implementing specifications in different OOL;

the use of a common environment for specification and design and a natural advance to implementation.

Related to obtaining these benefits we have the following remarks to make:

The techniques which are presently available do not permit a complete behavioral checking for an application; such an objective is not even taken into consideration in short or medium term. Nevertheless, the progress made in this direction are important. Within FOOPS, and implicitly in the subset implemented by us, checking assumes the use of rewriting techniques for the equational axioms.

A totally independent (from the object state) behavioral-description is possible only for a few number of objects. Thus, sooner or later it is imperative that a connection between the specification of the behavior and the object state be made.

As in most situations, to obtain information you must pay a price. On the one hand, the code written for specification is not always as legible as the one used for implementation. On the other hand, it is difficult, if not impossible that within a functional-type language to specify data structures with direct access that be efficient at execution (ex. arrays). The fact that functional languages favor recursive specifications sometimes constitutes an advantage, but sometimes take a heavy toil from the performance of execution times.

3.2 Algebraic specification languages

Definition 3.2.1

Let P(A) be the set of A subsets. Then, a specification language is characterized by:

S, a set of syntactical objects or specifications,

A, a set of semantic objects,

M:S® P(A), a semantic function,

If SÎ S is a specification and AÎ M(S) then A is called S specification model.

The syntactic objects of a specification language are also called algebraic specifications. Specifications are made of keywords, user declared identifiers and operators. The difference between a program and a specification is that the latter is an abstract description, while the program is a concrete description, executable by a machine. Some specialists say that any specification must be executable [Fucs92].

The semantic objects of specification languages are the multi-sorted algebras, shortly algebras. These represent mathematical structures which consider objects different from data. Objects have states, while data do not. Data are grouped in sorts, and objects in classes.

Taking into consideration what has been said before, it is clear that the specification language notion encompasses more than the algebraic specification, which it contains. The differences among the specification languages come mainly from the different options related to the syntactical objects (S), semantical objects (A) and the semantic function (M).

Specifications can be made with:

equational axioms (ex. Pop(push(x, s))=s)

conditional equational axioms (ex. GetCount(L)=Zero() if isEmpty(L)),

first-order axioms (which add the quantifiers $ and " , but the expressive capability remains low relating to the induction principles or to expressing the minimality properties of sorts,

first- order axioms +inductive definitions.

Related to the algebraic types as semantic objects, we have the following options:

sorts + total functions,

sorts + partial functions,

sorts + predicates + partial functions.

As for semantic functions, there are the following cases to take into consideration:

M(S) contains only one algebra, also called situation with initial algebra (a model used for the description by equational axioms).

M(S) contains any number of algebras, also called situation with free semantics (used when describing by first-level axioms),

M(S) contains only minimal algebras, also called situation with minimal algebras.

The methodology used by FOOPS, consequently also by the subset m FOOPS, is characterized by the use of:

specifications described by conditional equational axioms

sort-algebras + partial functions,

a semantic described by an initial algebra.

3.3 mFOOPS specification

3.3.1 Basic notions

The language is a subset of the standard FOOPS, made on the basis of some practical restrictions.

The functional module is the main programming unit at functional level in FOOPS, which encapsulates executable code. A functional module defines one or more abstract data types, formed of an elementary data set and the operations defined on them. Data are entities with non-modifiable state, like numbers and colors. A data set is called sort, and the associated operations functions. A functional module can be described syntactically in the following way:

fmod <ModId> is

<...>

endf

A sort is defined by a syntactic declaration like:

sort <SortId>.

and a function by:

fn <FnId>: <SortIdList> -> <SortId>.

The chosen mFOOPS subset allows only the definition of functions in prefixed (or standard) form.

The description of a function's behavior is made with the help of axioms. Axioms are equalities, possibly conditioned by a Boolean expression. The terms are syntactic constructions made by functions call, that is by referring a variable declared by:

var <VarId>: <SortId>.

Consequently, the axiom form is:

[c]ax <Term> = <Term> [if <Term>].

The object module is the main specifying and programming unit at object level in FOOPS, which encapsulates executable code. Within an object module it is possible to define one or more classes, which are potential object collections. The attributes and methods associated to a class describe the objects' internal state and the operations which can alter it. Moreover, an object module can contain definitions of abstract data types. The syntactic construction by which an object module is described is:

omod <ModId> is

<...>

endo

classes being introduced by:

class <ClassId>.

respectively by,

subclass <ClassId> < <ClassList>.

The attributes, as well as the methods, are described syntactically by:

at <AttrId> : <ClassId> <TypeId> -> <TypeId>

[default : (<Term>)].

me <MethId> : <ClassId> < TypeId> -> <ClassId>.

The semantic properties of attributes and methods are formulated with the help of conditional or non-conditional axioms. In this situation it is permitted that besides functions and variables, attributes and methods should appear in the terms.

Syntax of m FOOPS specifications:

<FOOPS specifications>	::=	<Module> {<Module>}
<Module>	::=	< Functional Module > \| < Object Module >
<Functional Module>	::=	fmod <ModId> is [<Import List >] < Functional Declaration > {< Functional Declaration >} endf
<Object Module >	::=	omod <ModId> is [<Import List >] < Object Declaration > {< Object Declaration >} endo
<Import List>	::=	using <ModId> "." {using <ModId> "."}
<Functional Declaration>	::=	< Sort Declaration > \| < Function Declaration > \| < Variable Declaration > \| <Axiom>
<Object Declaration>	::=	< Functional Declaration > \| < Class Declaration > \| < Attribute Declaration > \| < Method Declaration >
<Sort Declaration>	::=	sort <SortId> ["[" library "]"] "."
<Function Declaration>	::=	fn <FnId>: {<TipId>} -> <TipId> ["[" library "]"] "."
<Variable Declaration>	::=	var <VarId>: <TipId> "."
<Class Declaration>	::=	class <ClassId> ["[" library "]"] "."\| subclass < ClassId > "<" {< ClassId>} ["[" library "]"] "."
<Attribute Declaration>	::=	at <AttrId>":" {<TypeId>} "->" < TypeId> [ "[" default ":" "(" <Term> ")" "]" ] [ "[" redef "]" ] [ "[" library "]" ] "."
<Method Declaration>	::=	me <MethId> ":" {< TypeId>} "->" < TypeId> [ "[" redef "]" } [ "[" library "]" ] "."
<Axiom>	::=	ax <Term> "=" <Term> "."\| cax <Term> "=" <Term> if <Term> "."
<Term>	::=	<VarId> \| <OppId>"("<Term>{"," <Term>}")" \| new <ClassId>

3.3.2 Module import relation

A module can import other modules, at functional as well as at object level. The module import relation defines module hierarchies, because if a module M is imported by a module M', then it is imported by any other module that imports M'. Thus, it can be said that the module import relation defines the inheritance at a module level, inheritance meaning the inclusion of lower-level modules in higher level ones. The module import relation has the following properties:

it is explicitly defined, the importing module having to name all the import modules (in the import list),

it is multiple, any module being able to import any number of modules,

it is not recursive, a module not being able to import itself, be it directly or by means of imported modules.

The structure of FOOPS specifications resembles a direct acyclic graph in which nodes are modules, and the arcs express the import relations between them. Even if standard language permits three possibilities to import modules - protecting, extending and using, in mFOOPS importing is only allowed in using mode. The other two possibilities have restrictions regarding the use of the imported module, which, even if not hard to verify, have no correspondent in object-oriented programming languages.

The import o a module A by a module B is made by including in module B the declaration:

using A.

Besides the normal interdiction of using recursive import declarations, the following are also prohibited: importing an object module by a functional one and the direct and repeated import of the same module.

3.3.3 The inheritance relation

Standard FOOPS allows inheritance at sort level as well as at class level. m FOOPS only allows class inheritance, sort inheritance being considered unimportant. From our point of view, sorts have to be used only at the declaration of basic types, and we considered that at this level inheritance is irrelevant.

A class without superclasses is declared by:

class B.

Superclass specification is made when declaring the class by:

subclass A < B C D.

This declares class A as direct inheritor of classes B, C and D. The mentioned superclasses must be declared in the current module or in a module imported by it. The lack of a superclass declaration is considered an error. The semantic support of the inheritance relation is given by the inclusion relation at the sorted algebras level, used at semantic class modeling.

The checks made on these declarations by the mFOOPS compiler signal:

the uniqueness of names for sorts and classes, any duplication being considered an error;

the inexistence of cycles in the class inheritance relationship; if a cycle is detected, then the classes that are part of it are shown and the compilation is finished

repeated and direct inheritances from the same class (ex. subclass A<B B.) are considered simple (not repeated) relationships and are shown to the user as a warning

the error due to the sort inheritance.

3.3.4 Variable declarations

Associate an identifier, the variable name, to a sort or class type. The visibility domain of such a variable is the entire module where the declaration appears. For example, a Boolean variable X is declared by:

var X : Boolean.

From the restrictions related to variable use we can mention that:

the use in the same module of two variables with the same name is forbidden, even if they are of different types,

a variable's sort or class type must be declared in the same module where the variable is declared or in an module imported (directly or indirectly) by the former.

3.3.5 Operation signature

Functions, methods and attributes are referred to by the generic term of operations. We continue by presenting a few semantic aspects related to these entities.

3.3.5.1 Functions

Can be declared in functional or object modules by syntactic declarations such as:

fn <FnId>: {<TypeId>} -> <TypeId>.

that mention the function name, the value domain and the result type.

The last two characteristics are also referred to by function arity.

3.3.5.2 Attributes

Are defined by syntactic constructions such as:

at <AttrId>: <ClassId> {<TypeId>} -> <TypeId>

[default: (<Term>)]

[redef].

that can only appear in object modules.

The checks made on attribute signature are similar to those made for function signature. Thus, the types mentioned in the domain and the result type must be defined in the current module or in a module imported by it. Moreover, in this situation it is compulsory that the domain not be void and that the first indicated type be a class (an aspect underlined in the syntactic description by <ClassId>). This class is considered the class of the attribute. Any infringement of these rules is considered error.

Attributes can be classified in stored and calculated (derived). The value of a stored attribute is explicitly retained within the object and can be directly modified by using a method. The value of a derived attribute is obtained by evaluating an expression that can have as terms other attributes or functions. Derived attributes cannot be directly actualized; in other words, the value of a derived attribute depends directly on the value of the stocked attributes included in its expression. Derived attributes represent what in the database community is called calculated or virtual fields. They are the correspondents of Eiffel functions. It is often unclear whether an attribute must be stored or calculated, the choice being purely conventional.

In m FOOPS there is no syntactic distinction between derived and stored attributes. An attribute is considered stored if there is no axiom to tell its value.

A memorized attribute can have an implicit variable defined. This value is declared by the clause default, like in the following example:

at Age: Person -> Integer [default: (Zero())].

In m FOOPS, redefining an attribute or method must be explicitly specified with the clause redef.

3.3.5.3 Methods

Are operations that change the object states by modifying the value of one or more attributes. The method effect is described by axioms. The syntax of a method declaration is similar to that of functions and attributes. It is:

me <MethId>: <ClassId> {<TypeId>} -> <ClassId> [redef].

Method and attribute declarations can appear only in object modules. The use of undefined types or the methods definition for sorts is considered an error. The meaning of the redef clause is the same as in the case of attributes. It specifies that in descendents, a method redefines the superclass method with the same signature.

3.3.5.4 Entry-time objects

Are the object-level equivalent of constants (0 arity functions) from the functional level. They are objects that serve to define a special situation, as the object Empty, used to define an empty list. An entry-time object is declared by the following syntactic construction:

me <ObjId>: -> <ClassId>.

For this type of declarations, the existence of a class definition referred by ClassId, in the current module or in one of the imported ones is checked. The lack of this declaration is considered an error.

3.3.6 The redefining rule

Every syntactic attribute or method declaration is checked to see whether it redefines a declaration or not. We say that the attribute with the signature:

at Attr: Class1 <Type1List> -> Type1.

is correctly redefined by:

at Attr: Class2 < Type2List> -> Type2 [redef].

if and only if:

Class2 is Class1's own subclass,

every type from the list <Type2List> is equal to or is a subtype of the corresponding type in <Type1List> and the two lists have the same dimension,

Type2 is a subtype of Type1 (a type is his own subtype).

A method with the signature:

me Meth: Class1 < Type1List> -> Class1.

redefines the method:

me Meth: Class2 <Type2List> -> Class2.

if and only if:

Class1 is Clasa2's own subclass,

every type from the list <Type1List> is equal to or is a subtype of the corresponding type in <Type2List> and the two lists have the same dimension,

In the case of a redefinition, it is checked whether this one is explicitly mentioned [redef]. If not, the compiler signals the redefinition to the user by a warning and considers it implicit. The existence of a duplicate is considered an error.

3.3.7 Term types

Syntactically, a term is defined by:

(1) <VarId>

(2) [ClassId:]< OppId>({<ListTerms>})

(3) new <ClassId>

A term can be:

a reference to a variable,,

an operation call,

the call of operator new followed by a class name.

The checking made upon the term depends on their kind and are in fact a trial to establish every term type.

3.3.8 Axiom checking

In m FOOPS, axioms are used to describe functions and methods behavior. Axioms can be conditioned or not and are defined by:

ax <LeftTerm> = <RightTerm>.

cax < LeftTerm > = < RightTerm > if <Condition>.

The checks made upon axioms depend on the operation nature (function, method or derived attribute) which is described by the axiom. Thus, first, the operation defined by the axiom is identified, after which specific checks are made depending on its nature.

3.3.8.1 Function axioms

If the left term of an axiom is a function call then it is considered that the axiom defines that function. For example, the axiom:

ax Not(True())=False().

Where the functions Not, True and False are defined in the BOOLEAN module.

In the case of these axioms, the types of the left and right terms are verified, as well as the axiom's condition and it is verified whether the right term type is equal to or is a subtype of the left term. The axioms used at function defining are not taken into consideration at the code generation.

3.3.8.2 Axioms for derived attributes

An axiom defines an attribute referred by AttrName if the left term has the following form:

AtrName (X1,...,Xn),

where X1,...,Xn are variable references.

3.3.8.3 Method axioms

Method behavior is described by the use of axioms, that can be classified in direct and indirect axioms.

Direct axioms specify the actualized attributes and the actualization value after method execution. The left term of a direct axiom has the following form:

AttrName (MethName (X1,...,Xn))

Where MethName is the name of the specified method. AttrName is the name of the modified attribute and X1,...,Xn are variable references.

Indirect axioms define the methods using a method expression. Syntactically, an indirect axiom has the following form:

ax MethName (X1,...,Xn) = <MethExpression>.

where MethName is the name of the method specified by the axiom, X1,...,Xn are distinct variable references and <MethExpression> is a method expression, a term with special properties. Method expressions are built with the ";" operator, the semantics of which being equivalent to that of sequential composition. Formally, method expressions are defined by:

3.3.8.4 Axioms for entry-time objects

In the case of entry-time objects it is possible to specify the initial attribute values with axioms. These have the following form:

ax AttrName (EntryTimeObject ())=<Term>

Where EntryTimeObject is the name of the entry-time object, AttrName is the attribute which needs a value and <Term > is that value.

3.4 The m FOOPS class library

3.4.1 The need for and the role of class libraries

Any object-oriented language, and thus all object-oriented specification languages must be implemented in an "environment" which must also contain a class collection the role of which is to offer the basic components for application building. In our case, the library has had a supplementary connotation. Firstly, it has been used for compiler and language testing, thus offering a first feedback necessary in the error elimination process, and secondly it offered a compulsory test set to validate the language and extend it with new concepts.

3.4.2 Choosing classes for a first library

Being a specification language that wants to generate code in imperative OOLs (in our case, C++ and EIFFEL) the first thing to do was the basic types (Boolean, Integer, Character, Real, String) specification. Even if for some basic types the behavior can be completely specified (see Integer, Boolean), out of considerations related exclusively to the efficiency of the generated code we preferred to present the interface signature and to make the implementation directly in C++ or Eiffel).

Secondly, the specification of the fundamental data structures is the next type family which must belong to any component library.

Contrary to the purely functional specification languages, in which no information related to component structure is presented, in m FOOPS this structure must be specified. From the point of view of structure, the implementations made, undoubtedly represent a "point of view" (many implementation variants being possible). The variant we chose resembles to the Smalltalk style. An important difference relative to Smalltalk is that the demonstration of the implementation conformance with the functional specification is easier to do in m FOOPS.

3.5 Conclusions

After the language specification and after the compiler, m FOOPS library and some project design and implementation, the following results have ensued:

Even if it has a very simple syntax, the language permits a natural behavior specification, suggestive concerning the implementation mechanism.

The extension of m FOOPS (and implicitly of the compiler) with generic types would considerably increase the expressing capacity and the components' structuring possibilities.

If code generation is an important objective of a specification language, the state-modifying operations and the operations that allow instance printing must be the first ones to implement (as they allow incremental component testing even in the realization phase).

The representation of class relationships with diagrams is extremely useful in the case of algebraic specifications too. It allows a bird's eye view, thus helping when taking some implementation decisions (optimal parent choice, comparison of the interfaces of different components).

The symbiosis of the object model and the algebraic specifications is favored by the promotion of decentralization and of the description of different abstraction levels. The application of the above-mentioned principles supports component specification at a fine granularity level. Thus, the realization of the specifications is much easier to do and understand.

The construction of a high reusable component library represents, in the case of formal algebraic specifications too, the first condition that must be fulfilled to promote the components' algebraic specifications. Difficulties that must be overcome even in simpler cases (see the specifications of the Bag class), probably constitute one of the reasons for which the dissemination of algebraic specifications did not proceed conforming to the very optimistic foreseeing of over a decade.

One of the possible solutions could be the automatic specification for the components described using state transition diagrams charts. This solution is perfectly feasible as conditional equational axioms allow that the behavior be directly expressed relating to the state of the object (and the actions that are executed after a transition are in fact assignments) or permit the message sending to the objects related to the one described.

The algebraic specification of some entities (classes) offers greater checking possibilities. The price that must be paid is not limited only to the difficulty of specification. In some cases, the use of an OCL type formalism or even the direct description of the behavior in a programming language is much more intelligible.