Use Case Pre/Post Conditions

Hello! What is an appropriate approach to modeling pre- and post conditions for a use case in SysML v2?

A use case’s objective is itself a requirement, so you model pre- and post-conditions the same way you would on any requirement: assume constraint for what must hold going in, require constraint for what must hold on completion.

use case def Withdraw {
    subject account : Account;
    actor customer : Customer;
    attribute amount : ScalarValues::Real;

    objective {
        assume constraint { account.balance >= amount }   // precondition
        require constraint { account.balance >= 0 }        // postcondition
    }
}