afp-mirror
/
Shadow_SC_DOM
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
Shadow_SC_DOM/Shadow_SC_DOM/tests/slots.thy

948 lines
46 KiB
Plaintext
Raw Permalink Blame History

(***********************************************************************************
* Copyright (c) 2016-2020 The University of Sheffield, UK
* 2019-2020 University of Exeter, 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
***********************************************************************************)
(* This file is automatically generated, please do not modify! *)
section\<open>Testing slots\<close>
text\<open>This theory contains the test cases for slots.\<close>
theory slots
imports
"Shadow_DOM_BaseTest"
begin
definition slots_heap :: "heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l" where
"slots_heap = create_heap [(cast (document_ptr.Ref 1), cast (create_document_obj html (Some (cast (element_ptr.Ref 1))) [])),
(cast (element_ptr.Ref 1), cast (create_element_obj ''html'' [cast (element_ptr.Ref 2), cast (element_ptr.Ref 8)] fmempty None)),
(cast (element_ptr.Ref 2), cast (create_element_obj ''head'' [cast (element_ptr.Ref 3), cast (element_ptr.Ref 4), cast (element_ptr.Ref 5), cast (element_ptr.Ref 6), cast (element_ptr.Ref 7)] fmempty None)),
(cast (element_ptr.Ref 3), cast (create_element_obj ''title'' [cast (character_data_ptr.Ref 1)] fmempty None)),
(cast (character_data_ptr.Ref 1), cast (create_character_data_obj ''Shadow%20DOM%3A%20Slots%20and%20assignments'')),
(cast (element_ptr.Ref 4), cast (create_element_obj ''meta'' [] (fmap_of_list [(''name'', ''author''), (''title'', ''Hayato Ito''), (''href'', ''mailto:hayato@google.com'')]) None)),
(cast (element_ptr.Ref 5), cast (create_element_obj ''script'' [] (fmap_of_list [(''src'', ''/resources/testharness.js'')]) None)),
(cast (element_ptr.Ref 6), cast (create_element_obj ''script'' [] (fmap_of_list [(''src'', ''/resources/testharnessreport.js'')]) None)),
(cast (element_ptr.Ref 7), cast (create_element_obj ''script'' [] (fmap_of_list [(''src'', ''resources/shadow-dom.js'')]) None)),
(cast (element_ptr.Ref 8), cast (create_element_obj ''body'' [cast (element_ptr.Ref 9), cast (element_ptr.Ref 13), cast (element_ptr.Ref 14), cast (element_ptr.Ref 18), cast (element_ptr.Ref 19), cast (element_ptr.Ref 21), cast (element_ptr.Ref 22), cast (element_ptr.Ref 30), cast (element_ptr.Ref 31), cast (element_ptr.Ref 39), cast (element_ptr.Ref 40), cast (element_ptr.Ref 48), cast (element_ptr.Ref 49), cast (element_ptr.Ref 57), cast (element_ptr.Ref 58), cast (element_ptr.Ref 64), cast (element_ptr.Ref 65), cast (element_ptr.Ref 71), cast (element_ptr.Ref 72), cast (element_ptr.Ref 78), cast (element_ptr.Ref 79), cast (element_ptr.Ref 85), cast (element_ptr.Ref 86), cast (element_ptr.Ref 92), cast (element_ptr.Ref 93), cast (element_ptr.Ref 112)] fmempty None)),
(cast (element_ptr.Ref 9), cast (create_element_obj ''div'' [cast (element_ptr.Ref 10)] (fmap_of_list [(''id'', ''test_basic'')]) None)),
(cast (element_ptr.Ref 10), cast (create_element_obj ''div'' [cast (element_ptr.Ref 11)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 1))))),
(cast (element_ptr.Ref 11), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
(cast (shadow_root_ptr.Ref 1), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 12)])),
(cast (element_ptr.Ref 12), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
(cast (element_ptr.Ref 13), 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'')),
(cast (element_ptr.Ref 14), cast (create_element_obj ''div'' [cast (element_ptr.Ref 15)] (fmap_of_list [(''id'', ''test_basic_closed'')]) None)),
(cast (element_ptr.Ref 15), cast (create_element_obj ''div'' [cast (element_ptr.Ref 16)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 2))))),
(cast (element_ptr.Ref 16), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
(cast (shadow_root_ptr.Ref 2), cast (create_shadow_root_obj Closed [cast (element_ptr.Ref 17)])),
(cast (element_ptr.Ref 17), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
(cast (element_ptr.Ref 18), 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'')),
(cast (element_ptr.Ref 19), cast (create_element_obj ''div'' [cast (element_ptr.Ref 20)] (fmap_of_list [(''id'', ''test_slot_not_in_shadow'')]) None)),
(cast (element_ptr.Ref 20), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1'')]) None)),
(cast (element_ptr.Ref 21), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 4)] fmempty None)),
(cast (character_data_ptr.Ref 4), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
(cast (element_ptr.Ref 22), cast (create_element_obj ''div'' [cast (element_ptr.Ref 23), cast (element_ptr.Ref 25)] (fmap_of_list [(''id'', ''test_slot_not_in_shadow_2'')]) None)),
(cast (element_ptr.Ref 23), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 24)] (fmap_of_list [(''id'', ''s1'')]) None)),
(cast (element_ptr.Ref 24), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1'')]) None)),
(cast (element_ptr.Ref 25), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 26), cast (element_ptr.Ref 27)] (fmap_of_list [(''id'', ''s2'')]) None)),
(cast (element_ptr.Ref 26), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c2'')]) None)),
(cast (element_ptr.Ref 27), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 28), cast (element_ptr.Ref 29)] (fmap_of_list [(''id'', ''s3'')]) None)),
(cast (element_ptr.Ref 28), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c3_1'')]) None)),
(cast (element_ptr.Ref 29), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c3_2'')]) None)),
(cast (element_ptr.Ref 30), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 5)] fmempty None)),
(cast (character_data_ptr.Ref 5), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
(cast (element_ptr.Ref 31), cast (create_element_obj ''div'' [cast (element_ptr.Ref 32)] (fmap_of_list [(''id'', ''test_slot_name_matching'')]) None)),
(cast (element_ptr.Ref 32), cast (create_element_obj ''div'' [cast (element_ptr.Ref 33), cast (element_ptr.Ref 34), cast (element_ptr.Ref 35)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 3))))),
(cast (element_ptr.Ref 33), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
(cast (element_ptr.Ref 34), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c2''), (''slot'', ''slot2'')]) None)),
(cast (element_ptr.Ref 35), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c3''), (''slot'', ''yyy'')]) None)),
(cast (shadow_root_ptr.Ref 3), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 36), cast (element_ptr.Ref 37), cast (element_ptr.Ref 38)])),
(cast (element_ptr.Ref 36), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
(cast (element_ptr.Ref 37), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
(cast (element_ptr.Ref 38), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s3''), (''name'', ''xxx'')]) None)),
(cast (element_ptr.Ref 39), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 6)] fmempty None)),
(cast (character_data_ptr.Ref 6), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
(cast (element_ptr.Ref 40), cast (create_element_obj ''div'' [cast (element_ptr.Ref 41)] (fmap_of_list [(''id'', ''test_no_direct_host_child'')]) None)),
(cast (element_ptr.Ref 41), cast (create_element_obj ''div'' [cast (element_ptr.Ref 42), cast (element_ptr.Ref 43), cast (element_ptr.Ref 44)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 4))))),
(cast (element_ptr.Ref 42), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
(cast (element_ptr.Ref 43), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c2''), (''slot'', ''slot1'')]) None)),
(cast (element_ptr.Ref 44), cast (create_element_obj ''div'' [cast (element_ptr.Ref 45)] fmempty None)),
(cast (element_ptr.Ref 45), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c3''), (''slot'', ''slot1'')]) None)),
(cast (shadow_root_ptr.Ref 4), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 46), cast (element_ptr.Ref 47)])),
(cast (element_ptr.Ref 46), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
(cast (element_ptr.Ref 47), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot1'')]) None)),
(cast (element_ptr.Ref 48), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 7)] fmempty None)),
(cast (character_data_ptr.Ref 7), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
(cast (element_ptr.Ref 49), cast (create_element_obj ''div'' [cast (element_ptr.Ref 50)] (fmap_of_list [(''id'', ''test_default_slot'')]) None)),
(cast (element_ptr.Ref 50), cast (create_element_obj ''div'' [cast (element_ptr.Ref 51), cast (element_ptr.Ref 52), cast (element_ptr.Ref 53)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 5))))),
(cast (element_ptr.Ref 51), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1'')]) None)),
(cast (element_ptr.Ref 52), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c2''), (''slot'', '''')]) None)),
(cast (element_ptr.Ref 53), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c3''), (''slot'', ''foo'')]) None)),
(cast (shadow_root_ptr.Ref 5), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 54), cast (element_ptr.Ref 55), cast (element_ptr.Ref 56)])),
(cast (element_ptr.Ref 54), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
(cast (element_ptr.Ref 55), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2'')]) None)),
(cast (element_ptr.Ref 56), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s3'')]) None)),
(cast (element_ptr.Ref 57), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 8)] fmempty None)),
(cast (character_data_ptr.Ref 8), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
(cast (element_ptr.Ref 58), cast (create_element_obj ''div'' [cast (element_ptr.Ref 59)] (fmap_of_list [(''id'', ''test_slot_in_slot'')]) None)),
(cast (element_ptr.Ref 59), cast (create_element_obj ''div'' [cast (element_ptr.Ref 60), cast (element_ptr.Ref 61)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 6))))),
(cast (element_ptr.Ref 60), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot2'')]) None)),
(cast (element_ptr.Ref 61), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c2''), (''slot'', ''slot1'')]) None)),
(cast (shadow_root_ptr.Ref 6), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 62)])),
(cast (element_ptr.Ref 62), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 63)] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
(cast (element_ptr.Ref 63), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
(cast (element_ptr.Ref 64), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 9)] fmempty None)),
(cast (character_data_ptr.Ref 9), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
(cast (element_ptr.Ref 65), cast (create_element_obj ''div'' [cast (element_ptr.Ref 66)] (fmap_of_list [(''id'', ''test_slot_is_assigned_to_slot'')]) None)),
(cast (element_ptr.Ref 66), cast (create_element_obj ''div'' [cast (element_ptr.Ref 67)] (fmap_of_list [(''id'', ''host1'')]) (Some (cast (shadow_root_ptr.Ref 7))))),
(cast (element_ptr.Ref 67), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
(cast (shadow_root_ptr.Ref 7), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 68)])),
(cast (element_ptr.Ref 68), cast (create_element_obj ''div'' [cast (element_ptr.Ref 69)] (fmap_of_list [(''id'', ''host2'')]) (Some (cast (shadow_root_ptr.Ref 8))))),
(cast (element_ptr.Ref 69), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1''), (''slot'', ''slot2'')]) None)),
(cast (shadow_root_ptr.Ref 8), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 70)])),
(cast (element_ptr.Ref 70), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
(cast (element_ptr.Ref 71), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 10)] fmempty None)),
(cast (character_data_ptr.Ref 10), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
(cast (element_ptr.Ref 72), cast (create_element_obj ''div'' [cast (element_ptr.Ref 73)] (fmap_of_list [(''id'', ''test_open_closed'')]) None)),
(cast (element_ptr.Ref 73), cast (create_element_obj ''div'' [cast (element_ptr.Ref 74)] (fmap_of_list [(''id'', ''host1'')]) (Some (cast (shadow_root_ptr.Ref 9))))),
(cast (element_ptr.Ref 74), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
(cast (shadow_root_ptr.Ref 9), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 75)])),
(cast (element_ptr.Ref 75), cast (create_element_obj ''div'' [cast (element_ptr.Ref 76)] (fmap_of_list [(''id'', ''host2'')]) (Some (cast (shadow_root_ptr.Ref 10))))),
(cast (element_ptr.Ref 76), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1''), (''slot'', ''slot2'')]) None)),
(cast (shadow_root_ptr.Ref 10), cast (create_shadow_root_obj Closed [cast (element_ptr.Ref 77)])),
(cast (element_ptr.Ref 77), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
(cast (element_ptr.Ref 78), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 11)] fmempty None)),
(cast (character_data_ptr.Ref 11), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
(cast (element_ptr.Ref 79), cast (create_element_obj ''div'' [cast (element_ptr.Ref 80)] (fmap_of_list [(''id'', ''test_closed_closed'')]) None)),
(cast (element_ptr.Ref 80), cast (create_element_obj ''div'' [cast (element_ptr.Ref 81)] (fmap_of_list [(''id'', ''host1'')]) (Some (cast (shadow_root_ptr.Ref 11))))),
(cast (element_ptr.Ref 81), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
(cast (shadow_root_ptr.Ref 11), cast (create_shadow_root_obj Closed [cast (element_ptr.Ref 82)])),
(cast (element_ptr.Ref 82), cast (create_element_obj ''div'' [cast (element_ptr.Ref 83)] (fmap_of_list [(''id'', ''host2'')]) (Some (cast (shadow_root_ptr.Ref 12))))),
(cast (element_ptr.Ref 83), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1''), (''slot'', ''slot2'')]) None)),
(cast (shadow_root_ptr.Ref 12), cast (create_shadow_root_obj Closed [cast (element_ptr.Ref 84)])),
(cast (element_ptr.Ref 84), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
(cast (element_ptr.Ref 85), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 12)] fmempty None)),
(cast (character_data_ptr.Ref 12), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
(cast (element_ptr.Ref 86), cast (create_element_obj ''div'' [cast (element_ptr.Ref 87)] (fmap_of_list [(''id'', ''test_closed_open'')]) None)),
(cast (element_ptr.Ref 87), cast (create_element_obj ''div'' [cast (element_ptr.Ref 88)] (fmap_of_list [(''id'', ''host1'')]) (Some (cast (shadow_root_ptr.Ref 13))))),
(cast (element_ptr.Ref 88), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
(cast (shadow_root_ptr.Ref 13), cast (create_shadow_root_obj Closed [cast (element_ptr.Ref 89)])),
(cast (element_ptr.Ref 89), cast (create_element_obj ''div'' [cast (element_ptr.Ref 90)] (fmap_of_list [(''id'', ''host2'')]) (Some (cast (shadow_root_ptr.Ref 14))))),
(cast (element_ptr.Ref 90), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1''), (''slot'', ''slot2'')]) None)),
(cast (shadow_root_ptr.Ref 14), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 91)])),
(cast (element_ptr.Ref 91), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
(cast (element_ptr.Ref 92), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 13)] fmempty None)),
(cast (character_data_ptr.Ref 13), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
(cast (element_ptr.Ref 93), cast (create_element_obj ''div'' [cast (element_ptr.Ref 94)] (fmap_of_list [(''id'', ''test_complex'')]) None)),
(cast (element_ptr.Ref 94), cast (create_element_obj ''div'' [cast (element_ptr.Ref 95), cast (element_ptr.Ref 96), cast (element_ptr.Ref 97), cast (element_ptr.Ref 98)] (fmap_of_list [(''id'', ''host1'')]) (Some (cast (shadow_root_ptr.Ref 15))))),
(cast (element_ptr.Ref 95), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
(cast (element_ptr.Ref 96), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c2''), (''slot'', ''slot2'')]) None)),
(cast (element_ptr.Ref 97), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c3'')]) None)),
(cast (element_ptr.Ref 98), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c4''), (''slot'', ''slot-none'')]) None)),
(cast (shadow_root_ptr.Ref 15), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 99)])),
(cast (element_ptr.Ref 99), cast (create_element_obj ''div'' [cast (element_ptr.Ref 100), cast (element_ptr.Ref 101), cast (element_ptr.Ref 102), cast (element_ptr.Ref 103), cast (element_ptr.Ref 104), cast (element_ptr.Ref 105), cast (element_ptr.Ref 106), cast (element_ptr.Ref 107)] (fmap_of_list [(''id'', ''host2'')]) (Some (cast (shadow_root_ptr.Ref 16))))),
(cast (element_ptr.Ref 100), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1''), (''slot'', ''slot5'')]) None)),
(cast (element_ptr.Ref 101), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2''), (''slot'', ''slot6'')]) None)),
(cast (element_ptr.Ref 102), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s3'')]) None)),
(cast (element_ptr.Ref 103), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s4''), (''name'', ''slot4''), (''slot'', ''slot-none'')]) None)),
(cast (element_ptr.Ref 104), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c5''), (''slot'', ''slot5'')]) None)),
(cast (element_ptr.Ref 105), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c6''), (''slot'', ''slot6'')]) None)),
(cast (element_ptr.Ref 106), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c7'')]) None)),
(cast (element_ptr.Ref 107), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c8''), (''slot'', ''slot-none'')]) None)),
(cast (shadow_root_ptr.Ref 16), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 108), cast (element_ptr.Ref 109), cast (element_ptr.Ref 110), cast (element_ptr.Ref 111)])),
(cast (element_ptr.Ref 108), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s5''), (''name'', ''slot5'')]) None)),
(cast (element_ptr.Ref 109), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s6''), (''name'', ''slot6'')]) None)),
(cast (element_ptr.Ref 110), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s7'')]) None)),
(cast (element_ptr.Ref 111), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s8''), (''name'', ''slot8'')]) None)),
(cast (element_ptr.Ref 112), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 14)] fmempty None)),
(cast (character_data_ptr.Ref 14), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]"
definition slots_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "slots_document = Some (cast (document_ptr.Ref 1))"
text \<open>'Slots: Basic.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_basic'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_basic'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp3 \<leftarrow> tmp2 . assignedSlot;
tmp4 \<leftarrow> n . ''s1'';
assert_equals(tmp3, tmp4);
tmp5 \<leftarrow> n . ''s1'';
tmp6 \<leftarrow> tmp5 . assignedNodes();
tmp7 \<leftarrow> n . ''c1'';
assert_array_equals(tmp6, [tmp7])
}) slots_heap"
by eval
text \<open>'Slots: Basic, elements only.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_basic'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''s1'';
tmp2 \<leftarrow> tmp1 . assignedElements();
tmp3 \<leftarrow> n . ''c1'';
assert_array_equals(tmp2, [tmp3])
}) slots_heap"
by eval
text \<open>'Slots: Slots in closed.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_basic_closed'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_basic_closed'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp3 \<leftarrow> tmp2 . assignedSlot;
assert_equals(tmp3, None);
tmp4 \<leftarrow> n . ''s1'';
tmp5 \<leftarrow> tmp4 . assignedNodes();
tmp6 \<leftarrow> n . ''c1'';
assert_array_equals(tmp5, [tmp6])
}) slots_heap"
by eval
text \<open>'Slots: Slots in closed, elements only.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_basic_closed'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''s1'';
tmp2 \<leftarrow> tmp1 . assignedElements();
tmp3 \<leftarrow> n . ''c1'';
assert_array_equals(tmp2, [tmp3])
}) slots_heap"
by eval
text \<open>'Slots: Slots not in a shadow tree.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_slot_not_in_shadow'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_slot_not_in_shadow'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''s1'';
tmp3 \<leftarrow> tmp2 . assignedNodes();
assert_array_equals(tmp3, [])
}) slots_heap"
by eval
text \<open>'Slots: Slots not in a shadow tree, elements only.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_slot_not_in_shadow'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''s1'';
tmp2 \<leftarrow> tmp1 . assignedElements();
assert_array_equals(tmp2, [])
}) slots_heap"
by eval
text \<open>'Slots: Distributed nodes for Slots not in a shadow tree.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_slot_not_in_shadow_2'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_slot_not_in_shadow_2'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp3 \<leftarrow> tmp2 . assignedSlot;
assert_equals(tmp3, None);
tmp4 \<leftarrow> n . ''c2'';
tmp5 \<leftarrow> tmp4 . assignedSlot;
assert_equals(tmp5, None);
tmp6 \<leftarrow> n . ''c3_1'';
tmp7 \<leftarrow> tmp6 . assignedSlot;
assert_equals(tmp7, None);
tmp8 \<leftarrow> n . ''c3_2'';
tmp9 \<leftarrow> tmp8 . assignedSlot;
assert_equals(tmp9, None);
tmp10 \<leftarrow> n . ''s1'';
tmp11 \<leftarrow> tmp10 . assignedNodes();
assert_array_equals(tmp11, []);
tmp12 \<leftarrow> n . ''s2'';
tmp13 \<leftarrow> tmp12 . assignedNodes();
assert_array_equals(tmp13, []);
tmp14 \<leftarrow> n . ''s3'';
tmp15 \<leftarrow> tmp14 . assignedNodes();
assert_array_equals(tmp15, []);
tmp16 \<leftarrow> n . ''s1'';
tmp17 \<leftarrow> tmp16 . assignedNodes(True);
assert_array_equals(tmp17, []);
tmp18 \<leftarrow> n . ''s2'';
tmp19 \<leftarrow> tmp18 . assignedNodes(True);
assert_array_equals(tmp19, []);
tmp20 \<leftarrow> n . ''s3'';
tmp21 \<leftarrow> tmp20 . assignedNodes(True);
assert_array_equals(tmp21, [])
}) slots_heap"
by eval
text \<open>'Slots: Name matching'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_slot_name_matching'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_slot_name_matching'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp3 \<leftarrow> tmp2 . assignedSlot;
tmp4 \<leftarrow> n . ''s1'';
assert_equals(tmp3, tmp4);
tmp5 \<leftarrow> n . ''c2'';
tmp6 \<leftarrow> tmp5 . assignedSlot;
tmp7 \<leftarrow> n . ''s2'';
assert_equals(tmp6, tmp7);
tmp8 \<leftarrow> n . ''c3'';
tmp9 \<leftarrow> tmp8 . assignedSlot;
assert_equals(tmp9, None)
}) slots_heap"
by eval
text \<open>'Slots: No direct host child.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_no_direct_host_child'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_no_direct_host_child'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp3 \<leftarrow> tmp2 . assignedSlot;
tmp4 \<leftarrow> n . ''s1'';
assert_equals(tmp3, tmp4);
tmp5 \<leftarrow> n . ''c2'';
tmp6 \<leftarrow> tmp5 . assignedSlot;
tmp7 \<leftarrow> n . ''s1'';
assert_equals(tmp6, tmp7);
tmp8 \<leftarrow> n . ''c3'';
tmp9 \<leftarrow> tmp8 . assignedSlot;
assert_equals(tmp9, None);
tmp10 \<leftarrow> n . ''s1'';
tmp11 \<leftarrow> tmp10 . assignedNodes();
tmp12 \<leftarrow> n . ''c1'';
tmp13 \<leftarrow> n . ''c2'';
assert_array_equals(tmp11, [tmp12, tmp13])
}) slots_heap"
by eval
text \<open>'Slots: Default Slot.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_default_slot'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_default_slot'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp3 \<leftarrow> tmp2 . assignedSlot;
tmp4 \<leftarrow> n . ''s2'';
assert_equals(tmp3, tmp4);
tmp5 \<leftarrow> n . ''c2'';
tmp6 \<leftarrow> tmp5 . assignedSlot;
tmp7 \<leftarrow> n . ''s2'';
assert_equals(tmp6, tmp7);
tmp8 \<leftarrow> n . ''c3'';
tmp9 \<leftarrow> tmp8 . assignedSlot;
assert_equals(tmp9, None)
}) slots_heap"
by eval
text \<open>'Slots: Slot in Slot does not matter in assignment.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_slot_in_slot'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_slot_in_slot'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp3 \<leftarrow> tmp2 . assignedSlot;
tmp4 \<leftarrow> n . ''s2'';
assert_equals(tmp3, tmp4);
tmp5 \<leftarrow> n . ''c2'';
tmp6 \<leftarrow> tmp5 . assignedSlot;
tmp7 \<leftarrow> n . ''s1'';
assert_equals(tmp6, tmp7)
}) slots_heap"
by eval
text \<open>'Slots: Slot is assigned to another slot'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_slot_is_assigned_to_slot'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_slot_is_assigned_to_slot'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp3 \<leftarrow> tmp2 . assignedSlot;
tmp4 \<leftarrow> n . ''s1'';
assert_equals(tmp3, tmp4);
tmp5 \<leftarrow> n . ''s1'';
tmp6 \<leftarrow> tmp5 . assignedSlot;
tmp7 \<leftarrow> n . ''s2'';
assert_equals(tmp6, tmp7);
tmp8 \<leftarrow> n . ''s1'';
tmp9 \<leftarrow> tmp8 . assignedNodes();
tmp10 \<leftarrow> n . ''c1'';
assert_array_equals(tmp9, [tmp10]);
tmp11 \<leftarrow> n . ''s2'';
tmp12 \<leftarrow> tmp11 . assignedNodes();
tmp13 \<leftarrow> n . ''s1'';
assert_array_equals(tmp12, [tmp13]);
tmp14 \<leftarrow> n . ''s1'';
tmp15 \<leftarrow> tmp14 . assignedNodes(True);
tmp16 \<leftarrow> n . ''c1'';
assert_array_equals(tmp15, [tmp16]);
tmp17 \<leftarrow> n . ''s2'';
tmp18 \<leftarrow> tmp17 . assignedNodes(True);
tmp19 \<leftarrow> n . ''c1'';
assert_array_equals(tmp18, [tmp19])
}) slots_heap"
by eval
text \<open>'Slots: Open > Closed.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_open_closed'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_open_closed'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp3 \<leftarrow> tmp2 . assignedSlot;
tmp4 \<leftarrow> n . ''s1'';
assert_equals(tmp3, tmp4);
tmp5 \<leftarrow> n . ''s1'';
tmp6 \<leftarrow> tmp5 . assignedSlot;
assert_equals(tmp6, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'');
tmp7 \<leftarrow> n . ''s1'';
tmp8 \<leftarrow> tmp7 . assignedNodes();
tmp9 \<leftarrow> n . ''c1'';
assert_array_equals(tmp8, [tmp9]);
tmp10 \<leftarrow> n . ''s2'';
tmp11 \<leftarrow> tmp10 . assignedNodes();
tmp12 \<leftarrow> n . ''s1'';
assert_array_equals(tmp11, [tmp12]);
tmp13 \<leftarrow> n . ''s1'';
tmp14 \<leftarrow> tmp13 . assignedNodes(True);
tmp15 \<leftarrow> n . ''c1'';
assert_array_equals(tmp14, [tmp15]);
tmp16 \<leftarrow> n . ''s2'';
tmp17 \<leftarrow> tmp16 . assignedNodes(True);
tmp18 \<leftarrow> n . ''c1'';
assert_array_equals(tmp17, [tmp18])
}) slots_heap"
by eval
text \<open>'Slots: Closed > Closed.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_closed_closed'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_closed_closed'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp3 \<leftarrow> tmp2 . assignedSlot;
assert_equals(tmp3, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'');
tmp4 \<leftarrow> n . ''s1'';
tmp5 \<leftarrow> tmp4 . assignedSlot;
assert_equals(tmp5, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'');
tmp6 \<leftarrow> n . ''s1'';
tmp7 \<leftarrow> tmp6 . assignedNodes();
tmp8 \<leftarrow> n . ''c1'';
assert_array_equals(tmp7, [tmp8]);
tmp9 \<leftarrow> n . ''s2'';
tmp10 \<leftarrow> tmp9 . assignedNodes();
tmp11 \<leftarrow> n . ''s1'';
assert_array_equals(tmp10, [tmp11]);
tmp12 \<leftarrow> n . ''s1'';
tmp13 \<leftarrow> tmp12 . assignedNodes(True);
tmp14 \<leftarrow> n . ''c1'';
assert_array_equals(tmp13, [tmp14]);
tmp15 \<leftarrow> n . ''s2'';
tmp16 \<leftarrow> tmp15 . assignedNodes(True);
tmp17 \<leftarrow> n . ''c1'';
assert_array_equals(tmp16, [tmp17])
}) slots_heap"
by eval
text \<open>'Slots: Closed > Open.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_closed_open'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_closed_open'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp3 \<leftarrow> tmp2 . assignedSlot;
assert_equals(tmp3, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'');
tmp4 \<leftarrow> n . ''s1'';
tmp5 \<leftarrow> tmp4 . assignedSlot;
tmp6 \<leftarrow> n . ''s2'';
assert_equals(tmp5, tmp6);
tmp7 \<leftarrow> n . ''s1'';
tmp8 \<leftarrow> tmp7 . assignedNodes();
tmp9 \<leftarrow> n . ''c1'';
assert_array_equals(tmp8, [tmp9]);
tmp10 \<leftarrow> n . ''s2'';
tmp11 \<leftarrow> tmp10 . assignedNodes();
tmp12 \<leftarrow> n . ''s1'';
assert_array_equals(tmp11, [tmp12]);
tmp13 \<leftarrow> n . ''s1'';
tmp14 \<leftarrow> tmp13 . assignedNodes(True);
tmp15 \<leftarrow> n . ''c1'';
assert_array_equals(tmp14, [tmp15]);
tmp16 \<leftarrow> n . ''s2'';
tmp17 \<leftarrow> tmp16 . assignedNodes(True);
tmp18 \<leftarrow> n . ''c1'';
assert_array_equals(tmp17, [tmp18])
}) slots_heap"
by eval
text \<open>'Slots: Complex case: Basi line.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_complex'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_complex'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp3 \<leftarrow> tmp2 . assignedSlot;
tmp4 \<leftarrow> n . ''s1'';
assert_equals(tmp3, tmp4);
tmp5 \<leftarrow> n . ''c2'';
tmp6 \<leftarrow> tmp5 . assignedSlot;
tmp7 \<leftarrow> n . ''s2'';
assert_equals(tmp6, tmp7);
tmp8 \<leftarrow> n . ''c3'';
tmp9 \<leftarrow> tmp8 . assignedSlot;
tmp10 \<leftarrow> n . ''s3'';
assert_equals(tmp9, tmp10);
tmp11 \<leftarrow> n . ''c4'';
tmp12 \<leftarrow> tmp11 . assignedSlot;
assert_equals(tmp12, None);
tmp13 \<leftarrow> n . ''s1'';
tmp14 \<leftarrow> tmp13 . assignedSlot;
tmp15 \<leftarrow> n . ''s5'';
assert_equals(tmp14, tmp15);
tmp16 \<leftarrow> n . ''s2'';
tmp17 \<leftarrow> tmp16 . assignedSlot;
tmp18 \<leftarrow> n . ''s6'';
assert_equals(tmp17, tmp18);
tmp19 \<leftarrow> n . ''s3'';
tmp20 \<leftarrow> tmp19 . assignedSlot;
tmp21 \<leftarrow> n . ''s7'';
assert_equals(tmp20, tmp21);
tmp22 \<leftarrow> n . ''s4'';
tmp23 \<leftarrow> tmp22 . assignedSlot;
assert_equals(tmp23, None);
tmp24 \<leftarrow> n . ''c5'';
tmp25 \<leftarrow> tmp24 . assignedSlot;
tmp26 \<leftarrow> n . ''s5'';
assert_equals(tmp25, tmp26);
tmp27 \<leftarrow> n . ''c6'';
tmp28 \<leftarrow> tmp27 . assignedSlot;
tmp29 \<leftarrow> n . ''s6'';
assert_equals(tmp28, tmp29);
tmp30 \<leftarrow> n . ''c7'';
tmp31 \<leftarrow> tmp30 . assignedSlot;
tmp32 \<leftarrow> n . ''s7'';
assert_equals(tmp31, tmp32);
tmp33 \<leftarrow> n . ''c8'';
tmp34 \<leftarrow> tmp33 . assignedSlot;
assert_equals(tmp34, None);
tmp35 \<leftarrow> n . ''s1'';
tmp36 \<leftarrow> tmp35 . assignedNodes();
tmp37 \<leftarrow> n . ''c1'';
assert_array_equals(tmp36, [tmp37]);
tmp38 \<leftarrow> n . ''s2'';
tmp39 \<leftarrow> tmp38 . assignedNodes();
tmp40 \<leftarrow> n . ''c2'';
assert_array_equals(tmp39, [tmp40]);
tmp41 \<leftarrow> n . ''s3'';
tmp42 \<leftarrow> tmp41 . assignedNodes();
tmp43 \<leftarrow> n . ''c3'';
assert_array_equals(tmp42, [tmp43]);
tmp44 \<leftarrow> n . ''s4'';
tmp45 \<leftarrow> tmp44 . assignedNodes();
assert_array_equals(tmp45, []);
tmp46 \<leftarrow> n . ''s5'';
tmp47 \<leftarrow> tmp46 . assignedNodes();
tmp48 \<leftarrow> n . ''s1'';
tmp49 \<leftarrow> n . ''c5'';
assert_array_equals(tmp47, [tmp48, tmp49]);
tmp50 \<leftarrow> n . ''s6'';
tmp51 \<leftarrow> tmp50 . assignedNodes();
tmp52 \<leftarrow> n . ''s2'';
tmp53 \<leftarrow> n . ''c6'';
assert_array_equals(tmp51, [tmp52, tmp53]);
tmp54 \<leftarrow> n . ''s7'';
tmp55 \<leftarrow> tmp54 . assignedNodes();
tmp56 \<leftarrow> n . ''s3'';
tmp57 \<leftarrow> n . ''c7'';
assert_array_equals(tmp55, [tmp56, tmp57]);
tmp58 \<leftarrow> n . ''s8'';
tmp59 \<leftarrow> tmp58 . assignedNodes();
assert_array_equals(tmp59, []);
tmp60 \<leftarrow> n . ''s1'';
tmp61 \<leftarrow> tmp60 . assignedNodes(True);
tmp62 \<leftarrow> n . ''c1'';
assert_array_equals(tmp61, [tmp62]);
tmp63 \<leftarrow> n . ''s2'';
tmp64 \<leftarrow> tmp63 . assignedNodes(True);
tmp65 \<leftarrow> n . ''c2'';
assert_array_equals(tmp64, [tmp65]);
tmp66 \<leftarrow> n . ''s3'';
tmp67 \<leftarrow> tmp66 . assignedNodes(True);
tmp68 \<leftarrow> n . ''c3'';
assert_array_equals(tmp67, [tmp68]);
tmp69 \<leftarrow> n . ''s4'';
tmp70 \<leftarrow> tmp69 . assignedNodes(True);
assert_array_equals(tmp70, []);
tmp71 \<leftarrow> n . ''s5'';
tmp72 \<leftarrow> tmp71 . assignedNodes(True);
tmp73 \<leftarrow> n . ''c1'';
tmp74 \<leftarrow> n . ''c5'';
assert_array_equals(tmp72, [tmp73, tmp74]);
tmp75 \<leftarrow> n . ''s6'';
tmp76 \<leftarrow> tmp75 . assignedNodes(True);
tmp77 \<leftarrow> n . ''c2'';
tmp78 \<leftarrow> n . ''c6'';
assert_array_equals(tmp76, [tmp77, tmp78]);
tmp79 \<leftarrow> n . ''s7'';
tmp80 \<leftarrow> tmp79 . assignedNodes(True);
tmp81 \<leftarrow> n . ''c3'';
tmp82 \<leftarrow> n . ''c7'';
assert_array_equals(tmp80, [tmp81, tmp82]);
tmp83 \<leftarrow> n . ''s8'';
tmp84 \<leftarrow> tmp83 . assignedNodes(True);
assert_array_equals(tmp84, [])
}) slots_heap"
by eval
text \<open>'Slots: Mutation: appendChild.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_complex'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_complex'';
removeWhiteSpaceOnlyTextNodes(tmp1);
d1 \<leftarrow> slots_document . createElement(''div'');
d1 . setAttribute(''slot'', ''slot1'');
tmp2 \<leftarrow> n . ''host1'';
tmp2 . appendChild(d1);
tmp3 \<leftarrow> n . ''s1'';
tmp4 \<leftarrow> tmp3 . assignedNodes();
tmp5 \<leftarrow> n . ''c1'';
assert_array_equals(tmp4, [tmp5, d1]);
tmp6 \<leftarrow> d1 . assignedSlot;
tmp7 \<leftarrow> n . ''s1'';
assert_equals(tmp6, tmp7);
tmp8 \<leftarrow> n . ''s5'';
tmp9 \<leftarrow> tmp8 . assignedNodes(True);
tmp10 \<leftarrow> n . ''c1'';
tmp11 \<leftarrow> n . ''c5'';
assert_array_equals(tmp9, [tmp10, d1, tmp11])
}) slots_heap"
by eval
text \<open>'Slots: Mutation: Change slot= attribute 1.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_complex'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_complex'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp2 . setAttribute(''slot'', ''slot-none'');
tmp3 \<leftarrow> n . ''s1'';
tmp4 \<leftarrow> tmp3 . assignedNodes();
assert_array_equals(tmp4, []);
tmp5 \<leftarrow> n . ''c1'';
tmp6 \<leftarrow> tmp5 . assignedSlot;
assert_equals(tmp6, None);
tmp7 \<leftarrow> n . ''s5'';
tmp8 \<leftarrow> tmp7 . assignedNodes(True);
tmp9 \<leftarrow> n . ''c5'';
assert_array_equals(tmp8, [tmp9])
}) slots_heap"
by eval
text \<open>'Slots: Mutation: Change slot= attribute 2.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_complex'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_complex'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp2 . setAttribute(''slot'', ''slot2'');
tmp3 \<leftarrow> n . ''s1'';
tmp4 \<leftarrow> tmp3 . assignedNodes();
assert_array_equals(tmp4, []);
tmp5 \<leftarrow> n . ''s2'';
tmp6 \<leftarrow> tmp5 . assignedNodes();
tmp7 \<leftarrow> n . ''c1'';
tmp8 \<leftarrow> n . ''c2'';
assert_array_equals(tmp6, [tmp7, tmp8]);
tmp9 \<leftarrow> n . ''c1'';
tmp10 \<leftarrow> tmp9 . assignedSlot;
tmp11 \<leftarrow> n . ''s2'';
assert_equals(tmp10, tmp11);
tmp12 \<leftarrow> n . ''s5'';
tmp13 \<leftarrow> tmp12 . assignedNodes(True);
tmp14 \<leftarrow> n . ''c5'';
assert_array_equals(tmp13, [tmp14]);
tmp15 \<leftarrow> n . ''s6'';
tmp16 \<leftarrow> tmp15 . assignedNodes(True);
tmp17 \<leftarrow> n . ''c1'';
tmp18 \<leftarrow> n . ''c2'';
tmp19 \<leftarrow> n . ''c6'';
assert_array_equals(tmp16, [tmp17, tmp18, tmp19])
}) slots_heap"
by eval
text \<open>'Slots: Mutation: Change slot= attribute 3.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_complex'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_complex'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c4'';
tmp2 . setAttribute(''slot'', ''slot1'');
tmp3 \<leftarrow> n . ''s1'';
tmp4 \<leftarrow> tmp3 . assignedNodes();
tmp5 \<leftarrow> n . ''c1'';
tmp6 \<leftarrow> n . ''c4'';
assert_array_equals(tmp4, [tmp5, tmp6]);
tmp7 \<leftarrow> n . ''c4'';
tmp8 \<leftarrow> tmp7 . assignedSlot;
tmp9 \<leftarrow> n . ''s1'';
assert_equals(tmp8, tmp9);
tmp10 \<leftarrow> n . ''s5'';
tmp11 \<leftarrow> tmp10 . assignedNodes(True);
tmp12 \<leftarrow> n . ''c1'';
tmp13 \<leftarrow> n . ''c4'';
tmp14 \<leftarrow> n . ''c5'';
assert_array_equals(tmp11, [tmp12, tmp13, tmp14])
}) slots_heap"
by eval
text \<open>'Slots: Mutation: Remove a child.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_complex'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_complex'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''c1'';
tmp2 . remove();
tmp3 \<leftarrow> n . ''s1'';
tmp4 \<leftarrow> tmp3 . assignedNodes();
assert_array_equals(tmp4, []);
tmp5 \<leftarrow> n . ''c1'';
tmp6 \<leftarrow> tmp5 . assignedSlot;
assert_equals(tmp6, None);
tmp7 \<leftarrow> n . ''s5'';
tmp8 \<leftarrow> tmp7 . assignedNodes(True);
tmp9 \<leftarrow> n . ''c5'';
assert_array_equals(tmp8, [tmp9])
}) slots_heap"
by eval
text \<open>'Slots: Mutation: Add a slot: after.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_complex'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_complex'';
removeWhiteSpaceOnlyTextNodes(tmp1);
slot \<leftarrow> slots_document . createElement(''slot'');
slot . setAttribute(''name'', ''slot1'');
tmp2 \<leftarrow> n . ''host2'';
tmp2 . appendChild(slot);
tmp3 \<leftarrow> slot . assignedNodes();
assert_array_equals(tmp3, [])
}) slots_heap"
by eval
text \<open>'Slots: Mutation: Add a slot: before.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_complex'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_complex'';
removeWhiteSpaceOnlyTextNodes(tmp1);
slot \<leftarrow> slots_document . createElement(''slot'');
slot . setAttribute(''name'', ''slot1'');
tmp3 \<leftarrow> n . ''s1'';
tmp2 \<leftarrow> n . ''host2'';
tmp2 . insertBefore(slot, tmp3);
tmp4 \<leftarrow> slot . assignedNodes();
tmp5 \<leftarrow> n . ''c1'';
assert_array_equals(tmp4, [tmp5]);
tmp6 \<leftarrow> n . ''c1'';
tmp7 \<leftarrow> tmp6 . assignedSlot;
assert_equals(tmp7, slot);
tmp8 \<leftarrow> n . ''s7'';
tmp9 \<leftarrow> tmp8 . assignedNodes();
tmp10 \<leftarrow> n . ''s3'';
tmp11 \<leftarrow> n . ''c7'';
assert_array_equals(tmp9, [slot, tmp10, tmp11]);
tmp12 \<leftarrow> n . ''s7'';
tmp13 \<leftarrow> tmp12 . assignedNodes(True);
tmp14 \<leftarrow> n . ''c1'';
tmp15 \<leftarrow> n . ''c3'';
tmp16 \<leftarrow> n . ''c7'';
assert_array_equals(tmp13, [tmp14, tmp15, tmp16])
}) slots_heap"
by eval
text \<open>'Slots: Mutation: Remove a slot.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_complex'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_complex'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''s1'';
tmp2 . remove();
tmp3 \<leftarrow> n . ''s1'';
tmp4 \<leftarrow> tmp3 . assignedNodes();
assert_array_equals(tmp4, []);
tmp5 \<leftarrow> n . ''c1'';
tmp6 \<leftarrow> tmp5 . assignedSlot;
assert_equals(tmp6, None);
tmp7 \<leftarrow> n . ''s5'';
tmp8 \<leftarrow> tmp7 . assignedNodes();
tmp9 \<leftarrow> n . ''c5'';
assert_array_equals(tmp8, [tmp9]);
tmp10 \<leftarrow> n . ''s5'';
tmp11 \<leftarrow> tmp10 . assignedNodes(True);
tmp12 \<leftarrow> n . ''c5'';
assert_array_equals(tmp11, [tmp12])
}) slots_heap"
by eval
text \<open>'Slots: Mutation: Change slot name= attribute.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_complex'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_complex'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''s1'';
tmp2 . setAttribute(''name'', ''slot2'');
tmp3 \<leftarrow> n . ''s1'';
tmp4 \<leftarrow> tmp3 . assignedNodes();
tmp5 \<leftarrow> n . ''c2'';
assert_array_equals(tmp4, [tmp5]);
tmp6 \<leftarrow> n . ''c1'';
tmp7 \<leftarrow> tmp6 . assignedSlot;
assert_equals(tmp7, None);
tmp8 \<leftarrow> n . ''c2'';
tmp9 \<leftarrow> tmp8 . assignedSlot;
tmp10 \<leftarrow> n . ''s1'';
assert_equals(tmp9, tmp10);
tmp11 \<leftarrow> n . ''s5'';
tmp12 \<leftarrow> tmp11 . assignedNodes();
tmp13 \<leftarrow> n . ''s1'';
tmp14 \<leftarrow> n . ''c5'';
assert_array_equals(tmp12, [tmp13, tmp14]);
tmp15 \<leftarrow> n . ''s5'';
tmp16 \<leftarrow> tmp15 . assignedNodes(True);
tmp17 \<leftarrow> n . ''c2'';
tmp18 \<leftarrow> n . ''c5'';
assert_array_equals(tmp16, [tmp17, tmp18])
}) slots_heap"
by eval
text \<open>'Slots: Mutation: Change slot slot= attribute.'\<close>
lemma "test (do {
tmp0 \<leftarrow> slots_document . getElementById(''test_complex'');
n \<leftarrow> createTestTree(tmp0);
tmp1 \<leftarrow> n . ''test_complex'';
removeWhiteSpaceOnlyTextNodes(tmp1);
tmp2 \<leftarrow> n . ''s1'';
tmp2 . setAttribute(''slot'', ''slot6'');
tmp3 \<leftarrow> n . ''s1'';
tmp4 \<leftarrow> tmp3 . assignedNodes();
tmp5 \<leftarrow> n . ''c1'';
assert_array_equals(tmp4, [tmp5]);
tmp6 \<leftarrow> n . ''s5'';
tmp7 \<leftarrow> tmp6 . assignedNodes();
tmp8 \<leftarrow> n . ''c5'';
assert_array_equals(tmp7, [tmp8]);
tmp9 \<leftarrow> n . ''s6'';
tmp10 \<leftarrow> tmp9 . assignedNodes();
tmp11 \<leftarrow> n . ''s1'';
tmp12 \<leftarrow> n . ''s2'';
tmp13 \<leftarrow> n . ''c6'';
assert_array_equals(tmp10, [tmp11, tmp12, tmp13]);
tmp14 \<leftarrow> n . ''s6'';
tmp15 \<leftarrow> tmp14 . assignedNodes(True);
tmp16 \<leftarrow> n . ''c1'';
tmp17 \<leftarrow> n . ''c2'';
tmp18 \<leftarrow> n . ''c6'';
assert_array_equals(tmp15, [tmp16, tmp17, tmp18])
}) slots_heap"
by eval
end
Reference in New Issue View Git Blame Copy Permalink