forked from afp-mirror/Core_DOM
Use prefixed document variable.
This commit is contained in:
Michael Herzberg
parent
ac0fa734e4
commit
2aa64dcace
|
|
@ -27,8 +27,10 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
***********************************************************************************)
|
||||
|
||||
section\<open>Testing adoptNode\<close>
|
||||
text\<open>This theory contains the test cases for adoptNode.\<close>
|
||||
(* This file is automatically generated, please do not modify! *)
|
||||
|
||||
section\<open>Testing Core_DOM\<close>
|
||||
text\<open>This theory contains the test cases for Core_DOM.\<close>
|
||||
|
||||
theory Document_adoptNode
|
||||
imports
|
||||
|
|
@ -52,30 +54,30 @@ definition Document_adoptNode_heap :: heap⇩f⇩i⇩n⇩a⇩l where
|
|||
(cast (element_ptr.Ref 11), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 3)] fmempty None)),
|
||||
(cast (character_data_ptr.Ref 3), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]"
|
||||
|
||||
definition document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "document = Some (cast (document_ptr.Ref 1))"
|
||||
definition Document_adoptNode_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "Document_adoptNode_document = Some (cast (document_ptr.Ref 1))"
|
||||
|
||||
|
||||
text \<open>"Adopting an Element called 'x<' should work."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
tmp0 \<leftarrow> document . getElementsByTagName(''x<'');
|
||||
tmp0 \<leftarrow> Document_adoptNode_document . getElementsByTagName(''x<'');
|
||||
y \<leftarrow> return (tmp0 ! 0);
|
||||
child \<leftarrow> y . firstChild;
|
||||
tmp1 \<leftarrow> y . parentNode;
|
||||
tmp2 \<leftarrow> document . body;
|
||||
tmp2 \<leftarrow> Document_adoptNode_document . body;
|
||||
assert_equals(tmp1, tmp2);
|
||||
tmp3 \<leftarrow> y . ownerDocument;
|
||||
assert_equals(tmp3, document);
|
||||
tmp4 \<leftarrow> document . adoptNode(y);
|
||||
assert_equals(tmp3, Document_adoptNode_document);
|
||||
tmp4 \<leftarrow> Document_adoptNode_document . adoptNode(y);
|
||||
assert_equals(tmp4, y);
|
||||
tmp5 \<leftarrow> y . parentNode;
|
||||
assert_equals(tmp5, None);
|
||||
tmp6 \<leftarrow> y . firstChild;
|
||||
assert_equals(tmp6, child);
|
||||
tmp7 \<leftarrow> y . ownerDocument;
|
||||
assert_equals(tmp7, document);
|
||||
assert_equals(tmp7, Document_adoptNode_document);
|
||||
tmp8 \<leftarrow> child . ownerDocument;
|
||||
assert_equals(tmp8, document);
|
||||
assert_equals(tmp8, Document_adoptNode_document);
|
||||
doc \<leftarrow> createDocument(None, None, None);
|
||||
tmp9 \<leftarrow> doc . adoptNode(y);
|
||||
assert_equals(tmp9, y);
|
||||
|
|
@ -94,8 +96,8 @@ lemma "test (do {
|
|||
text \<open>"Adopting an Element called ':good:times:' should work."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
x \<leftarrow> document . createElement('':good:times:'');
|
||||
tmp0 \<leftarrow> document . adoptNode(x);
|
||||
x \<leftarrow> Document_adoptNode_document . createElement('':good:times:'');
|
||||
tmp0 \<leftarrow> Document_adoptNode_document . adoptNode(x);
|
||||
assert_equals(tmp0, x);
|
||||
doc \<leftarrow> createDocument(None, None, None);
|
||||
tmp1 \<leftarrow> doc . adoptNode(x);
|
||||
|
|
|
|||
|
|
@ -27,8 +27,10 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
***********************************************************************************)
|
||||
|
||||
section\<open>Testing getElementById\<close>
|
||||
text\<open>This theory contains the test cases for getElementById.\<close>
|
||||
(* This file is automatically generated, please do not modify! *)
|
||||
|
||||
section\<open>Testing Core_DOM\<close>
|
||||
text\<open>This theory contains the test cases for Core_DOM.\<close>
|
||||
|
||||
theory Document_getElementById
|
||||
imports
|
||||
|
|
@ -60,23 +62,23 @@ definition Document_getElementById_heap :: heap⇩f⇩i⇩n⇩a⇩l where
|
|||
(cast (element_ptr.Ref 19), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 3)] fmempty None)),
|
||||
(cast (character_data_ptr.Ref 3), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]"
|
||||
|
||||
definition document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "document = Some (cast (document_ptr.Ref 1))"
|
||||
definition Document_getElementById_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "Document_getElementById_document = Some (cast (document_ptr.Ref 1))"
|
||||
|
||||
|
||||
text \<open>"Document.getElementById with a script-inserted element"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test2'';
|
||||
test \<leftarrow> document . createElement(''div'');
|
||||
test \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
test . setAttribute(''id'', TEST_ID);
|
||||
gBody . appendChild(test);
|
||||
result \<leftarrow> document . getElementById(TEST_ID);
|
||||
result \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_not_equals(result, None, ''should not be null.'');
|
||||
tmp0 \<leftarrow> result . tagName;
|
||||
assert_equals(tmp0, ''div'', ''should have appended element's tag name'');
|
||||
gBody . removeChild(test);
|
||||
removed \<leftarrow> document . getElementById(TEST_ID);
|
||||
removed \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(removed, None, ''should not get removed element.'')
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -85,19 +87,19 @@ lemma "test (do {
|
|||
text \<open>"update `id` attribute via setAttribute/removeAttribute"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test3'';
|
||||
test \<leftarrow> document . createElement(''div'');
|
||||
test \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
test . setAttribute(''id'', TEST_ID);
|
||||
gBody . appendChild(test);
|
||||
UPDATED_ID \<leftarrow> return ''test3-updated'';
|
||||
test . setAttribute(''id'', UPDATED_ID);
|
||||
e \<leftarrow> document . getElementById(UPDATED_ID);
|
||||
e \<leftarrow> Document_getElementById_document . getElementById(UPDATED_ID);
|
||||
assert_equals(e, test, ''should get the element with id.'');
|
||||
old \<leftarrow> document . getElementById(TEST_ID);
|
||||
old \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(old, None, ''shouldn't get the element by the old id.'');
|
||||
test . removeAttribute(''id'');
|
||||
e2 \<leftarrow> document . getElementById(UPDATED_ID);
|
||||
e2 \<leftarrow> Document_getElementById_document . getElementById(UPDATED_ID);
|
||||
assert_equals(e2, None, ''should return null when the passed id is none in document.'')
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -107,13 +109,13 @@ text \<open>"Ensure that the id attribute only affects elements present in a doc
|
|||
|
||||
lemma "test (do {
|
||||
TEST_ID \<leftarrow> return ''test4-should-not-exist'';
|
||||
e \<leftarrow> document . createElement(''div'');
|
||||
e \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
e . setAttribute(''id'', TEST_ID);
|
||||
tmp0 \<leftarrow> document . getElementById(TEST_ID);
|
||||
tmp0 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(tmp0, None, ''should be null'');
|
||||
tmp1 \<leftarrow> document . body;
|
||||
tmp1 \<leftarrow> Document_getElementById_document . body;
|
||||
tmp1 . appendChild(e);
|
||||
tmp2 \<leftarrow> document . getElementById(TEST_ID);
|
||||
tmp2 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(tmp2, e, ''should be the appended element'')
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -122,23 +124,23 @@ lemma "test (do {
|
|||
text \<open>"in tree order, within the context object's tree"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test5'';
|
||||
target \<leftarrow> document . getElementById(TEST_ID);
|
||||
target \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_not_equals(target, None, ''should not be null'');
|
||||
tmp0 \<leftarrow> target . getAttribute(''data-name'');
|
||||
assert_equals(tmp0, ''1st'', ''should return the 1st'');
|
||||
element4 \<leftarrow> document . createElement(''div'');
|
||||
element4 \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
element4 . setAttribute(''id'', TEST_ID);
|
||||
element4 . setAttribute(''data-name'', ''4th'');
|
||||
gBody . appendChild(element4);
|
||||
target2 \<leftarrow> document . getElementById(TEST_ID);
|
||||
target2 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_not_equals(target2, None, ''should not be null'');
|
||||
tmp1 \<leftarrow> target2 . getAttribute(''data-name'');
|
||||
assert_equals(tmp1, ''1st'', ''should be the 1st'');
|
||||
tmp2 \<leftarrow> target2 . parentNode;
|
||||
tmp2 . removeChild(target2);
|
||||
target3 \<leftarrow> document . getElementById(TEST_ID);
|
||||
target3 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_not_equals(target3, None, ''should not be null'');
|
||||
tmp3 \<leftarrow> target3 . getAttribute(''data-name'');
|
||||
assert_equals(tmp3, ''4th'', ''should be the 4th'')
|
||||
|
|
@ -146,17 +148,15 @@ lemma "test (do {
|
|||
by eval
|
||||
|
||||
|
||||
text \<open>"Modern browsers optimize this method with using internal id cache.
|
||||
This test checks that their optimization should effect only append to
|
||||
`Document`, not append to `Node`."\<close>
|
||||
text \<open>"Modern browsers optimize this method with using internal id cache. This test checks that their optimization should effect only append to `Document`, not append to `Node`."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
TEST_ID \<leftarrow> return ''test6'';
|
||||
s \<leftarrow> document . createElement(''div'');
|
||||
s \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
s . setAttribute(''id'', TEST_ID);
|
||||
tmp0 \<leftarrow> document . createElement(''div'');
|
||||
tmp0 \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
tmp0 . appendChild(s);
|
||||
tmp1 \<leftarrow> document . getElementById(TEST_ID);
|
||||
tmp1 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(tmp1, None, ''should be null'')
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -165,17 +165,17 @@ lemma "test (do {
|
|||
text \<open>"changing attribute's value via `Attr` gotten from `Element.attribute`."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test7'';
|
||||
element \<leftarrow> document . createElement(''div'');
|
||||
element \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
element . setAttribute(''id'', TEST_ID);
|
||||
gBody . appendChild(element);
|
||||
target \<leftarrow> document . getElementById(TEST_ID);
|
||||
target \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(target, element, ''should return the element before changing the value'');
|
||||
element . setAttribute(''id'', (TEST_ID @ ''-updated''));
|
||||
target2 \<leftarrow> document . getElementById(TEST_ID);
|
||||
target2 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(target2, None, ''should return null after updated id via Attr.value'');
|
||||
target3 \<leftarrow> document . getElementById((TEST_ID @ ''-updated''));
|
||||
target3 \<leftarrow> Document_getElementById_document . getElementById((TEST_ID @ ''-updated''));
|
||||
assert_equals(target3, element, ''should be equal to the updated element.'')
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -184,19 +184,19 @@ lemma "test (do {
|
|||
text \<open>"update `id` attribute via element.id"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test12'';
|
||||
test \<leftarrow> document . createElement(''div'');
|
||||
test \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
test . setAttribute(''id'', TEST_ID);
|
||||
gBody . appendChild(test);
|
||||
UPDATED_ID \<leftarrow> return (TEST_ID @ ''-updated'');
|
||||
test . setAttribute(''id'', UPDATED_ID);
|
||||
e \<leftarrow> document . getElementById(UPDATED_ID);
|
||||
e \<leftarrow> Document_getElementById_document . getElementById(UPDATED_ID);
|
||||
assert_equals(e, test, ''should get the element with id.'');
|
||||
old \<leftarrow> document . getElementById(TEST_ID);
|
||||
old \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(old, None, ''shouldn't get the element by the old id.'');
|
||||
test . setAttribute(''id'', '''');
|
||||
e2 \<leftarrow> document . getElementById(UPDATED_ID);
|
||||
e2 \<leftarrow> Document_getElementById_document . getElementById(UPDATED_ID);
|
||||
assert_equals(e2, None, ''should return null when the passed id is none in document.'')
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -205,33 +205,33 @@ lemma "test (do {
|
|||
text \<open>"where insertion order and tree order don't match"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test13'';
|
||||
container \<leftarrow> document . createElement(''div'');
|
||||
container \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
container . setAttribute(''id'', (TEST_ID @ ''-fixture''));
|
||||
gBody . appendChild(container);
|
||||
element1 \<leftarrow> document . createElement(''div'');
|
||||
element1 \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
element1 . setAttribute(''id'', TEST_ID);
|
||||
element2 \<leftarrow> document . createElement(''div'');
|
||||
element2 \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
element2 . setAttribute(''id'', TEST_ID);
|
||||
element3 \<leftarrow> document . createElement(''div'');
|
||||
element3 \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
element3 . setAttribute(''id'', TEST_ID);
|
||||
element4 \<leftarrow> document . createElement(''div'');
|
||||
element4 \<leftarrow> Document_getElementById_document . createElement(''div'');
|
||||
element4 . setAttribute(''id'', TEST_ID);
|
||||
container . appendChild(element2);
|
||||
container . appendChild(element4);
|
||||
container . insertBefore(element3, element4);
|
||||
container . insertBefore(element1, element2);
|
||||
test \<leftarrow> document . getElementById(TEST_ID);
|
||||
test \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(test, element1, ''should return 1st element'');
|
||||
container . removeChild(element1);
|
||||
test \<leftarrow> document . getElementById(TEST_ID);
|
||||
test \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(test, element2, ''should return 2nd element'');
|
||||
container . removeChild(element2);
|
||||
test \<leftarrow> document . getElementById(TEST_ID);
|
||||
test \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(test, element3, ''should return 3rd element'');
|
||||
container . removeChild(element3);
|
||||
test \<leftarrow> document . getElementById(TEST_ID);
|
||||
test \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(test, element4, ''should return 4th element'');
|
||||
container . removeChild(element4)
|
||||
}) Document_getElementById_heap"
|
||||
|
|
@ -241,16 +241,16 @@ lemma "test (do {
|
|||
text \<open>"Inserting an id by inserting its parent node"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
gBody \<leftarrow> document . body;
|
||||
gBody \<leftarrow> Document_getElementById_document . body;
|
||||
TEST_ID \<leftarrow> return ''test14'';
|
||||
a \<leftarrow> document . createElement(''a'');
|
||||
b \<leftarrow> document . createElement(''b'');
|
||||
a \<leftarrow> Document_getElementById_document . createElement(''a'');
|
||||
b \<leftarrow> Document_getElementById_document . createElement(''b'');
|
||||
a . appendChild(b);
|
||||
b . setAttribute(''id'', TEST_ID);
|
||||
tmp0 \<leftarrow> document . getElementById(TEST_ID);
|
||||
tmp0 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(tmp0, None);
|
||||
gBody . appendChild(a);
|
||||
tmp1 \<leftarrow> document . getElementById(TEST_ID);
|
||||
tmp1 \<leftarrow> Document_getElementById_document . getElementById(TEST_ID);
|
||||
assert_equals(tmp1, b)
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
@ -260,15 +260,15 @@ text \<open>"Document.getElementById must not return nodes not present in docume
|
|||
|
||||
lemma "test (do {
|
||||
TEST_ID \<leftarrow> return ''test15'';
|
||||
outer \<leftarrow> document . getElementById(''outer'');
|
||||
middle \<leftarrow> document . getElementById(''middle'');
|
||||
inner \<leftarrow> document . getElementById(''inner'');
|
||||
tmp0 \<leftarrow> document . getElementById(''middle'');
|
||||
outer \<leftarrow> Document_getElementById_document . getElementById(''outer'');
|
||||
middle \<leftarrow> Document_getElementById_document . getElementById(''middle'');
|
||||
inner \<leftarrow> Document_getElementById_document . getElementById(''inner'');
|
||||
tmp0 \<leftarrow> Document_getElementById_document . getElementById(''middle'');
|
||||
outer . removeChild(tmp0);
|
||||
new_el \<leftarrow> document . createElement(''h1'');
|
||||
new_el \<leftarrow> Document_getElementById_document . createElement(''h1'');
|
||||
new_el . setAttribute(''id'', ''heading'');
|
||||
inner . appendChild(new_el);
|
||||
tmp1 \<leftarrow> document . getElementById(''heading'');
|
||||
tmp1 \<leftarrow> Document_getElementById_document . getElementById(''heading'');
|
||||
assert_equals(tmp1, None)
|
||||
}) Document_getElementById_heap"
|
||||
by eval
|
||||
|
|
|
|||
|
|
@ -27,8 +27,10 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
***********************************************************************************)
|
||||
|
||||
section\<open>Testing insertBefore\<close>
|
||||
text\<open>This theory contains the test cases for insertBefore.\<close>
|
||||
(* This file is automatically generated, please do not modify! *)
|
||||
|
||||
section\<open>Testing Core_DOM\<close>
|
||||
text\<open>This theory contains the test cases for Core_DOM.\<close>
|
||||
|
||||
theory Node_insertBefore
|
||||
imports
|
||||
|
|
@ -48,14 +50,14 @@ definition Node_insertBefore_heap :: heap⇩f⇩i⇩n⇩a⇩l where
|
|||
(cast (element_ptr.Ref 8), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 2)] fmempty None)),
|
||||
(cast (character_data_ptr.Ref 2), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]"
|
||||
|
||||
definition document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "document = Some (cast (document_ptr.Ref 1))"
|
||||
definition Node_insertBefore_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "Node_insertBefore_document = Some (cast (document_ptr.Ref 1))"
|
||||
|
||||
|
||||
text \<open>"Calling insertBefore an a leaf node Text must throw HIERARCHY\_REQUEST\_ERR."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
node \<leftarrow> document . createTextNode(''Foo'');
|
||||
tmp0 \<leftarrow> document . createTextNode(''fail'');
|
||||
node \<leftarrow> Node_insertBefore_document . createTextNode(''Foo'');
|
||||
tmp0 \<leftarrow> Node_insertBefore_document . createTextNode(''fail'');
|
||||
assert_throws(HierarchyRequestError, node . insertBefore(tmp0, None))
|
||||
}) Node_insertBefore_heap"
|
||||
by eval
|
||||
|
|
@ -64,13 +66,13 @@ lemma "test (do {
|
|||
text \<open>"Calling insertBefore with an inclusive ancestor of the context object must throw HIERARCHY\_REQUEST\_ERR."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
tmp1 \<leftarrow> document . body;
|
||||
tmp2 \<leftarrow> document . getElementById(''log'');
|
||||
tmp0 \<leftarrow> document . body;
|
||||
tmp1 \<leftarrow> Node_insertBefore_document . body;
|
||||
tmp2 \<leftarrow> Node_insertBefore_document . getElementById(''log'');
|
||||
tmp0 \<leftarrow> Node_insertBefore_document . body;
|
||||
assert_throws(HierarchyRequestError, tmp0 . insertBefore(tmp1, tmp2));
|
||||
tmp4 \<leftarrow> document . documentElement;
|
||||
tmp5 \<leftarrow> document . getElementById(''log'');
|
||||
tmp3 \<leftarrow> document . body;
|
||||
tmp4 \<leftarrow> Node_insertBefore_document . documentElement;
|
||||
tmp5 \<leftarrow> Node_insertBefore_document . getElementById(''log'');
|
||||
tmp3 \<leftarrow> Node_insertBefore_document . body;
|
||||
assert_throws(HierarchyRequestError, tmp3 . insertBefore(tmp4, tmp5))
|
||||
}) Node_insertBefore_heap"
|
||||
by eval
|
||||
|
|
@ -79,9 +81,9 @@ lemma "test (do {
|
|||
text \<open>"Calling insertBefore with a reference child whose parent is not the context node must throw a NotFoundError."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
a \<leftarrow> document . createElement(''div'');
|
||||
b \<leftarrow> document . createElement(''div'');
|
||||
c \<leftarrow> document . createElement(''div'');
|
||||
a \<leftarrow> Node_insertBefore_document . createElement(''div'');
|
||||
b \<leftarrow> Node_insertBefore_document . createElement(''div'');
|
||||
c \<leftarrow> Node_insertBefore_document . createElement(''div'');
|
||||
assert_throws(NotFoundError, a . insertBefore(b, c))
|
||||
}) Node_insertBefore_heap"
|
||||
by eval
|
||||
|
|
@ -104,9 +106,9 @@ lemma "test (do {
|
|||
text \<open>"Inserting a node before itself should not move the node"\<close>
|
||||
|
||||
lemma "test (do {
|
||||
a \<leftarrow> document . createElement(''div'');
|
||||
b \<leftarrow> document . createElement(''div'');
|
||||
c \<leftarrow> document . createElement(''div'');
|
||||
a \<leftarrow> Node_insertBefore_document . createElement(''div'');
|
||||
b \<leftarrow> Node_insertBefore_document . createElement(''div'');
|
||||
c \<leftarrow> Node_insertBefore_document . createElement(''div'');
|
||||
a . appendChild(b);
|
||||
a . appendChild(c);
|
||||
tmp0 \<leftarrow> a . childNodes;
|
||||
|
|
|
|||
|
|
@ -27,8 +27,10 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
***********************************************************************************)
|
||||
|
||||
section\<open>Testing removeChild\<close>
|
||||
text\<open>This theory contains the test cases for removeChild.\<close>
|
||||
(* This file is automatically generated, please do not modify! *)
|
||||
|
||||
section\<open>Testing Core_DOM\<close>
|
||||
text\<open>This theory contains the test cases for Core_DOM.\<close>
|
||||
|
||||
theory Node_removeChild
|
||||
imports
|
||||
|
|
@ -50,17 +52,17 @@ definition Node_removeChild_heap :: heap⇩f⇩i⇩n⇩a⇩l where
|
|||
(cast (element_ptr.Ref 10), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 2)] fmempty None)),
|
||||
(cast (character_data_ptr.Ref 2), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]"
|
||||
|
||||
definition document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "document = Some (cast (document_ptr.Ref 1))"
|
||||
definition Node_removeChild_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "Node_removeChild_document = Some (cast (document_ptr.Ref 1))"
|
||||
|
||||
|
||||
text \<open>"Passing a detached Element to removeChild should not affect it."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
doc \<leftarrow> return document;
|
||||
doc \<leftarrow> return Node_removeChild_document;
|
||||
s \<leftarrow> doc . createElement(''div'');
|
||||
tmp0 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp0, doc);
|
||||
tmp1 \<leftarrow> document . body;
|
||||
tmp1 \<leftarrow> Node_removeChild_document . body;
|
||||
assert_throws(NotFoundError, tmp1 . removeChild(s));
|
||||
tmp2 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp2, doc)
|
||||
|
|
@ -71,13 +73,13 @@ lemma "test (do {
|
|||
text \<open>"Passing a non-detached Element to removeChild should not affect it."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
doc \<leftarrow> return document;
|
||||
doc \<leftarrow> return Node_removeChild_document;
|
||||
s \<leftarrow> doc . createElement(''div'');
|
||||
tmp0 \<leftarrow> doc . documentElement;
|
||||
tmp0 . appendChild(s);
|
||||
tmp1 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp1, doc);
|
||||
tmp2 \<leftarrow> document . body;
|
||||
tmp2 \<leftarrow> Node_removeChild_document . body;
|
||||
assert_throws(NotFoundError, tmp2 . removeChild(s));
|
||||
tmp3 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp3, doc)
|
||||
|
|
@ -88,7 +90,7 @@ lemma "test (do {
|
|||
text \<open>"Calling removeChild on an Element with no children should throw NOT\_FOUND\_ERR."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
doc \<leftarrow> return document;
|
||||
doc \<leftarrow> return Node_removeChild_document;
|
||||
s \<leftarrow> doc . createElement(''div'');
|
||||
tmp0 \<leftarrow> doc . body;
|
||||
tmp0 . appendChild(s);
|
||||
|
|
@ -106,7 +108,7 @@ lemma "test (do {
|
|||
s \<leftarrow> doc . createElement(''div'');
|
||||
tmp0 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp0, doc);
|
||||
tmp1 \<leftarrow> document . body;
|
||||
tmp1 \<leftarrow> Node_removeChild_document . body;
|
||||
assert_throws(NotFoundError, tmp1 . removeChild(s));
|
||||
tmp2 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp2, doc)
|
||||
|
|
@ -123,7 +125,7 @@ lemma "test (do {
|
|||
tmp0 . appendChild(s);
|
||||
tmp1 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp1, doc);
|
||||
tmp2 \<leftarrow> document . body;
|
||||
tmp2 \<leftarrow> Node_removeChild_document . body;
|
||||
assert_throws(NotFoundError, tmp2 . removeChild(s));
|
||||
tmp3 \<leftarrow> s . ownerDocument;
|
||||
assert_equals(tmp3, doc)
|
||||
|
|
@ -148,7 +150,7 @@ lemma "test (do {
|
|||
text \<open>"Passing a value that is not a Node reference to removeChild should throw TypeError."\<close>
|
||||
|
||||
lemma "test (do {
|
||||
tmp0 \<leftarrow> document . body;
|
||||
tmp0 \<leftarrow> Node_removeChild_document . body;
|
||||
assert_throws(TypeError, tmp0 . removeChild(None))
|
||||
}) Node_removeChild_heap"
|
||||
by eval
|
||||
|
|
|
|||
Reference in New Issue