10.2.2 Values包的良构规则

BagTypeValue

没有额外良构规则。

CollectionValue

没有额外良构规则。

DomainElement

没有额外良构规则。

Element

没有额外良构规则。

EnumValue

没有额外良构规则。

LocalSnapshot

[1] 同一时刻isPost和isPre只能有一个为真。

context LocalSnapshot
inv: isPost implies isPre = false
inv: isPre implies isPost = false

[2] 只有在快照是一个后置条件快照时，它才能关联有一个前置条件快照。

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

没有额外良构规则。

ObjectValue

[1] 对象的历史是有序的。第一个元素没有前趋，最后一个没有后继。

context ObjectValue
inv: history->oclIsTypeOf( Sequence(LocalSnapShot) )
inv: history->last().succ->size() = 0
inv: history->first().pre->size() = 0

OclMessageValue

[1] 在同一时刻，isSyncOperation, isAsyncOperation和isSignal属性只能有一个为真。

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] 返回消息只有在消息值是一个同步操作调用时才出现。

context OclMessageValue
inv: isSyncOperation implies returnMessage->size() = 1
inv: not isSyncOperation implies returnMessage->size() = 0

OclVoidValue

没有额外良构规则。

PrimitiveValue

没有额外良构规则

SequenceTypeValue

[1] 所有属于一个序列值的元素都有一个唯一的索引值。

context SequenceTypeValue
inv: self.elements->isUnique(e : Element | e.indexNr)

SetTypeValue

[1] 属于一个set值的所有元素必须有唯一值。

context SetTypeValue
inv: self.elements->isUnique(e : Element | e.value)

StaticValue

没有额外的良构规则。

TupleValue

[1] 属于一个元组值的所有元素具有唯一的名称。

context TupleValue
inv: self.elements->isUnique(e : NameValueBinding | e.name)

Value

没有额外的良构规则。