Z в Isabelle

Question

Я пытаюсь ввести и доказать спецификации 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 

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

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

Answer 1

Некоторые люди разработали frameworks for Z-specifications in Isabelle/HOL (other link) десять лет назад. (Насколько я знаю, они больше не поддерживаются, но, возможно, они могут помочь вам.)

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

Но давайте сначала придерживаться общей Изабель/HOL.

Кодирование ваш фрагмент Z-спецификации в виде простого 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"