Z dans Isabelle

Question

J'essaie de saisir et de prouver les spécifications Z dans Isabelle.

Dire que j'ai une spécification de distributeur automatique écrit dans le format 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} 

Je ne sais pas si je devrais mettre le schéma est comme lemmes ou fonctions?

C'est ce que j'ai jusqu'à présent:

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 

Les synonymes de type fonctionnent bien mais quand je reçois au schéma de trésorerie exact que je traduit par une fonction de exact_cash je continue à avoir des erreurs. Donc, en résumé, je voudrais juste savoir comment entrer des schémas dans isabelle.

Answer 1

Certaines personnes ont développé frameworks for Z-specifications in Isabelle/HOL (other link) il y a dix ans. (Pour autant que je sache, ils ne sont plus maintenus - mais ils peuvent peut-être encore vous aider.)

Habituellement, les spécifications Z peuvent être réécrites assez facilement dans les spécifications TLA. Donc, vous pouvez également essayer d'utiliser le HOL-TLA-session activement maintenu d'Isabelle.

Mais gardons d'abord le commun Isabelle/HOL.

Encoding votre fragment Z-spécification dans la plaine Isabelle/HOL ressemblerait à quelque chose comme:

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 

Notez que je supprimé la distinction entre les variables d'entrée et de sortie. La variable Delta VMSTATE dans VM_operation est divisée en vmstate et vmstate'.

Pour vraiment travailler avec une telle spécification, vous auriez besoin de plus de définitions auxiliaires. Par exemple, l'espace d'état de la spécification pourrait alors être définie comme un prédicat inductif comme, par exemple:

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"