17.6.3 语义

交互操作数

交互操作数是联合片段的一个区域。只有带有true guards的交互操作数才被包括在语义的计算内。如果没有提供guard,也被认为是一个true guard。

交互操作数的语义由它的组成交互片段和隐含的seq操作来给出。

交互约束

交互约束总是与联合片段一块儿使用。

联合片段

联合片段的语义依赖于交互操作符。下面会对每种交互操作符类型做解释。

与一个联合片段关联的Gates代表了联合片段和它的环境之间的语法接口,是到其它交互片段的接口。

Consider Ignore Fragments

ConsiderIgnoreFragment是一个带有Ignore或Consider交互操作符值的联合片段。

Continuations

Continuations只有和Alternative联合片段和(弱)排序一块儿才有语义。

如果Alternative联合片段的一个交互操作数以一个名为X的Continuation结束,只有以Continuation X开始的交互片段才能被追加(appended)。

交互操作符种类值

交互操作符的值对于联合片段的语义非常重要,下面介绍每一个交互操作符枚举值。

Alternatives

交互操作符alt至少该联合片段代表的是一个行为的选择。最多一个操作数被选中。被选中的操作数必须有一个计算为真的显式或隐式guard表达式。隐式的true guard表明该操作数没有guard。

定义一个选择的轨迹集合是所有操作数的(guarded)轨迹的合集。

一个被else guarded的操作数指明它是所属封闭联合片段中所有其它guards析取的反。

如果所有有guard的操作数的guard都计算为假,那么它们都不执行,该封闭交互片段的其余部分被执行。

如果一个内部联合片段Gate用于一个alt联合片段的任一交互操作数中,那么具有相同名称的Gate必须用于这个alt联合片段的每个交互操作数内。

Option

交互操作符opt指示该联合片段代表一个行为的选择,其中(唯一)的操作数要么出现要么不出现(即,该选择是可选的)。一个option语义上等同一个alternative联合片段,其中只有一个操作数有非空内容,第二个操作数是空的。

Break

交互操作符break指示该联合片段代表了一个阻断场景,其中的操作数执行而该封闭交互片段中的其后部分则不执行。当带有guard的阻断操作符的guard为真时,所属封闭交互片段的剩余部分将被忽略。当阻断操作数的guard为假时,这个阻断操作数被忽略,其所属封闭交互片段其后的部分被选择。在不带guard的阻断操作数和所属封闭交互片段其后部分之间无法作出选择决策。

带有阻断交互操作符的联合片段应该覆盖封闭交互片段所有的生命线。

Parallel

交互操作符par指示该联合片段代表了多个操作数行为之间的一个并行合并。不同操作数的出现规约可以以任意方式交错,只要每个操作数内保持应用的次序。

一个并行的合并定义了一个轨迹的集合,它们描述了操作数的出现规约可能交错的各种方式而不妨碍每个操作数内部出现规约的次序。

Weak Sequencing

交互操作符seq指示该联合片段代表了多个操作数行为之间的一个弱序。

弱序由具有如下特点的轨迹的集合来定义:

  1. 每个操作数内的出现规约的次序在结果中仍然维持。
  2. 来自不同操作数的不同生命线上的出现规约可以以任意次序出现。
  3. 来自不同操作数的相同生命线上的出现规约是有序的,第一个操作数的出现规约先于第二个操作数的。

当所有的操作数作用于分离的参与者集合时,弱序退化为一个并行合并。当所有的操作数作用于一个参与者时,弱序退化为一个严格序。

Strict Sequencing

交互操作符strict指示该联合片段代表了所有操作数行为之间的一个严格序。

Negative

交互操作符neg指示该联合片段代表了定义为无效的轨迹。

使用neg交互操作符的联合片段所定义的轨迹集合就是它的(唯一)操作数中给出的轨迹的集合,只不过这个集合是一个无效的集合而非有效的轨迹。所有不同于Negative的交互片段都被认为是有意义的(它们描述的轨迹是有效并且应该是可能的)。

Critical Region

交互操作符critical指示该联合片段代表了一个关键区域。关键区域意味着该区域内的轨迹不能被其它出现规约(在那些由该关键区域所覆盖的生命线上)所交错。这意味着当封闭片段决定有效轨迹时该区域是以原子的形式被对待的。即使封闭的联合片段可能暗示一些出现规约可能交错进入该区域,例如使用par操作符,这可以通过定义一个区域来阻止。

因此封闭构造的轨迹集合由关键区域来限制。

Ignore/Consider

交互操作符ignore指示有些消息类型没有显示在这个联合片段中。这些消息类型被认为不重要并且如果它们出现在一个相应的执行中可以隐含地被忽略。作为一种选择,可以把ignore理解为被ignore的消息类型可以出现在轨迹中的任何地方。

相反,交互操作符consider指示哪些消息应该在这个联合片段中被考虑。这等价于定义其它的消息可以被忽略。

Assertion

交互操作符assert指示该联合片段代表一个断言。断言操作数中的序列是唯一有效的contiuations,所有其它的continuations都导致无效的轨迹。断言通常与Ignore或Consider联合使用,如图17.17。

Loop

交互操作符loop指示该联合片段代表了一个循环。这个循环操作数将会重复多次。

Guard可能包括迭代的下限和上限,以及一个布尔表达式。其语义是该循环会迭代至少‘minint’次(由guard中的迭代表达式给出)至多‘maxint’次。在执行了‘minint’次之后如果布尔表达式为假,那么循环终止。循环构造代表了一个seq操作符的迭代应用,其中循环操作数在前一次迭代结果之后被序列化。

如果该循环包含一个独立的带有一个规约的交互约束,那么循环只有在该规约计算为真的情况下才继续而不管是否达到了循环所规定的最小迭代次数。

results matching ""

    No results matching ""