Use or Extend relationships in the flow modifique the postcondition?

Question

I understand that postcondition must be true, and the state that the system have to end the user story.

In a normal flow I can have many use or extend relationships with other use cases. For example, I have a use case See all vouchers. Its goal is that a user can see all the vouchers in the web portal. If the user wants, he/she can mark one voucher as "valid" or "not valid", (mark a voucher is another use case). I've shown it as a fourth step in my specification --if he/she wants mark it, jump to mark voucher use case --.

But I wonder what postcondition I should define for See voucher?

1. the user see all the vouchers
2. the user see all the vouchers and he can check one like "valid" or "not valid".
3. the user see all the vouchers and he can check one like "valid".

P.S: the happy path in "check voucher" is that the voucher be "valid". The "not valid" case is an alternative path.

Answer 1

Use cases might not be the tool you need

You seem to use use-case to decompose detailed functionality into more detailed functionality. Although this is not forbidden in UML, functional decomposition is not recommended, as it leads to unreadable use-cases. So better think about user-goals e.g. Review and verify vouchers

You may be tempted to model your user interface with use-cases. Don't! This is not a good idea, and the inventors of UML even strongly advised not to do that.

Finally, use-cases are not activities. You seem to describe a sequential ordering of activities: request to view all vouchers then open and verify one, etc... One step finishes before the next step is executed. For this, prefer activity diagrams. There is no notion of sequence in use-cases.

If you nevertheless want (or have to) use use-cases:

Preliminary remark about postconditions

A postcondition is a constraint that must be satisfied (true) at the end of a behavior. This means that:

IF the behavior is finished THEN the postcondition must be true.

In the formal verification, you could also make use of the logical contraposition

IF the postcondition is not true THEN the behavior should not be finished (unless the model or its implementation is buggy).

But the postcondition does not drive the behavior: the postcondition could be true from the beginning of the behavior or could become true at any moment of the behavior without interrupting/terminating it.

A typical example are postconditions on operations of stacks:

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   

Post condition of use cases

You could indeed state your post-condition in one of the way you've suggested. But two important remarks:

• Use cases are constraints that must be true at the end of the use-case. You should therefore be careful not to make the constraint too strong. So if a user is involved in a use case See all vouchers you would probably not expect that the user scrolls down and read all the 123 000 vouchers in the system and should not write "The user saw all the vouchers". So you could write a more prudent post-condition, like "The user could see a list of vouchers".
• Actors may be human users. As we all know, users are not necessarily rational. i'd therefore recommend to express the post-conditions in regard of the system and not the users. So "A list of vouchers was made available to the users".

It is important to realise that an «include» or «extend» dependency does not mean that the initial use-case is finished. If marking or checking is included (i.e. always happens) in See all vouchers or extends that use-case (i.e. it may sometimes happen), the See all vouchers continues until that use-case is finished, i.e. all the included and extending use-cases are finished as well.