Z в Изабель

Я пытаюсь ввести и доказать спецификации Z в Isabelle.

Скажем, у меня есть спецификация торгового автомата, написанная в формате 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

Синонимы типов работают нормально, однако когда я добираюсь до точной схемы cash, которую я перевел как функции exact_cash, я продолжаю получать ошибки.

Итак, вкратце я просто хотел бы знать, как это сделать. входная схема в Изабель.

1 3
formal-languages

1 ответ:

Некоторые люди разработали фреймворки для Z-спецификаций в Isabelle / HOL (другая ссылка ) десять лет назад. (Насколько я знаю, они больше не поддерживаются – но, возможно, они все еще могут быть вам полезны.)

Обычно Z-спецификации могут быть переписаны в спецификации TLA довольно легко. Таким образом, вы также можете попробовать использовать активно поддерживаемую HOL-TLA-сессию Изабель.

Но давайте сначала остановимся на обычной Изабель / хол.

Кодирование ваш фрагмент Z-спецификации в plain Isabelle/HOL будет выглядеть примерно так: 

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
Обратите внимание, что я отбросил различие между входными и выходными переменными. Дельта-переменная VMSTATE в VM_operation разделяется на 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"
2