The Strong Object Invariant
Yüklə 222,23 Kb.
|
- Bu səhifədəki naviqasiya:
- Conceptual definitions
- Basic elements of the analysis of object invariants
- As Prescribed Analysis
- As Described Analysis
- Conclusions
|
The Strong Object Invariant Dušan Malbaški 1, Aleksandar Kupusinac 1 1 Faculty of Technical Sciences, Trg Dositeja Obradovića 6, 21000 Novi Sad, Serbia Abstract – The concept of an invariant is fundamental to object-oriented programming, because it provides information on the overall behaviour of the class and/or its objects. An invariant is a predicate, that is true in every state that is proclaimed as valid. A strong invariant is a predicate, that is true in every valid state and false in every invalid state. Basically, we can divide them into two categories: object invariants and class invariants. Object invariants describe the consistency of object, i.e. non-static fields. Analysis of invariants takes the most important place in object-oriented program verification and can be directed in two ways – as prescribed and as described. This paper considers both analyses which are based on the strongest dynamic postconditions of methods with the guard as the precondition, thus, determining all possible transitions and only them. In addition, since dynamic postconditions are logical functions of the initial-final states, our solution is based solely on the first-order predicate logic. Keywords – Invariants, Object oriented programming, Program correctness, Program verification.
Object-oriented programming has been created through evolution, as a response to the software market requests. Therefore, already during the development of theory and practice the factual situation was established in which there are different views on the fundamental concepts of object-oriented methodology – class, object and invariant. The terminology used in object-oriented programming is not satisfactory, because in addition to synonymy, it often meets reckless use of the entrenched terms from other fields of science (especially philosophy). The main problem with the definitions in object-oriented programming is that they all have a free form not allowing the object and the class to have independent definitions. In this paper we explain the conceptual definitions of class, object and invariant [1] that are based on concepts. By definition, a concept is the thought on the essential characteristics of the unit of observation [2]. With this approach, we can clearly explain what is the class invariant, and what is object invariant. Analysis of invariants is a central point when it comes to analyzing the semantics of class or semantics of object-oriented programs [3]. The importance of invariants in the analysis of the class semantics is clearly described by Bertrand Meyer [4]: “To me the notion of the invariant is one of the most illuminating concepts that can be learned from the object-oriented method. Only when I have derived the invariant (for a class that I write) or read and understood it (for someone else’s class) do I feel that I know what the class is about.”. Invariant is every predicate that is true in any valid state, while may or may not be true in an invalid state. In particular, the predicate that uniquely separates the set of valid and set of invalid states, we call the strong invariant. In other words, a strong invariant is any predicate that is true in every valid state and false in every invalid state. However, since all the strong invariants uniquely separate sets of valid and invalid states, we conclude that all strong invariants are uniform to the level of equivalence [5]. Based on conceptual definitions, invariants in the class are basically divided into object and class invariants. Invariant property means that all the methods are activated by one and only one object-representative (i.e. this) and describes all valid states in which that object can be found. Analysis of invariants can be directed in two ways:
In this paper we will consider both analyses of object invariants based on the strongest dynamic postconditions of methods with the guard as the precondition, provided that it determines all reachable states and only them. In the Section 2 we consider conceptual definitions of class, object and invariant. Basic elements of the analysis of invariants are given in the Section 3. In the Sections 4 and 5 we consider as prescribed and as described analyses, respectively.
During the design of an information system, an object-oriented developer would spend most of his time for modelling. However, it should be noted here that a developer deals with thoughts, not with actual participants of the information system. Therefore, our presentation will begin with a definition of the concept:
where the term unit of observation should be understood in the broadest sense, as a unit of observation and/or thinking. Characteristics of the unit can be divided into essential and inessential. The thought of any characteristic is called property, and the thought of the essential characteristic is called the essential property [2]. Inessential properties can be de rived from the essential. For example, properties of the con cept TRIANGLE are being a convex polygon and having three sides, while the altitudes equality in an equilateral triangle is not an essential property, because it follows from the equality of its sides. Concepts can be classified in various ways, but for our consideration, the most important is a division between individual and class concepts. Individual concepts refer to indivi dual units of observation. Individual units that have co mmon properties constitute a class, and the thought of a given class is the class concept. Thus, individual concepts HAYDN, MOZART and BEETHOVEN are the thoughts of famous composers who have in common that they belong to the period of classicism, and that their work is more or less related to Vienna. Based on common properties, they constitute a class, and thought of this class is the class concept VIENNA CLASSICISTS. Obviously, individual concepts may or may not be rea listic, while the class concepts are not. For example, the class con cept VIENNA CLASSICIST is not realistic, while the individual concept MOZART is realistic (com poser Mozart existed in the period 1756-1791 yr.). How ever, both individual and class concepts TRIANGLE are not realistic. The more abstract class concepts can be obtained from class concepts by the method of abstrac tion, thus creating a hierarchy of classes, which has a tree structure. For instance, from the class concept VIENNA CLASSICIST, we can obtain more abstract class con cept COMPOSER, and from this more abstract class concept ARTIST etc. It is customary to begin learning object-oriented pro gra mming with a consideration of the term entity. By ISO definition, an entity is any concrete or abstract thing that exists, that existed or could exist, including connections between these things. We prefer to treat entity as a synonym for the unit of observation and find that there is no need to put it to the forefront, because as already stated, information system developer deals with con cepts, i.e. thoughts. Consideration of all essential properties of a concept in general is often a difficult philosophical question, since it is not an easy task do decide whether some feature is essential or not. In order to avoid such difficulties we stick to the problem domain. In contrast to the logician, the software developer does not have to take into account all essential properties, but just those that are relevant, i.e. those that are of interest for a given problem domain. For example, designer of information systems for tax administration for the concept CITIZEN will choose properties name, identification number, address, data on income etc., but certainly will not choose the properties height and weight, although every citizen has them. On the other hand, the designer of information systems for health care institu tions, next to the name, identification number, address, etc., will safely select the height and weight, because these properties are essential in determining the patient treatment, while dropping data on income. Let us introduce the following definitions:
Now, we can define a class:
The class concept properties are divided into two groups: features and fragments. The class concept may also contain other class concepts, and we call them fragments. For instance, class concept CAR has the feature colour and the fragment MOTOR. The features can be descriptive, such as colour, weight, etc., and operational as well as the possibility of movement, ability to fly and so on. Now we present the conceptual definition of the object:
These definitions have two major advantages over the va rious definitions that can be found in the literature on object-oriented programming. Firstly, conceptual definitions are based on concepts, i.e. the well-elabora ted and clear system of terms and their mea nings. Secondly, the conceptual definitions of class and object are equal in the semantic sense, i.e. class is not defined over the object or vice versa. Obviously, a conceptual aspect of class and object puts them in equal position. The difference is that the class corresponds to a class concept, and the object to an indivi dual concept. Classes and objects are interrelated by an assumption, which actually has the power of a postulate:
For example, each object isosceles triangle (with specific side length values) belongs to the class Isosceles triangle. Fragments and features of the class appear in the class case, while the fragments and features of the individual object appear in the individual case. For instance, if the class feature is colour, then the individual feature appears as white or green. The concepts can be complex which means that their fragments themselves may have fragments, and so on. A book consists of chapters, chapters contain paragraphs, paragraphs lines and lines contain characters. The concept structure is the set consisting of the concept itself, its frag ments, and further their fragments, etc., all moderated by the relation to be a fragment. If the concept does not include fragments, but only features, we say that it has a simple structure. If it contains at least one fragment, then the concept has a com plex structure. For example, the concept CAR contains fragment MOTOR, so it has complex structure. The concept POINT contains only features, such as coordinate values, so we say that it has a simple structure. Since the object models an individual concept, by modelling the concept structure we get the object structure. Similarly, we can talk about simple and complex object structures. The essential characteristics of an object are that it has the identity, state and behaviour [9]. The conceptual de finition is not in conflict with these essential characteris tics. Indeed, since each individual concept has identity that uniquely defines it, this property is mapped on the object, as its model, and each object has identity that uniquely defines it. The state of an object with a simple structure determines its descriptive features. The state of an object with complex structure determines its descriptive features, as well as states of its fragments. If we now consider this conclusion using a different crite rion, i.e. if we firstly look the object state set, then it follows that the descriptive features are derived from the state, i.e. they are functions of the state. In the imple mentation phase the data members represent des criptive features, while the object members represent fragments. Operational characteristics determine the object behaviour, which is described by its methods. By the definition of the object, it logically follows that the objects of the same class have the same structure and same behaviour. Class and object are related exactly as the data type and variable in standard programming languages. For example, int variables are occurren ces (instances) of int type and objects are occurrences (instances) of their class. Among all the concept features, both descriptive and operational, some never change: they constitute an invariant. For the concept TRIANGLE, no matter whether it is an individual or class concept, feature Modelling assumes the choice of the finite set of relevant features, both descriptive and operational. At the same time, it implies the choice of invariant features that are relevant to the particular model. Such features are called invariant relevant features. All invariant relevant features describe the concept essence in a given problem domain. Above mentioned features
Based on the fact that the invariant feature can be descriptive as well as operational, after modelling, we get several types of invariants [7]:
In addition, there are invariants that are defined in the implementation phase, although they may not be in the problem domain. For example, a sequential stack with capacity Consider now an object with a simple structure containing only the data-members of some type. Say, if data-member  (the triangle side length) is of the type real number, the question is - does this type matches the corresponding relevant concept feature? Although everything seems logical, unfortunately, the answer is negative, because the length of the triangle side may be of the type length, only. Such type does not exist in any programming language, but we have to improvise and say that the data-member is of the type positive real number. However, it does not end the problem, because the question is - can any three positive real numbers represent the side lengths of a triangle? Again the answer is negative, because these three numbers must satisfy the triangle inequality theorem (the sum of the lengths of any two sides of triangle is greater that the length of the third side). In other words, the invariant relevant feature of the concept TRIANGLE must be valid. It is now abundantly clear problem - on the one hand we have requests coming from the nature of the concept feature, and on the other hand we have the reality imposed by the descriptive power of programming languages. Therefore, it is fully justified to divide the final set of abstract states into two disjoint subsets, which are sets of valid and invalid states. For example, when it comes to a triangle, state (3, 4, 5) is valid, while states (-3, -4, -5) and (5, 1, 1) are invalid.
Let the class  contain only non-static fields  . To the class we assign a finite nonempty set of abstract states  . The set of all fields of the class is denoted by  . Assuming that there is at least one field in the class it follows that  Ø, so  Ø.
Definition 1. (Abstract state space) The abstract space of the class is a nonempty finite set of abstract states that is assigned to the class .
The abstract state space we di vide into two disjoint parts, namely the sets of valid states  and invalid states  . The set of valid states is assumed to be nonempty. Null-state  is a valid (quasi) state that an object occupies before its construction or after its destruction, i.e. when  , where  stands for the representative object. The set of all methods in the class is denoted by  provided that  Ø.
Definition 2. (Invariant) Let the class contain only non-static fields. An invariant in the class is every predicate  defined over its abstract state space that is true in every valid state.
Definition 3. (Strong invariant) Let the class contain only non-static fields. Strong invariant in the class is any predicate  defined over with the properties:
Note that the invariant must be true in all valid states, whilst in invalid states it may or may not. In the class Hoare triples [10], [11] are two special formulas of the first-order predicate calculus [12] defined over the abs tract state space . We introduce dynamic form of the total correctness formula (DTCF) in the object orien ted environment:
shortly denoted by  , where the postcondition  is now dynamic [13], meaning that it is a func tion of initial and final states, thus representing the tran sition function. In order to avoid confusion we will de note dynamic postconditions by the sign “ ^ ”. The structures of static and dynamic total correctness for mulas are the same. The predicate can be for mally replaced by the predicate  such that  , so the mathematical apparatus developed in the scope of static postconditions may be used for dynamic with out any restrictions, e.g. all general laws of Hoare logic hold in dynamic environment as well, such as the laws of consequence, conjunction, disjunction etc. The inter pretation of formula is the following – if the predicate  is true in some state then the method  terminates from that state and the transition will occur that satisfies the dynamic predicate  . The set of all states from which a method terminates is described by a special predicate called guard [14], [15].
Definition 4. (Guard) The guard of the method denoted by  is a predicate with the following properties:
Definition 5. (Strongest dynamic postcondition) The strongest dynamic postcondition of the method with respect to the precondition is predicate  if:
The most important case is the strongest dynamic postcondition with the guard
In the as prescribed analysis invariant is given in advance and we prove the class or object correctness with respect to the given invariant [6]. Definition 6. (Class correctness) Class , with strong invariant , is correct iff:
 ,
for all methods  .
Theorem 1. (As prescribed analysis) Let be strong invariant of the class . If
 ,
where  , then class is correct.
Proof. Let and
Based on property (1) from the Definition 5, we infer
Based on the second Hoare law of consequence, by (1) and (2) we obtain
Now, let us consider the following class written in Java: public class K { private int n; public K() { n=0; } public void m() { n++; if(n>10) throw new RuntimeException(); } } with the strong invariant:  .
Based on the class  ,
 ,
 ,
Since  ,
 ,
we obtain  ,
i.e.
 ,
and we conclude that class is correct.
In the as described analysis we assume that the object or class behaves correctly and based on that we derive the invariant [7]. Let the predicate  describe some valid states of the class and only them. Let us form the following recursive sequence of predicates:
Algorithm 1.  ,
 ,
 ,
where  . Consequently,
 .
Let  ,
where  ,  .
Lemma 1. The function  is monotonic on the chain  .
Proof. Suppose that Q.E.D. Lemma 2. The function has the least fixpoint on the chain .
Proof. By Tarski theorem [16] and Lemma 1, the function Q.E.D. Further, if  is the least fixpoint (Lemma 2) then obviously
 ,
where  . For the sake of simplicity we introduce the function  :
 .
Theorem 2. (As described analysis) The predicate  is a strong object invariant in the class , where  stands for null-predicate.
Proof. The predicate Q.E.D. Now, let us consider the previous Java class: public class K { private int n; public K() { n=0; } public void m() { n++; if(n>10) throw new RuntimeException(); } } Based on the class , we obtain:
,
,
,
 .
We adopt that  ,
 ,
 ,
 .
Since  we conclude that the predicate  is a fixpoint and
is the strong object invariant.
Conceptual definitions, given in this paper, allow independent consideration of class and object characteristics. From this conclusion, it is possible to clearly classify invariants in the class, which is the basis for the analysis of in variants. Analysis of class invariants has a central place in the class semantics, and therefore in the se mantics of object-oriented programs. Analysis of invari ants can be as prescribed, where the invariant is given in advance and as described, where the invariant is derived from the class. In this paper we have presented both analyses of object invariants that are based on the strongest dynamic postconditions of methods with the guard as the precondition. Acknowledgements This work was partially supported by the Ministry of Science and Education of the Repub lic of Serbia within the projects: ON 174026 and III 044006. References
Corresponding author: Aleksandar Kupusinac Institution: Faculty of Technical Sciences, University of Novi Sad, Novi Sad, Serbia E-mail: sasak@uns.ac.rs TEM Journal – Volume 1 / Number 1 / 2012. ISSN: 2217-8309 , www.tem-journal.com Yüklə 222,23 Kb. Dostları ilə paylaş:
|
is an invariant, where 
and 
are the descriptive features that represent side lengths, 
, where 
, 
and 
are the descriptive features that represent the values of internal angles. Obviously such an invariant holds, regardless of the changes (transfor mations) on the concept. Apparently, there are infinitely many invariants, all of which together build the concept essence.
is restricted to 
is an invariant in the class 
.
.
⊤
, i.e. if the precondition 
⊤
.
,
.
as the precondition. Let 
determines all valid transitions that can be accomplished by 
.
.
. The set 
of the form
. Obviously, it follows that
, where 
. Let 
, then 
, where 
. According to the property 
and 
and conclude that 
, i.e. 
. Based on that, we conclude that the function 
.
describes null-state and only it. By 
transitions are also valid. Thus the left to right implication holds, i.e. 
. Now, suppose that 
is a valid state such that 
. That means that the state 
. Since both implications hold, the equivalence 
also holds and that proves the theorem.
and form the following recursive sequence of predicates: