Difference between revisions of "OCL"

From Suhrid.net Wiki
Jump to navigationJump to search
 
(33 intermediate revisions by the same user not shown)
Line 10: Line 10:
 
* In a program, assertions express constraints on program state that must be true at a '''specified point''' during execution.
 
* In a program, assertions express constraints on program state that must be true at a '''specified point''' during execution.
 
* In a model/diagram, they document what must be true of an '''implementation''' of a modelling element.
 
* In a model/diagram, they document what must be true of an '''implementation''' of a modelling element.
* Can have optional preconditions - (must be true when operation is invoked). for e.g. an argument to a certain operation cannot be null.
+
 
* Can have optional postconditions - (must be true when operation completes). for e.g. the operation must update the database when it completes.
+
== Pre and Post Conditions ==
 +
* They are assertions associated with operations of a class.
 +
* Preconditions - (must be true when operation is invoked). for e.g. an argument to a certain operation cannot be null.
 +
* Postconditions - (must be true when operation completes). for e.g. the operation must update the database when it completes.
 +
* Can both be optional.
 +
 
 +
== Class Invariants ==
 +
* Classes may have global properties, preserved by all methods in the context of all instances of the class.
 +
* This is captured by the class invariant - a statement of what is '''always''' true of '''each''' class's instance.
  
 
= Design by contract =
 
= Design by contract =
  
 
* A pre and post condition can be viewed as a '''contract''' between an operation and its invokers.
 
* A pre and post condition can be viewed as a '''contract''' between an operation and its invokers.
 +
** An extension to the contract imposed by abstract class specialisation, interface realization.
 
* Something like - "If the client promises to invoke the operation with the precondition satisfied, then the operation guarantees that its implementing methods will deliver a final state in which the postcondition is true".
 
* Something like - "If the client promises to invoke the operation with the precondition satisfied, then the operation guarantees that its implementing methods will deliver a final state in which the postcondition is true".
 
* So the invoker doesn't care about how final state is produced
 
* So the invoker doesn't care about how final state is produced
Line 48: Line 57:
 
* Note it does '''not''' have the same meaning as static.
 
* Note it does '''not''' have the same meaning as static.
 
* This means the balance for '''''any''''' BankAccount object must be within 0 and 250000.  
 
* This means the balance for '''''any''''' BankAccount object must be within 0 and 250000.  
* self means the same thing as "this".
+
* self means the same thing as "this". Whenever self is used it refers to the instance of the type that is the context of the OCL constraint. If the context is BankAccount, self refers to an instance
 +
of BankAccount. In many cases, self can be omitted because the context is clear.  
 
* In this case, self need not be mentioned (doesnt make a difference though)
 
* In this case, self need not be mentioned (doesnt make a difference though)
  
Line 97: Line 107:
 
=== Iterated Traversals ===
 
=== Iterated Traversals ===
  
 +
* Iterated traversals can produce bags.
 
* Navigations can be composed of multiple references - we can denote more paths through a diagram.
 
* Navigations can be composed of multiple references - we can denote more paths through a diagram.
 
* e.g All the people who work for a comapany
 
* e.g All the people who work for a comapany
Line 135: Line 146:
 
* oclIsKindOf(t:OclType):true, if self and t are the same type or self is of a class derived from t (This behaves like Java's instanceof operator)
 
* oclIsKindOf(t:OclType):true, if self and t are the same type or self is of a class derived from t (This behaves like Java's instanceof operator)
 
* oclInState(s:OclState):true, if selfis in the state specified by s. s is the name of some state in the statechartfor the class.
 
* oclInState(s:OclState):true, if selfis in the state specified by s. s is the name of some state in the statechartfor the class.
* oclIsNew():true if used in a postcondition and the object is created by the operation.  
+
* oclIsNew():true if used in a postcondition and the object is created by the operation.
** For e.g. if a new object is created as a postcondition ?
 
** TODO: come up with a better example
 
  
 
== Logic in OCL ==
 
== Logic in OCL ==
Line 162: Line 171:
 
* Collections have some built in operations (like Java's Collection class has methods like size(), toArray() etc) which are accessed through the "->" operator.
 
* Collections have some built in operations (like Java's Collection class has methods like size(), toArray() etc) which are accessed through the "->" operator.
 
* e.g. sum() is a pre-defined operation on integer collection, here salary is a bag of integers - representing salarys of all staff.
 
* e.g. sum() is a pre-defined operation on integer collection, here salary is a bag of integers - representing salarys of all staff.
* TODO: understand this: how come there is no self defined here, how to interpret iterative traversal when collections are involved ?
 
 
<syntaxhighlight lang="java5">
 
<syntaxhighlight lang="java5">
 
context Department
 
context Department
 
staff.contract.grade.salary->sum()
 
staff.contract.grade.salary->sum()
 
</syntaxhighlight>
 
</syntaxhighlight>
 +
* How this works is that staff (self.staff) where self refers to a department instance will return a bag of Person objects. staff.contract will then return a bag of contract objects (contracts for all person objects in previous bag), similarly a bag of grade objects, followed by a bag of salary objects. The operation sum() is then applied to this bag.
 +
 +
=== Iterating operations ===
 +
 +
* These operations iterate over each element in the collection and evaluate an expression on them.
 +
* Each operation takes an expression as a parameter.
 +
* The select, collect result in a new collection.
 +
* forAll, exists result in a Boolean.
 +
 +
==== select ====
 +
 +
* An operation which allows us to specify criteria by which we can pick certain objects from a collection.
 +
* Like an SQL Query.
 +
* e.g : specify an invariant for the company, that none of its employees should have a salary that exceeds 50000
 +
<syntaxhighlight lang="java5">
 +
context Company inv:
 +
employees->select(p:Person | p.contract.grade.salary > 50000)->isEmpty()
 +
</syntaxhighlight>
 +
 +
Here the select is working on bag of Person that employees produces. The first part of select specifies on which object we are applying the condition, then a '|' separator character, then the condition for the select. Then the operator isEmpty() is applied which will return true if the collection returned by the select is true.
 +
 +
==== collect ====
 +
 +
* Takes an expression as an argument and makes a collection which '''contains all values''' of the expression.
 +
* for e.g. this gives a bag of all ages of all employees in a department.
 +
* TODO: Note just this statement, probably doesnt make sense, because its not acting as a constraint.
 +
 +
<syntaxhighlight lang="java5">
 +
context Department
 +
staff->collect(p:Person | p.Age())
 +
</syntaxhighlight>
 +
 +
* Another usage of collect,
 +
 +
<syntaxhighlight lang="java5">
 +
context Person inv:
 +
self.parents->collect(brothers)->collect(children)->notEmpty()
 +
</syntaxhighlight>
 +
 +
instead of
 +
 +
<syntaxhighlight lang="java5">
 +
context Person inv:
 +
self.parents.brothers.children->notEmpty()
 +
</syntaxhighlight>
 +
 +
[TODO: ? Isnt the second notation simpler, isnt collect supposed to take an expression ]
 +
 +
==== forAll ====
 +
 +
* Returns true if a certain condition holds for all elements in the collection, false otherwise.
 +
 +
==== exists ====
 +
 +
* Returns true if there is atleast one object in a collection for which a certain condition holds.
 +
 +
=== constraints ===
 +
 +
* Some basic invariant constraints:
 +
 +
* A person's employer must be the same as the person's department's company.
 +
<syntaxhighlight lang="java5">
 +
context Person inv:
 +
self.employer == self.department.company
 +
</syntaxhighlight>
 +
 +
* None of the employees in a company can be under the age of 18
 +
<syntaxhighlight lang="java5">
 +
context Company inv:
 +
self.employees->select(age()<18)->isEmpty() [TODO : isnt the structure of the select mandatory to have, the p:Person | p.Age() < 18 ?)
 +
</syntaxhighlight>
 +
 +
=== Iterative constraints ===
 +
 +
* '''select''' is an iterative constraint [How ? : see TODO above ]
 +
* '''forAll''': return true if every member of collection satisfies the boolean expression. (something like Java containsAll())
 +
<syntaxhighlight lang="java5">
 +
context Company inv: grade->forAll(g:Grade|not g.contract->isEmpty())
 +
</syntaxhighlight>
 +
 +
* '''exists''': true if there is one member of the collection satisfying the boolean expression (something like Java contains)
 +
<syntaxhighlight lang="java5">
 +
context Department inv:
 +
staff->exists(e:Employee | e.manager->isEmpty())
 +
</syntaxhighlight>
 +
* '''allInstances''': returns all instances of a type and its subtypes. not always necessary to use it - Difficult to implement it.
 +
** Better to set the correct context, rather than use allInstances.
 +
e.g. context Grade inv: self.salary>20000 is better than Grade.allInstances->forAll(g:Grade | g.salary > 20000)
 +
** allInstances might be useful to specify change in objects known to a system, (maybe constrain the no of objects to a specific number ?)
 +
 +
=== Pre and post conditions ===
 +
 +
* Pre and post conditions are standard OCL '''constraints'''
 +
* Example: @pre refers to the balance in the prestate.
 +
<syntaxhighlight lang="java5">
 +
context Savings_Account::withdraw(intamount)
 +
pre: amount <= balance
 +
post: balance = balance@pre-amount
 +
</syntaxhighlight>
 +
 +
 +
=== Generalizations ===
 +
 +
* Generalizations '''CANNOT''' be navigated in OCL.
 +
* However they can be constrained. (TODO : Perhaps, we can say used in Constraints) e.g. by saying a certain generic type must be a certain specific type
 +
* e.g. a:Account and a.oclIsKindOf(CurrentAccount)
 +
 +
== Inheritance ==
 +
 +
* There are some recommendations that subclasses must adopt when it comes to constraints.
 +
 +
=== Invariants ===
 +
 +
* An invariant for a superclass is inherited by its subclasses. A subclass may strengthen the invariant but cannot weaken it.
 +
 +
e.g. Superclass Stove and subclass ElectricStove
 +
<syntaxhighlight lang="java5">
 +
 +
context Stove inv:
 +
temperature <= 200
 +
 +
//Strengthening the invariant
 +
context ElectricStove inv:
 +
temperature <= 150 
 +
 +
//Weakening the invariant
 +
context ElectricStove inv:
 +
temperature <= 300
 +
 +
</syntaxhighlight>
 +
 +
* Now assume If the max temperature withstandable by the client of a Stove class is 250C.
 +
* If the client gets Stove class, then it is safe to use.
 +
* If the client gets ElectricStove class where it has strengthened the invariant ... temp of ElectricStove cant be more than 150, it will be safe in the clients env.
 +
* Now, if ElectricStove weakens the constraint, then it is no longer safe to use with clients who expect to be using a Stove class.
 +
 +
=== Pre and post conditions ===
 +
 +
* A precondition may be weakened, not strengthened in a redefinition of an operation in a subclass.
 +
* A postcondition may be strengthened, not weakened in a redefinition of an operation in a subclass.
 +
 +
* Example:
 +
 +
<syntaxhighlight lang="java5">
 +
 +
context Stove::open()
 +
pre: status = off
 +
post: status = off and isOpen
 +
 +
context ElectricStove::open()
 +
pre: status = off or temp <=100 //Weakened precondition
 +
post: status = off and isOpen and greenLightOn //Strengthened postcondition
 +
 +
</syntaxhighlight>
 +
 +
* Now ElectricStove open() will work for more than 1 precondition - it can be substituted for a stove (status = off) or it can be opened when temp < =100.
 +
* Postcondition is strengthened : Ensures that orginal constraints are satisfied and makes it stronger.
 +
 +
* If precondition was stronger, then ElectricStove won't be able to open in conditions where Stove opened - so again we're breaking the contract.
 +
* If postcondition were weaker like only checking for isOpen, then it wont fulfill expectations by clients of Stove.
 +
 +
= Constraints in Prog Languages =
 +
 +
* Java supports assertions.
 +
* Typically assertions are handled in testing tools like JUnit.
 +
* However, it depends where assertions are implemented - in code or in the test.
 +
 +
== Class invariants ==
 +
 +
* A class invariant means something that always is true within the context of a class.
 +
* But, how can this be constrained using assertions ? Class invariant assertions need to be implemented at the end of every method. Ugly!
 +
 +
== False Preconditions ==
  
[[Category:OODE]]
+
* The client has an '''''obligation''''' to satisfy the precondition.
 +
* If the precondition is false - then it's the callers fault, this is helpful in tracking down errors.
 +
* The OCL contract does not say anything about what to do when the precondition is false.
 +
** Any approach can work - throw an exception, return an error code.
 +
** Or Just Crash !
 +
* The responsibility of ensuring that the invariant is true is spread across the classes.
 +
** Constructors, methods etc must ensure the invariant is true. Although during operations, the invariant could be false.

Latest revision as of 17:03, 7 January 2012

Introduction

  • How can we express constraints in UML ?
  • E.g. the balance attribute in a SavingsAccount class can never be less than zero and more than 100000.
  • UML only has a notion of an informal constraint in terms of a note - which can be attached to a model. However its just text.
  • To write formal and machine checkable constraints - we use the Object Constraint Language (OCL).

Assertions

  • In a program, assertions express constraints on program state that must be true at a specified point during execution.
  • In a model/diagram, they document what must be true of an implementation of a modelling element.

Pre and Post Conditions

  • They are assertions associated with operations of a class.
  • Preconditions - (must be true when operation is invoked). for e.g. an argument to a certain operation cannot be null.
  • Postconditions - (must be true when operation completes). for e.g. the operation must update the database when it completes.
  • Can both be optional.

Class Invariants

  • Classes may have global properties, preserved by all methods in the context of all instances of the class.
  • This is captured by the class invariant - a statement of what is always true of each class's instance.

Design by contract

  • A pre and post condition can be viewed as a contract between an operation and its invokers.
    • An extension to the contract imposed by abstract class specialisation, interface realization.
  • Something like - "If the client promises to invoke the operation with the precondition satisfied, then the operation guarantees that its implementing methods will deliver a final state in which the postcondition is true".
  • So the invoker doesn't care about how final state is produced
  • And the implementer doesn't need to worry about cases where the precondition is not true.
  • So a contract can be many things:
    • A specification of what a method should do.
    • Documentation - more precise than class interfaces.
    • Offers runtime checks for correctness.
    • Are a basis for testing.
    • Are a basis for formal proofs of programs correctness.

OCL

  • OCL is the constraint language for UML.
  • Used to write general constraints on UML as well as DBC.
  • Can apply to any modeling element, not only classes.
  • OCL Essential Capabilities:
    • Specifying which model element is to be constrained (the context).
    • Navigating through models to identify objects that are relevant to a constraint.
    • Asserting properties about links between objects.

OCL Context

  • Consider a BankAccountclass with an integer balance.
  • OCL constraint
context BankAccount inv:
self.balance>=0 and self.balance<=250000
  • The constraint is an invariant that applies in the context of the class BankAccount. Invariant for the context BankAccount means that the constraint holds true for all instances of BankAccount.
  • Note it does not have the same meaning as static.
  • This means the balance for any BankAccount object must be within 0 and 250000.
  • self means the same thing as "this". Whenever self is used it refers to the instance of the type that is the context of the OCL constraint. If the context is BankAccount, self refers to an instance

of BankAccount. In many cases, self can be omitted because the context is clear.

  • In this case, self need not be mentioned (doesnt make a difference though)

Navigation Expressions

  • We can refer to object that are linked to the context object.
  • We need to start from the context object. Consider the below example:

Ocl-navigation.jpg

  • To get the set of employees working in a department :
context Department
self.staff
  • The association name has to be followed
  • Think of it something like the below code in Java, to access the Person object,
class Department {
  private Set<Person> staff;

  public Set<Person> getStaff() {
    return this.staff;
  }
}
  • If there is no association name, then the class name at the destination end of the context object can be used.
  • The class name has to be in lower case
  • Eg to get the department from the company:
context Company
self.department
  • The multiplicity of the assocation will tell us how many objects are retrieved.
  • e.g. below OCL will retrieve one object
context Department
self.company

Iterated Traversals

  • Iterated traversals can produce bags.
  • Navigations can be composed of multiple references - we can denote more paths through a diagram.
  • e.g All the people who work for a comapany
context Company
self.department.staff

self.department will give a set of departments, and then .staff is applied to each department producing a set of people. If people were not unique to a department, then a bag of people would be returned.

Names and Invariants

  • An OCL invariant need not be applicable to any instance:
  • e.g.
context bart: Person inv
bart.age == 10
  • Here bart is an object of type Person and we are stating that for the object bart, the age will always be 10. This is the invariant constraint for a single object.
  • An invariant can be given a name:
context bart: Person inv how_old:
bart.age == 10

Basic types

  • OCL supports basic types such as boolean, integer, real, string
  • Collection types such as collection,set,bag,tuple, are also basic types.
  • Additionally, every class appearing in the UML class model can be used as a basic type in OCL.

Basic operations

  • oclIsTypeOf(t:OclType):true, if selfand t are the same type (This is sort of useless, better to use oclIsKindOf())
  • oclIsKindOf(t:OclType):true, if self and t are the same type or self is of a class derived from t (This behaves like Java's instanceof operator)
  • oclInState(s:OclState):true, if selfis in the state specified by s. s is the name of some state in the statechartfor the class.
  • oclIsNew():true if used in a postcondition and the object is created by the operation.

Logic in OCL

  • Three valued: true, false and undefined.
  • e.g. illegal type conversion can result in undefined.
  • What will be the result of combining OCL's logic operators together ? i.e. what is the truth table ?
  • An expression is undefined if one of its arguments is undefined, except:
    • true OR anything is true (conventional)
    • false AND anything is false (conventional)
    • false IMPLIES anything is true. (TODO: what does this mean)

Operations on objects and collections

  • Operations and attributes defined for classes in a model can be used in an OCL expression.
  • Example:
context Person
self.age()
self.contract.grade.salary
  • Collections have some built in operations (like Java's Collection class has methods like size(), toArray() etc) which are accessed through the "->" operator.
  • e.g. sum() is a pre-defined operation on integer collection, here salary is a bag of integers - representing salarys of all staff.
context Department
staff.contract.grade.salary->sum()
  • How this works is that staff (self.staff) where self refers to a department instance will return a bag of Person objects. staff.contract will then return a bag of contract objects (contracts for all person objects in previous bag), similarly a bag of grade objects, followed by a bag of salary objects. The operation sum() is then applied to this bag.

Iterating operations

  • These operations iterate over each element in the collection and evaluate an expression on them.
  • Each operation takes an expression as a parameter.
  • The select, collect result in a new collection.
  • forAll, exists result in a Boolean.

select

  • An operation which allows us to specify criteria by which we can pick certain objects from a collection.
  • Like an SQL Query.
  • e.g : specify an invariant for the company, that none of its employees should have a salary that exceeds 50000
context Company inv:
employees->select(p:Person | p.contract.grade.salary > 50000)->isEmpty()

Here the select is working on bag of Person that employees produces. The first part of select specifies on which object we are applying the condition, then a '|' separator character, then the condition for the select. Then the operator isEmpty() is applied which will return true if the collection returned by the select is true.

collect

  • Takes an expression as an argument and makes a collection which contains all values of the expression.
  • for e.g. this gives a bag of all ages of all employees in a department.
  • TODO: Note just this statement, probably doesnt make sense, because its not acting as a constraint.
context Department
staff->collect(p:Person | p.Age())
  • Another usage of collect,
context Person inv: 
self.parents->collect(brothers)->collect(children)->notEmpty()

instead of

context Person inv:
self.parents.brothers.children->notEmpty()

[TODO: ? Isnt the second notation simpler, isnt collect supposed to take an expression ]

forAll

  • Returns true if a certain condition holds for all elements in the collection, false otherwise.

exists

  • Returns true if there is atleast one object in a collection for which a certain condition holds.

constraints

  • Some basic invariant constraints:
  • A person's employer must be the same as the person's department's company.
context Person inv:
self.employer == self.department.company
  • None of the employees in a company can be under the age of 18
context Company inv:
self.employees->select(age()<18)->isEmpty() [TODO : isnt the structure of the select mandatory to have, the p:Person | p.Age() < 18 ?)

Iterative constraints

  • select is an iterative constraint [How ? : see TODO above ]
  • forAll: return true if every member of collection satisfies the boolean expression. (something like Java containsAll())
context Company inv: grade->forAll(g:Grade|not g.contract->isEmpty())
  • exists: true if there is one member of the collection satisfying the boolean expression (something like Java contains)
context Department inv:
staff->exists(e:Employee | e.manager->isEmpty())
  • allInstances: returns all instances of a type and its subtypes. not always necessary to use it - Difficult to implement it.
    • Better to set the correct context, rather than use allInstances.

e.g. context Grade inv: self.salary>20000 is better than Grade.allInstances->forAll(g:Grade | g.salary > 20000)

    • allInstances might be useful to specify change in objects known to a system, (maybe constrain the no of objects to a specific number ?)

Pre and post conditions

  • Pre and post conditions are standard OCL constraints
  • Example: @pre refers to the balance in the prestate.
context Savings_Account::withdraw(intamount)
pre: amount <= balance
post: balance = balance@pre-amount


Generalizations

  • Generalizations CANNOT be navigated in OCL.
  • However they can be constrained. (TODO : Perhaps, we can say used in Constraints) e.g. by saying a certain generic type must be a certain specific type
  • e.g. a:Account and a.oclIsKindOf(CurrentAccount)

Inheritance

  • There are some recommendations that subclasses must adopt when it comes to constraints.

Invariants

  • An invariant for a superclass is inherited by its subclasses. A subclass may strengthen the invariant but cannot weaken it.

e.g. Superclass Stove and subclass ElectricStove

context Stove inv:
temperature <= 200

//Strengthening the invariant
context ElectricStove inv:
temperature <= 150   

//Weakening the invariant
context ElectricStove inv:
temperature <= 300
  • Now assume If the max temperature withstandable by the client of a Stove class is 250C.
  • If the client gets Stove class, then it is safe to use.
  • If the client gets ElectricStove class where it has strengthened the invariant ... temp of ElectricStove cant be more than 150, it will be safe in the clients env.
  • Now, if ElectricStove weakens the constraint, then it is no longer safe to use with clients who expect to be using a Stove class.

Pre and post conditions

  • A precondition may be weakened, not strengthened in a redefinition of an operation in a subclass.
  • A postcondition may be strengthened, not weakened in a redefinition of an operation in a subclass.
  • Example:
context Stove::open()
pre: status = off
post: status = off and isOpen 

context ElectricStove::open()
pre: status = off or temp <=100 //Weakened precondition
post: status = off and isOpen and greenLightOn //Strengthened postcondition
  • Now ElectricStove open() will work for more than 1 precondition - it can be substituted for a stove (status = off) or it can be opened when temp < =100.
  • Postcondition is strengthened : Ensures that orginal constraints are satisfied and makes it stronger.
  • If precondition was stronger, then ElectricStove won't be able to open in conditions where Stove opened - so again we're breaking the contract.
  • If postcondition were weaker like only checking for isOpen, then it wont fulfill expectations by clients of Stove.

Constraints in Prog Languages

  • Java supports assertions.
  • Typically assertions are handled in testing tools like JUnit.
  • However, it depends where assertions are implemented - in code or in the test.

Class invariants

  • A class invariant means something that always is true within the context of a class.
  • But, how can this be constrained using assertions ? Class invariant assertions need to be implemented at the end of every method. Ugly!

False Preconditions

  • The client has an obligation to satisfy the precondition.
  • If the precondition is false - then it's the callers fault, this is helpful in tracking down errors.
  • The OCL contract does not say anything about what to do when the precondition is false.
    • Any approach can work - throw an exception, return an error code.
    • Or Just Crash !
  • The responsibility of ensuring that the invariant is true is spread across the classes.
    • Constructors, methods etc must ensure the invariant is true. Although during operations, the invariant could be false.