Z in Isabelle
I am trying to introduce and prove the Z specs in Isabelle.
Let's say I have a vending machine specification written in LaTeX format:
\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}
I don't know if the circuit should be put as lemmas or functions?
This is what I have so far:
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
The type synonyms work great, but when I get to the exact cash schema, which I translated as exact_cash functions, I keep getting errors.
So, I would just like to know how to inject a schema into isabelle.
source to share
Some people developed a framework for the Z-specs in Isabelle / HOL ( another link ) ten years ago. (They are no longer supported as far as I know, but maybe they can help you.)
Usually the Z specifications can be easily rewritten into the TLA specifications. So you can also try to use the actively maintained HOL-TLA session Isabelle.
But let's stick with the general Isabelle / HOL first.
Encoding a Z-BOM snippet in plain Isabelle / HOL would look something like this:
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
Note that I have reversed the distinction between input and output variables. The delta variable VMSTATE
in VM_operation
is split into VMSTATE
and vmstate'
.
To actually work with such a specification, you need a few more helper definitions. For example, the state space of a specification can then be defined as an inductive predicate, for example, for example:
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"
source to share