z-notation - 使用 eclipse 的信用卡的 object-Z 规范

Question

我目前正在尝试为 CreditCard 类运行 object-Z 规范的示例，但是在声明可见性列表和 INIT 模式时遇到了问题。有什么办法可以解决这个问题吗？感谢您阅读

可见性列表表示这些项目不是该类的特征

未申报名称：余额

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>