タイプモデル（詳細）

• タイプの外部仕様

  • 静的モデル：静的タイプモデル・属性定義、不変量、等
  • 振る舞いモデル：オペレーション

Vending Machine

amont: Money

action insert_coin (value：Money)

post amountにvalueを追加

action check_availability (instructor, date)

post instructorが指定dateに授業を担当しているか否かを求める

Course Scheduling Machine

Client

Session

Instructor

grade:

full_schedule

*

*

staff

action buy_drink

pre amountは100円以上

post amountから100円を引く

前のｽﾗｲﾄﾞ

次のｽﾗｲﾄﾞ

最初のｽﾗｲﾄﾞに戻る

ｸﾞﾗﾌｨｯｸｽの表示