(* Title: JinjaThreads/J/State.thy
Author: Tobias Nipkow, Andreas Lochbihler
*)
chapter ‹JinjaThreads source language›
section ‹Program State›
theory State
imports
"../Common/Heap"
begin
type_synonym
'addr locals = "vname ⇀ 'addr val" ― ‹local vars, incl. params and ``this''›
type_synonym
('addr, 'heap) Jstate = "'heap × 'addr locals" ― ‹the heap and the local vars›
definition hp :: "'heap × 'x → 'heap" where "hp ≡ fst"
definition lcl :: "'heap × 'x → 'x" where "lcl ≡ snd"
lemma hp_conv [simp]: "hp (h, l) = h"
by(simp add: hp_def)
lemma lcl_conv [simp]: "lcl (h, l) = l"
by(simp add: lcl_def)
end
¤ Dauer der Verarbeitung: 0.3 Sekunden
¤
*© Formatika GbR, Deutschland
