106 Data Structure and Software Engineering: Challenges and Improvements
context Case inv: status=‘completed’ implies not (activity->exists(b |
b.oclIsTypeOf(SendInvoice) and b.status=‘completed’ and not b.next->exists(a |
a .oclIsTypeOf(PayGoods))) and activity->exists(b |
b.oclIsTypeOf(ReceiveGoods) andb.status=‘completed’ and notb.next->exists(a
|a.oclIsTypeOf(PayGoods))))
(c) e previous instances of two dierent Pay Good activities must have an
empty intersection.
context PayGoods inv: PayGoods.allInstances()-> forAll(s1,s2 |s1 <> s2 implies
s1.previous-> intersection(s2.previous)->isEmpty())
Acknowledgements
is work has been partially supported by the Italian grant FAR N. 4412/ICT, the
Spanish-Italian integrated action HI2006-0208, and ...