Commit fa3f99f5 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

The first of Achim D. Brucker's three entries

parent 014d0d5b7c4c
......@@ -8337,6 +8337,28 @@ abstract =
2) executable, i.e., we can generate executable code from our
specification.
 
[Core_SC_DOM]
title = The Safely Composable DOM
author = Achim D. Brucker <https://www.brucker.ch>, Michael Herzberg <http://www.dcs.shef.ac.uk/cgi-bin/makeperson?M.Herzberg>
topic = Computer science/Data structures
date = 2020-09-28
notify = adbrucker@0x5f.org, mail@michael-herzberg.de
abstract =
In this AFP entry, we formalize the core of the Safely Composable
Document Object Model (SC DOM). The SC DOM improve the standard DOM
(as formalized in the AFP entry "Core DOM") by strengthening
the tree boundaries set by shadow roots: in the SC DOM, the shadow
root is a sub-class of the document class (instead of a base class).
This modifications also results in changes to some API methods (e.g.,
getOwnerDocument) to return the nearest shadow root rather than the
document root. As a result, many API methods that, when called on a
node inside a shadow tree, would previously ``break out''
and return or modify nodes that are possibly outside the shadow tree,
now stay within its boundaries. This change in behavior makes programs
that operate on shadow trees more predictable for the developer and
allows them to make more assumptions about other code accessing the
DOM.
[Store_Buffer_Reduction]
title = A Reduction Theorem for Store Buffers
author = Ernie Cohen <mailto:ecohen@amazon.com>, Norbert Schirmer <mailto:norbert.schirmer@web.de>
......
An overview of the formalization is given in:
Achim D. Brucker and Michael Herzberg. A Formal Semantics of the Core DOM
in Isabelle/HOL. In The 2018 Web Conference Companion (WWW). Pages 741-749,
ACM Press, 2018. doi:10.1145/3184558.3185980
A BibTeX entry for LaTeX users is
@InProceedings{ brucker.ea:core-dom:2018,
abstract = {At its core, the Document Object Model (DOM) defines a tree-like
data structure for representing documents in general and HTML
documents in particular. It forms the heart of any rendering engine
of modern web browsers. Formalizing the key concepts of the DOM is
a pre-requisite for the formal reasoning over client-side JavaScript
programs as well as for the analysis of security concepts in modern
web browsers. In this paper, we present a formalization of the core DOM,
with focus on the node-tree and the operations defined on node-trees,
in Isabelle/HOL. We use the formalization to verify the functional
correctness of the most important functions defined in the DOM standard.
Moreover, our formalization is (1) extensible, i.e., can be extended without
the need of re-proving already proven properties and (2) executable, i.e.,
we can generate executable code from our specification.},
address = {New York, NY, USA},
author = {Achim D. Brucker and Michael Herzberg},
booktitle= {The 2018 Web Conference Companion (WWW)},
conf_date= {April 23-27, 2018},
doi = {10.1145/3184558.3185980},
editor = {Pierre{-}Antoine Champin and Fabien L. Gandon and Mounia Lalmas and Panagiotis G. Ipeirotis},
isbn = {978-1-4503-5640-4/18/04},
keywords = {Document Object Model, DOM, Formal Semantics, Isabelle/HOL},
location = {Lyon, France},
pages = {741--749},
pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-core-dom-2018.pdf},
publisher= {ACM Press},
title = {A Formal Semantics of the Core {DOM} in {Isabelle/HOL}},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-core-dom-2018},
year = {2018},
}
chapter AFP
session "Core_SC_DOM" (AFP) = "HOL-Library" +
options [timeout = 1200]
directories
"common"
"common/classes"
"common/monads"
"common/pointers"
"common/preliminaries"
"common/tests"
"safely_composable"
"safely_composable/classes"
"safely_composable/pointers"
theories
Core_DOM
Core_DOM_Tests
document_files (in "document")
"root.tex"
"root.bib"
(***********************************************************************************
* Copyright (c) 2016-2018 The University of Sheffield, UK
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* * Redistributions of source code must retain the above copyright notice, this
* list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
* SPDX-License-Identifier: BSD-2-Clause
***********************************************************************************)
section\<open>The Core DOM\<close>
text\<open>This theory is the main entry point of our formalization of the core DOM.\<close>
theory Core_DOM
imports
"Core_DOM_Heap_WF"
begin
end
(***********************************************************************************
* Copyright (c) 2016-2018 The University of Sheffield, UK
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* * Redistributions of source code must retain the above copyright notice, this
* list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
* SPDX-License-Identifier: BSD-2-Clause
*******************************************************************************\***)
section\<open>Basic Data Types\<close>
text\<open>
\label{sec:Core_DOM_Basic_Datatypes}
This theory formalizes the primitive data types used by the DOM standard~\cite{dom-specification}.
\<close>
theory Core_DOM_Basic_Datatypes
imports
Main
begin
type_synonym USVString = string
text\<open>
In the official standard, the type @{type "USVString"} corresponds to the set of all possible
sequences of Unicode scalar values. As we are not interested in analyzing the specifics of Unicode
strings, we just model @{type "USVString"} using the standard type @{type "string"} of Isabelle/HOL.
\<close>
type_synonym DOMString = string
text\<open>
In the official standard, the type @{type "DOMString"} corresponds to the set of all possible
sequences of code units, commonly interpreted as UTF-16 encoded strings. Again, as we are not
interested in analyzing the specifics of Unicode strings, we just model @{type "DOMString"} using
the standard type @{type "string"} of Isabelle/HOL.
\<close>
type_synonym doctype = DOMString
paragraph\<open>Examples\<close>
definition html :: doctype
where "html = ''<!DOCTYPE html>''"
hide_const id
text \<open>This dummy locale is used to create scoped definitions by using global interpretations
and defines.\<close>
locale l_dummy
end
This source diff could not be displayed because it is too large. You can view the blob instead.
(***********************************************************************************
* Copyright (c) 2016-2018 The University of Sheffield, UK
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* * Redistributions of source code must retain the above copyright notice, this
* list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
* SPDX-License-Identifier: BSD-2-Clause
***********************************************************************************)
section\<open>Core DOM Test Cases\<close>
text\<open>This theory aggregates the individual test cases for the core DOM.\<close>
theory Core_DOM_Tests
imports
"tests/Document_adoptNode"
"tests/Document_getElementById"
"tests/Node_insertBefore"
"tests/Node_removeChild"
begin
end
(***********************************************************************************
* Copyright (c) 2016-2018 The University of Sheffield, UK
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* * Redistributions of source code must retain the above copyright notice, this
* list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
* SPDX-License-Identifier: BSD-2-Clause
***********************************************************************************)
section\<open>The Class Infrastructure\<close>
text\<open>In this theory, we introduce the basic infrastructure for our encoding
of classes.\<close>
theory BaseClass
imports
"HOL-Library.Finite_Map"
"../pointers/Ref"
"../Core_DOM_Basic_Datatypes"
begin
named_theorems instances
consts get :: 'a
consts put :: 'a
consts delete :: 'a
text \<open>Overall, the definition of the class types follows closely the one of the pointer
types. Instead of datatypes, we use records for our classes. This allows us to, first,
make use of record inheritance, which is, in addition to the type synonyms of
previous class types, the second place where the inheritance relationship of
our types manifest. Second, we get a convenient notation to define classes, in
addition to automatically generated getter and setter functions.\<close>
text \<open>Along with our class types, we also develop our heap type, which is a finite
map at its core. It is important to note that while the map stores a mapping
from @{term "object_ptr"} to @{term "Object"}, we restrict the type variables
of the record extension slot of @{term "Object"} in such a way that allows
down-casting, but requires a bit of taking-apart and re-assembling of our records
before they are stored in the heap.\<close>
text \<open>Throughout the theory files, we will use underscore case to reference pointer
types, and camel case for class types.\<close>
text \<open>Every class type contains at least one attribute; nothing. This is used for
two purposes: first, the record package does not allow records without any
attributes. Second, we will use the getter of nothing later to check whether a
class of the correct type could be retrieved, for which we will be able to use
our infrastructure regarding the behaviour of getters across different heaps.\<close>
locale l_type_wf = fixes type_wf :: "'heap \<Rightarrow> bool"
locale l_known_ptr = fixes known_ptr :: "'ptr \<Rightarrow> bool"
end
This diff is collapsed.
This diff is collapsed.
(***********************************************************************************
* Copyright (c) 2016-2018 The University of Sheffield, UK
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* * Redistributions of source code must retain the above copyright notice, this
* list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
* SPDX-License-Identifier: BSD-2-Clause
***********************************************************************************)
section\<open>Node\<close>
text\<open>In this theory, we introduce the types for the Node class.\<close>
theory NodeClass
imports
ObjectClass
"../pointers/NodePointer"
begin
subsubsection\<open>Node\<close>
record RNode = RObject
+ nothing :: unit
register_default_tvars "'Node RNode_ext"
type_synonym 'Node Node = "'Node RNode_scheme"
register_default_tvars "'Node Node"
type_synonym ('Object, 'Node) Object = "('Node RNode_ext + 'Object) Object"
register_default_tvars "('Object, 'Node) Object"
type_synonym ('object_ptr, 'node_ptr, 'Object, 'Node) heap
= "('node_ptr node_ptr + 'object_ptr, 'Node RNode_ext + 'Object) heap"
register_default_tvars
"('object_ptr, 'node_ptr, 'Object, 'Node) heap"
type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit, unit, unit) heap"
definition node_ptr_kinds :: "(_) heap \<Rightarrow> (_) node_ptr fset"
where
"node_ptr_kinds heap =
(the |`| (cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r |`| (ffilter is_node_ptr_kind (object_ptr_kinds heap))))"
lemma node_ptr_kinds_simp [simp]:
"node_ptr_kinds (Heap (fmupd (cast node_ptr) node (the_heap h)))
= {|node_ptr|} |\<union>| node_ptr_kinds h"
apply(auto simp add: node_ptr_kinds_def)[1]
by force
definition cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e :: "(_) Object \<Rightarrow> (_) Node option"
where
"cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e obj = (case RObject.more obj of Inl node
\<Rightarrow> Some (RObject.extend (RObject.truncate obj) node) | _ \<Rightarrow> None)"
adhoc_overloading cast cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e
definition cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t:: "(_) Node \<Rightarrow> (_) Object"
where
"cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t node = (RObject.extend (RObject.truncate node) (Inl (RObject.more node)))"
adhoc_overloading cast cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
definition is_node_kind :: "(_) Object \<Rightarrow> bool"
where
"is_node_kind ptr \<longleftrightarrow> cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e ptr \<noteq> None"
definition get\<^sub>N\<^sub>o\<^sub>d\<^sub>e :: "(_) node_ptr \<Rightarrow> (_) heap \<Rightarrow> (_) Node option"
where
"get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr h = Option.bind (get (cast node_ptr) h) cast"
adhoc_overloading get get\<^sub>N\<^sub>o\<^sub>d\<^sub>e
locale l_type_wf_def\<^sub>N\<^sub>o\<^sub>d\<^sub>e
begin
definition a_type_wf :: "(_) heap \<Rightarrow> bool"
where
"a_type_wf h = (ObjectClass.type_wf h
\<and> (\<forall>node_ptr \<in> fset( node_ptr_kinds h). get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr h \<noteq> None))"
end
global_interpretation l_type_wf_def\<^sub>N\<^sub>o\<^sub>d\<^sub>e defines type_wf = a_type_wf .
lemmas type_wf_defs = a_type_wf_def
locale l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e = l_type_wf type_wf for type_wf :: "((_) heap \<Rightarrow> bool)" +
assumes type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e: "type_wf h \<Longrightarrow> NodeClass.type_wf h"
sublocale l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e \<subseteq> l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
apply(unfold_locales)
using ObjectClass.a_type_wf_def by auto
locale l_get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_lemmas = l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e
begin
sublocale l_get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas by unfold_locales
lemma get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf:
assumes "type_wf h"
shows "node_ptr |\<in>| node_ptr_kinds h \<longleftrightarrow> get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr h \<noteq> None"
using l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e_axioms assms
apply(simp add: type_wf_defs get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)
by (metis bind_eq_None_conv ffmember_filter fimage_eqI fmember.rep_eq is_node_ptr_kind_cast
get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf node_ptr_casts_commute2 node_ptr_kinds_def option.sel option.simps(3))
end
global_interpretation l_get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_lemmas type_wf
by unfold_locales
definition put\<^sub>N\<^sub>o\<^sub>d\<^sub>e :: "(_) node_ptr \<Rightarrow> (_) Node \<Rightarrow> (_) heap \<Rightarrow> (_) heap"
where
"put\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr node = put (cast node_ptr) (cast node)"
adhoc_overloading put put\<^sub>N\<^sub>o\<^sub>d\<^sub>e
lemma put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_ptr_in_heap:
assumes "put\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr node h = h'"
shows "node_ptr |\<in>| node_ptr_kinds h'"
using assms
unfolding put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def node_ptr_kinds_def
by (metis ffmember_filter fimage_eqI is_node_ptr_kind_cast node_ptr_casts_commute2
option.sel put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ptr_in_heap)
lemma put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_put_ptrs:
assumes "put\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr node h = h'"
shows "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast node_ptr|}"
using assms
by (simp add: put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_put_ptrs)
lemma node_ptr_kinds_commutes [simp]:
"cast node_ptr |\<in>| object_ptr_kinds h \<longleftrightarrow> node_ptr |\<in>| node_ptr_kinds h"
apply(auto simp add: node_ptr_kinds_def split: option.splits)[1]
by (metis (no_types, lifting) ffmember_filter fimage_eqI fset.map_comp
is_node_ptr_kind_none node_ptr_casts_commute2
option.distinct(1) option.sel)
lemma node_empty [simp]:
"\<lparr>RObject.nothing = (), RNode.nothing = (), \<dots> = RNode.more node\<rparr> = node"
by simp
lemma cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_inject [simp]: "cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t x = cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t y \<longleftrightarrow> x = y"
apply(simp add: cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def RObject.extend_def)
by (metis (full_types) RObject.surjective old.unit.exhaust)
lemma cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none [simp]:
"cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e obj = None \<longleftrightarrow> \<not> (\<exists>node. cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t node = obj)"
apply(auto simp add: cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def RObject.extend_def split: sum.splits)[1]
by (metis (full_types) RObject.select_convs(2) RObject.surjective old.unit.exhaust)
lemma cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_some [simp]: "cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e obj = Some node \<longleftrightarrow> cast node = obj"
by(auto simp add: cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def RObject.extend_def split: sum.splits)
lemma cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv [simp]: "cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e (cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t node) = Some node"
by simp
locale l_known_ptr\<^sub>N\<^sub>o\<^sub>d\<^sub>e
begin
definition a_known_ptr :: "(_) object_ptr \<Rightarrow> bool"
where
"a_known_ptr ptr = False"
end
global_interpretation l_known_ptr\<^sub>N\<^sub>o\<^sub>d\<^sub>e defines known_ptr = a_known_ptr .
lemmas known_ptr_defs = a_known_ptr_def
locale l_known_ptrs\<^sub>N\<^sub>o\<^sub>d\<^sub>e = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr \<Rightarrow> bool"
begin
definition a_known_ptrs :: "(_) heap \<Rightarrow> bool"
where
"a_known_ptrs h = (\<forall>ptr \<in> fset (object_ptr_kinds h). known_ptr ptr)"
lemma known_ptrs_known_ptr: "a_known_ptrs h \<Longrightarrow> ptr |\<in>| object_ptr_kinds h \<Longrightarrow> known_ptr ptr"
apply(simp add: a_known_ptrs_def)
using notin_fset by fastforce
lemma known_ptrs_preserved:
"object_ptr_kinds h = object_ptr_kinds h' \<Longrightarrow> a_known_ptrs h = a_known_ptrs h'"
by(auto simp add: a_known_ptrs_def)
lemma known_ptrs_subset:
"object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD)
lemma known_ptrs_new_ptr:
"object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow>
a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
by(simp add: a_known_ptrs_def)
end
global_interpretation l_known_ptrs\<^sub>N\<^sub>o\<^sub>d\<^sub>e known_ptr defines known_ptrs = a_known_ptrs .
lemmas known_ptrs_defs = a_known_ptrs_def
lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset
known_ptrs_new_ptr
by blast
lemma get_node_ptr_simp1 [simp]: "get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr (put\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr node h) = Some node"
by(auto simp add: get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)
lemma get_node_ptr_simp2 [simp]:
"node_ptr \<noteq> node_ptr' \<Longrightarrow> get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr (put\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr' node h) = get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr h"
by(auto simp add: get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)
end
(***********************************************************************************
* Copyright (c) 2016-2018 The University of Sheffield, UK
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* * Redistributions of source code must retain the above copyright notice, this
* list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
* SPDX-License-Identifier: BSD-2-Clause
***********************************************************************************)
section\<open>Object\<close>
text\<open>In this theory, we introduce the definition of the class Object. This class is the
common superclass of our class model.\<close>
theory ObjectClass
imports
BaseClass
"../pointers/ObjectPointer"
begin
record RObject =
nothing :: unit
register_default_tvars "'Object RObject_ext"
type_synonym 'Object Object = "'Object RObject_scheme"
register_default_tvars "'Object Object"
datatype ('object_ptr, 'Object) heap = Heap (the_heap: "((_) object_ptr, (_) Object) fmap")
register_default_tvars "('object_ptr, 'Object) heap"
type_synonym heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l = "(unit, unit) heap"
definition object_ptr_kinds :: "(_) heap \<Rightarrow> (_) object_ptr fset"
where
"object_ptr_kinds = fmdom \<circ> the_heap"
lemma object_ptr_kinds_simp [simp]:
"object_ptr_kinds (Heap (fmupd object_ptr object (the_heap h)))
= {|object_ptr|} |\<union>| object_ptr_kinds h"
by(auto simp add: object_ptr_kinds_def)
definition get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t :: "(_) object_ptr \<Rightarrow> (_) heap \<Rightarrow> (_) Object option"
where
"get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr h = fmlookup (the_heap h) ptr"
adhoc_overloading get get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
locale l_type_wf_def\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
begin
definition a_type_wf :: "(_) heap \<Rightarrow> bool"
where
"a_type_wf h = True"
end
global_interpretation l_type_wf_def\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t defines type_wf = a_type_wf .
lemmas type_wf_defs = a_type_wf_def
locale l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t = l_type_wf type_wf for type_wf :: "((_) heap \<Rightarrow> bool)" +
assumes type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t: "type_wf h \<Longrightarrow> ObjectClass.type_wf h"
locale l_get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas = l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
begin
lemma get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf:
assumes "type_wf h"
shows "object_ptr |\<in>| object_ptr_kinds h \<longleftrightarrow> get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr h \<noteq> None"
using l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_axioms assms
apply(simp add: type_wf_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def)
by (simp add: fmlookup_dom_iff object_ptr_kinds_def)
end
global_interpretation l_get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas type_wf
by (simp add: l_get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_lemmas.intro l_type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t.intro)
definition put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t :: "(_) object_ptr \<Rightarrow> (_) Object \<Rightarrow> (_) heap \<Rightarrow> (_) heap"
where
"put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h = Heap (fmupd ptr obj (the_heap h))"