объект-Z спецификация кредитной карты с использованием затмения - PullRequest
Новая
       19

объект-Z спецификация кредитной карты с использованием затмения

0 голосов
/ 18 марта 2020

В настоящее время я пытаюсь запустить пример спецификации object-Z для класса CreditCard, но я столкнулся с проблемой при объявлении списка видимости и схемы INIT. Есть ли способ исправить это? Спасибо за чтение

в списке видимости сказано, что элементы не являются функциями класса

необъявленное имя: баланс

1 Ответ

0 голосов
/ 03 мая 2020

Я не уверен, что CZT хорошо справляется с Object Z.

В качестве примера большой спецификации Z, я предлагаю этот недавно загруженный проект: https://github.com/vinahradau/finma

Для примера кредитной карты я создал эту схему (CZT, а затем преобразовал в латекс), которая хорошо работает в 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
└

Латекс: 

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