(* Title: JinjaDCI/J/State.thy
Author: Tobias Nipkow, Susannah Mansky
Copyright 2003 Technische Universitaet Muenchen, 2019-20 UIUC
Based on the Jinja theory J/State.thy by Tobias Nipkow
*)
section ‹ Program State ›
theory State imports "../Common/Exceptions" begin
type_synonym
locals = "vname ⇀ val" ― ‹local vars, incl. params and ``this''›
type_synonym
state = "heap × locals × sheap"
definition hp :: "state → heap"
where
"hp ≡ fst"
definition lcl :: "state → locals"
where
"lcl ≡ fst ∘ snd"
definition shp :: "state → sheap"
where
"shp ≡ snd ∘ snd"
(*<*)
declare hp_def[simp] lcl_def[simp] shp_def[simp]
(*>*)
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
¤
*© Formatika GbR, Deutschland
