使用 Eclipse 的信用卡对象 Z 规范

Question

我目前正在尝试运行 CreditCard class 的对象 Z 规范示例，但是我在声明可见性列表和 INIT schema.Is 时遇到了问题解决这个问题的方法？感谢阅读

visibility list says the items are not features of the class

undeclared name : balance

Answer 1

我不确定 CZT 能否很好地应对 Object Z。

大Z规范的例子，推荐这个最近上传的项目： https://github.com/vinahradau/finma

对于信用卡示例，我创建了这个模式（CZT，然后转换为乳胶），它在 jaza 中执行得很好。

长春：

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

乳胶：

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

使用 Eclipse 的信用卡对象 Z 规范

object-Z specification of credit card using eclipse

z-notation