在流中使用或扩展关系修改后置条件？

Answer 1

用例可能不是您需要的工具

您似乎使用用例将详细功能分解为更详细的功能。尽管这在 UML 中不被禁止，但不建议使用功能分解，因为它会导致不可读的用例。所以最好考虑用户目标，例如Review and verify vouchers

您可能很想用用例来模拟您的用户界面。不！这不是一个好主意，UML 的发明者甚至强烈建议不要这样做。

最后，用例不是活动。您似乎描述了活动的顺序：请求查看所有凭证然后打开并验证一个，等等......在执行下一步之前完成一个步骤。为此，更喜欢活动图。用例中没有序列的概念。

如果您仍然想要（或必须）使用用例：

关于后置条件的初步说明

后置条件是在行为结束时必须满足（真）的约束。这意味着：

如果行为完成，则后置条件必须为真。

在形式验证中，您还可以使用logical contraposition

如果后置条件不正确，则行为不应完成（除非模型或其实现有问题）。

但是后置条件不会驱动行为：后置条件可以从行为开始就为真，或者可以在行为的任何时刻变为真而不会中断/终止它。

一个典型的例子是堆栈操作的后置条件：

context stack::push() post: self.size>0    
// This means: after a push on the stack the size of the stack is greater than 0
// But for the second push, the condition is already verified at the beginnin, but the push will never be performed   

用例的后期条件

您确实可以以您建议的一种方式陈述您的后置条件。但是有两个重要的说明：

• 用例是在用例结束时必须为真的约束。因此，您应该注意不要使约束过强。因此，如果用户涉及用例See all vouchers，您可能不会期望用户向下滚动并阅读系统中的所有 123 000 张凭证，并且不应该写“用户看到了所有的优惠券“。所以你可以写一个更谨慎的后置条件，比如“用户可以看到优惠券列表”。
• 参与者可能是人类用户。众所周知，用户不一定是理性的。因此，我建议表达有关系统而不是用户的后置条件。所以 ”向用户提供了优惠券列表”。

重要的是要意识到 «include» 或 «extend» 依赖并不意味着初始用例已经完成。如果在See all vouchers 中包含标记或检查（即总是发生）或扩展该用例（即有时可能发生），则See all vouchers 将继续，直到该用例完成，即所有包含和扩展的使用-案件也结束了。