[CZT-Users] Several questions

[Philippe de R. <ph...@fr...>]

Hello,

is there anyone in this list?

Does the oz compiler in Eclipse work?

When I click the + sign next to "Credit Card" class show below, to fold it,
Eclipse folds it right after "limit E {1000, 2000, ...}" which is obviously not the
class's end.

Furthermore, Eclipse displays a " syntax error at ZPROJ" next to the (limit, balance, etc.)  visibility list.

Any help would be much appreciated.

pr



┌  CreditCard
 Visibility list
 ⨡ ( limit, balance, INIT, withdraw, deposit, withdrawAvail  )
 
 Constant schema
╷
  limit: ℕ
|
 limit ∈ { 1000, 2000, 5000 }
└

 ┌─
  balance: ℤ
 |
   balance + limit >= 0
└

┌ Init 
  balance = 0
  └
┌ widthDraw 
  Δ ( balance )
  amount?: ℕ
 | 
 amount? <= balance + limit
 balance' = balance - amount?
└
┌ deposit 
  Δ ( balance )
  amount?: ℕ
 | 
balance' = balance + amount?
└

┌ widthdrawAvail 
  Δ ( balance )
  amount!: ℕ
 | 
amount! = balance + limit
balance' = - limit
└


 
└