object-Z specification of credit card using eclipse

Question

i am currently trying to run an example of object-Z specification for the CreditCard class, but i encountered a problem when declaring the visibility list and INIT schema.Is there any way to fix this ? Thank you for reading

visibility list says the items are not features of the class

undeclared name : balance

Answer 1

I'm not sure CZT copes well with Object Z.

For an example of a big Z specification, I suggest this recently uploaded project: https://github.com/vinahradau/finma

For the credit card example, I created this schema (CZT and then converted into latex), which executes well in jaza.

CZT:

┌ LIMIT
  limit: ℤ
|
  limit ∈ {1000, 2000, 5000}
└

┌ BALANCE
  ΞLIMIT
  balance: ℤ
|
  balance + limit ≥ 0
└

┌ Init
  BALANCE ′
|
  balance′ = 0
└

┌ SetLimit
  ΔLIMIT
  limit?: ℕ
|
  limit′ = limit? 
└

┌ Withdraw
  ΔBALANCE
  amount?: ℕ
|
  amount? ≤ balance + limit
  balance′ = balance − amount?
└

┌ Deposit
  ΔBALANCE
  amount?: ℕ
|
  balance′ = balance + amount?
└

┌ WithdrawAvail
  ΔBALANCE
  amount!: ℕ
|
  amount! = balance + limit
  balance′ = -limit
└

Latex:

\begin{schema}{LIMIT}
 limit : \num 
\where
 limit \in \{ 1000 , 2000 , 5000 \}
\end{schema}

\begin{schema}{BALANCE}
 \Xi LIMIT \\
 balance : \num 
\where
 balance + limit \geq 0
\end{schema}

\begin{schema}{Init}
 BALANCE~' 
\where
 balance' = 0
\end{schema}

\begin{schema}{SetLimit}
 \Delta LIMIT \\
 limit? : \nat 
\where
 limit' = limit?
\end{schema}

\begin{schema}{Withdraw}
 \Delta BALANCE \\
 amount? : \nat 
\where
 amount? \leq balance + limit \\
 balance' = balance - amount?
\end{schema}

\begin{schema}{Deposit}
 \Delta BALANCE \\
 amount? : \nat 
\where
 balance' = balance + amount?
\end{schema}

\begin{schema}{WithdrawAvail}
 \Delta BALANCE \\
 amount! : \nat 
\where
 amount! = balance + limit \\
 balance' =~\negate limit
\end{schema}

Jaza:

JAZA> load C:\jaza\creditcard.
Loading 'C:\jaza\creditcard.' ...
Added 7 definitions.
JAZA> do Init
\lblot balance'==0, limit'==1000, limit''==1000 \rblot
JAZA> ; SetLimit
    Input limit? = 1000
\lblot balance'==0, limit'==1000 \rblot
JAZA> ; Deposit
    Input amount? = 10
\lblot balance'==10, limit'==1000, limit''==1000 \rblot
JAZA>
JAZA>
JAZA>
JAZA> ; Withdraw
    Input amount? = 5
\lblot balance'==5, limit'==1000, limit''==1000 \rblot
JAZA> ; WithdrawAvail
\lblot amount!==1005, balance'==-1000, limit'==1000, limit''==1000 \rblot
JAZA>