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
└
└
|
