Proof: Set Dictionary Item Property Example

Let's prove the following theorem:

if the following are true:
  • expression state at time 39 = "call_function_begin"
  • Value Stack at time 39 = [ [ "Spain", [ "ES", [ Python reference 0, [ ] ] ] ], [ ] ]
  • the expression at time 39 = __setitem__(locations, "ES", "Spain")
  • Python Object Store at time 39 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]
  • the element at index 0 of stack (Python Object Store at time 39) = {"ES": "Estonia", "MX": "Mexico"}

then Python Object Store at time 40 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]

Code Editor
LW Python State
Current Line1Current Tab0Time0
LW Python Simulator

Proof:

View as a tree | View dependent proofs | Try proving it

Given
1 expression state at time 39 = "call_function_begin"
2 Value Stack at time 39 = [ [ "Spain", [ "ES", [ Python reference 0, [ ] ] ] ], [ ] ]
3 the expression at time 39 = __setitem__(locations, "ES", "Spain")
4 Python Object Store at time 39 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]
5 the element at index 0 of stack (Python Object Store at time 39) = {"ES": "Estonia", "MX": "Mexico"}
Proof Table
# Claim Reason
1 Python Object Store at time (39 + 1) = result of storing (Python dictionary (result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ])) at index 0 of stack (Python Object Store at time 39) if expression state at time 39 = "call_function_begin" and Value Stack at time 39 = [ [ "Spain", [ "ES", [ Python reference 0, [ ] ] ] ], [ ] ] and the expression at time 39 = __setitem__(locations, "ES", "Spain") and the element at index 0 of stack (Python Object Store at time 39) = {"ES": "Estonia", "MX": "Mexico"}, then Python Object Store at time (39 + 1) = result of storing (Python dictionary (result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ])) at index 0 of stack (Python Object Store at time 39)
2 result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ] = [ entry "ES": "Spain", [ entry "MX": "Mexico", [ ] ] ] result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ] = [ entry "ES": "Spain", [ entry "MX": "Mexico", [ ] ] ]
3 Python dictionary (result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ]) = {"ES": "Spain", "MX": "Mexico"} if result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ] = [ entry "ES": "Spain", [ entry "MX": "Mexico", [ ] ] ], then Python dictionary (result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ]) = {"ES": "Spain", "MX": "Mexico"}
4 result of storing (Python dictionary (result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ])) at index 0 of stack (Python Object Store at time 39) = result of storing {"ES": "Spain", "MX": "Mexico"} at index 0 of stack [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] if Python Object Store at time 39 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] and Python dictionary (result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ]) = {"ES": "Spain", "MX": "Mexico"}, then result of storing (Python dictionary (result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ])) at index 0 of stack (Python Object Store at time 39) = result of storing {"ES": "Spain", "MX": "Mexico"} at index 0 of stack [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]
5 result of storing {"ES": "Spain", "MX": "Mexico"} at index 0 of stack [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ] result of storing {"ES": "Spain", "MX": "Mexico"} at index 0 of stack [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]
6 result of storing (Python dictionary (result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ])) at index 0 of stack (Python Object Store at time 39) = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ] if result of storing (Python dictionary (result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ])) at index 0 of stack (Python Object Store at time 39) = result of storing {"ES": "Spain", "MX": "Mexico"} at index 0 of stack [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] and result of storing {"ES": "Spain", "MX": "Mexico"} at index 0 of stack [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ] = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ], then result of storing (Python dictionary (result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ])) at index 0 of stack (Python Object Store at time 39) = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]
7 Python Object Store at time (39 + 1) = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ] if Python Object Store at time (39 + 1) = result of storing (Python dictionary (result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ])) at index 0 of stack (Python Object Store at time 39) and result of storing (Python dictionary (result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ])) at index 0 of stack (Python Object Store at time 39) = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ], then Python Object Store at time (39 + 1) = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]
8 39 + 1 = 40 39 + 1 = 40
9 Python Object Store at time (39 + 1) = Python Object Store at time 40 if 39 + 1 = 40, then Python Object Store at time (39 + 1) = Python Object Store at time 40
10 Python Object Store at time 40 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ] if Python Object Store at time (39 + 1) = Python Object Store at time 40 and Python Object Store at time (39 + 1) = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ], then Python Object Store at time 40 = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]

Comments

Please log in to add comments