t15.use

UML设计测试工具

-- $ProjectHeader: use 2-3-0-release.1 Mon, 12 Sep 2005 20:18:33 +0200 green $

model t15  -- pre-/postconditions

class A
operations
  op1(p1 : Integer) : String
    post: 'AAA' <> 'BBB'
end

class B
attributes
  c : Integer
end

association R between
  A[*]
  B[1]
end

constraints

context a : A 
  inv: a.b.c >= 0

context A::op1(p1 : Integer) : String
  pre:  p1.mod(2) = 0
  pre:  b.c > 0
  post: b.c@pre = 0
  post: self@pre.b.c = 0
  post: Set{1,2,3}->notEmpty
  post: result = 'foo'

context A::op1(p1 : Integer) : String
  post: true