我正在尝试在 Isabelle 中输入和证明 Z 规范。
假设我有一个用 LaTeX 格式编写的自动售货机规范:
\begin{zed}
price:\nat
\end{zed}
\begin{schema}{VMSTATE}
stock, takings: \nat
\end{schema}
\begin{schema}{VM\_operation}
\Delta VMSTATE \\
cash\_tendered?, cash\_refunded!: \nat \\
bars\_delivered! : \nat
\end{schema}
\begin{schema}{exact\_cash}
cash\_tendered?: \nat
\where
cash\_tendered? = price
\end{schema}
我不知道我应该将模式作为引理还是函数?
这是我目前所拥有的:
theory vendingmachine
imports
Main Fact "~~/src/HOL/Hoare/Hoare_Logic"
begin
type_synonym price = nat
type_synonym stock = nat
type_synonym takings = nat
type_synonym cash_tendered = nat
function exact_cash "(cash_tendered:nat)"
where
cash_tendered ≡ price;
end
类型同义词工作正常,但是当我到达我已翻译为 exact_cash 函数的确切现金模式时,我不断收到错误。
总而言之,我只想知道如何将模式输入到 isabelle 中。
最佳答案
有人开发了frameworks for Z-specifications in Isabelle/HOL ( other link ) 十年前。 (据我所知,它们不再被维护——但也许它们仍然可以对你有所帮助。)
通常,Z 规范可以很容易地重写为 TLA 规范。因此,您也可以尝试使用积极维护的 HOL-TLA-session伊莎贝尔。
但让我们首先坚持使用常见的 Isabelle/HOL。
用纯 Isabelle/HOL 编码你的 Z 规范片段看起来像这样:
theory VendingMachine
imports
Main
begin
--"record datatype for the state variables"
record VMSTATE =
stock :: nat
takings :: nat
--"a vending machine is parameterized over a price constant"
locale VendingMachine =
fixes price :: nat
begin
definition VM_operation ::
"VMSTATE ⇒ VMSTATE ⇒ nat ⇒ nat ⇒ nat ⇒ bool"
where "VM_operation vmstate vmstate' cash_tendered cash_refunded bars_delivered ≡
True" --"TODO: specify predicate"
definition exact_cash ::
"nat ⇒ bool"
where "exact_cash cash_tendered ≡
cash_tendered = price"
end
end
请注意,我放弃了输入变量和输出变量之间的区别。 VM_operation
中的增量变量 VMSTATE
分为 vmstate
和 vmstate'
。
要真正使用这样的规范,您需要更多辅助定义。例如,规范的状态空间可以定义为归纳谓词,例如:
inductive_set state_space :: "VMSTATE set"
where
Init: "⦇ stock = 10, takings = 0 ⦈ ∈ state_space"
--"some initial state for the sake of a meaningful definition...."
| Step: "vmstate ∈ state_space
∧ (∃ cash_tendered cash_refunded bars_delivered .
VM_operation vmstate vmstate' cash_tendered cash_refunded bars_delivered)
⟹ vmstate' ∈ state_space"
关于formal-languages - Z 变成伊莎贝尔,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/31699357/