formal-languages - Z 变成伊莎贝尔

Question

我正在尝试在 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 中。

Answer 1

有人开发了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"