|
The set of name value bindings that hold the changes in time of the subvalues of the associated object value. |
|
The sequence of OclMessageValues that the associated ObjectValue at the certain point in time has sent, and are not yet put through to their targets. |
|
The sequence of OclMessageValues that the associated ObjectValue at the certain point in time has received, but not yet dealt with. |
|
The predecessor of this local snapshot in the history of an object value. |
|
The successor of this local snapshot in the history of an object value. |
|
If this snapshot is a snapshot at postcondition time of a certain operation execution, then pre is the associated snapshot at precondition time of the same operation in the history of an object value. |
|
A sequence of name value bindings that hold the arguments of the message from the source to the target. |
|
The object value that has sent this signal. |
|
The object value for which this signal has been intended. |
|
The ocl message value that holds the values of the result and out parameters of a synchronous operation call in its arguments. Is only present if this message represents a synchronous operation call. |
context LocalSnapshot
inv: isPost implies isPre = false
inv: ispre implies isPost = false
context LocalSnapshot
inv: isPost implies pre->size() = 1
inv: not isPost implies pre->size() = 0
inv: self.pre->size() = 1 implies self.pre.isPre
= true
NameValueBinding context ObjectValue
inv: history->oclIsTypeOf(
Sequence(LocalSnapShot) )
inv: history->last().succ->size = 0
inv: history->first().pre->size = 0
context OclMessageValue
inv: isSyncOperation implies isAsyncOperation =
false and isSignal =
false
inv: isAsyncOperation implies isSyncOperation =
false and isSignal =
false
inv: isSignal implies isSyncOperation = false and
isAsyncOperation =
false
[2] The return message is only present if, and only if the ocl
message
value is a synchronous operation call. context OclMessageValue
inv: isSyncOperation implies
returnMessage->size() = 1
inv: not isSyncOperation implies
returnMessage->size() = 0
self.element->isUnique(e : Element |
e.indexNr)
SetTypeValue self.element->isUnique(e : Element |
e.value)
StaticValueself.elements->isUnique(e : Element | e.name)
context LocalSnapshot
def: let allPredecessors() : Sequence(LocalSnapshot)
=
if pred->notEmpty then
pred->union(pred.allPredecessors())
else
Sequence {}
endif
def: let allSuccessors() : Sequence(LocalSnapshot) =
if succ->notEmpty then
succ->union(succ.allSuccessors())
else
Sequence {}
endif
ObjectValue context ObjectValue::getCurrentValueOf(n:
String): Value
pre: -- none
post: result =
history->last().bindings->any(name = n).value
context OclExpEval::outgoingMessages() :
Sequence( OclMessageValue )
pre: -- none
post:
let end: LocalSnapshot =
history->last().allPredecessors()->select( isPost = true
)->first() in
let start: LocalSnapshot = end.pre in
let inBetween: Sequence( LocalSnapshot ) =
start.allSuccessors()->excluding(
end.allSuccessors())->including( start ) in
result = inBetween.outputQ->iterate (
-- creating a sequence with all
elements present once
m : oclMessageValue;
res: Sequence( OclMessageValue )
= Sequence{}
| if not
res->includes( m )
then res->append( m )
else res
endif )
endif
context TupleValue::getValueOf(n: String):
Value
pre: -- none
post: result = elements->any(name = n).value