Transcript From the OCL to JML - Department of Computer Science

By Karen Richart
The Object Constraint
Language (OCL)
 Formal specification
language that could be used
for constraining the model
elements that occur in a
UML diagram.
The Object Constraint
Language (OCL)
 Formal specification
language that could be used
for constraining the model
elements that occur in a
UML diagram.
The Java Modeling
Language (JML)
 Design for specifying java
classes and interfaces.
Motivation
 To be able to map UML object oriented designs with
OCL constraints to Java classes annotated with JML
specifications
WHY?
 Map object oriented design models expressed in UML
and OCL to Java classes annotated with JML
specifications
 Development of Java application using UML/OCL,
JML for later stages
 Can use tools that support JML to reason about
specifications, testing and verification
 JML same notation as Java
Basic Types
OCL
JML (Java)
 Boolean
 Boolean
 Integer
 int
 Real
 float/double
 String
 String
Boolean
Operators
 μ(b1 and b2) = μ(b1)
&& μ(b2)
 μ(b1 or b2) = μ(b1) ||
μ(b2)
and - &&
or - ||
implies - ==>
not - !
 μ(b1 implies b2) =
μ(b1) ==> μ(b2)
 μ(not b1) = !μ(b1)
Collection Operators
OCL
JML
 Collection(T)
 Object VS value collections
 Set(T)
 JMLObjectSet/JMLValueS
et
 Bag(T)
 Sequence(T)
 JMLObjectBag/JMLValue
Bag
 JMLObjectSequence/JML
ValueSequence
JMLValueSet VS
JMLObjectSet
JMLValueSet
 (\forall JMLType e; μ(s).has(e);
e instanceof JMLLong)
Set(Person)
(\forall Object p; μ(s).has(p);
p instanceof Person)
JMLObjectSet
 (\forall Object e; μ(s).has(e);
e instanceof T)
Common Operators
 μ(c->size()) = μ(c).size()
 μ(c->includes(e)) = μ(c).has(μ(e))
 μ(c->excludes(e)) = !μ(c).has(μ(e)).
What about excludesAll()?
 c1->excludesAll(c2)
 μ(c1->excludesAll(c2)) =
 (\forAll T e;μ(c2).has(e);!μ(c1).has(e))
Other operators
 μ(s->union(s1)) = μ(s).union(μ(s1))
 μ(s->intersection(s1)) = μ(s).intersection(μ(s1))
 μ(s->union(b)) = μ(s).toBag().union(μ(b))
Iterator Expressions
 μ(c->exists(e : T | p(e))) =
(\exists T e;μ(c).has(e);μ(p))
μ(c->select(e : T | p(e))) =
new JMLObjectSet{T e | μ(c).has(e) && μ(p)}
Operations not defined in
Java
 Library for OCL type that facilitates mapping
 Including classes for the collection types along with
their operations
 s->op(..) To s.op(.. )
class OclIntegerOperations {
max()
i1.max(i2)
μ(i1.max(i2)) =
OclIntegerOperations.max(i1,i2)
static public int max(int i1, int i2){
if (i1 > i2) {return i1;}
else {return i2;}
}
static public int min(int i1, int i2){
if (i1 < i2) {return i1;}
else {return i2;}}
}
Collections
 public class OclObjectSet extends JMLObjectSet{
public boolean includes(Object e) {this.has(e);}
//@ is the argument ‘==’ to one of the objects in the set
public int size() {this.size()};
//@ number of elements in the set
public boolean notEmpty() {!isEmpty(); }
//@ is the set not empty? }
context Title
Inv: availableCopies > 0 = copies->exists(isAvailable)
availableCopies >0 <==>
(\exists Copy c; copies.includes(c); c.isAvailable)
Exercise
Translate the following OCL constraint to JML
Solution ?
/*@ requires question->excludes(q) = !question.has(q);
@ ensures question == \old(question.union(q));
@*/
Thank You