Set Dictionary Item Property

To set a dictionary entry key and value, LW Python looks at the "Values Stack" to find the location (reference) of the dictionary in the Object Store. Then, LW Python will set the key and value. Finally, LW Python will store the modified dictionary back in the Object Store. More formally,

if the following are true:
  • Expression Stack at time t = [ [ ], [ [ function call with name: "__setitem__" and arguments: args, ys ], rest ] ]
  • Value Stack at time t = [ [ value, [ key, [ Python reference idx, [ ] ] ] ], [ next_level, other_levels ] ]
  • the element at index idx of stack (Python Object Store at time t) = Python dictionary entries

then Python Object Store at time (t + 1) = result of storing (Python dictionary (result of storing value at key: key in map: entries)) at index idx of stack (Python Object Store at time t)

For example, suppose that the following are true:
  • Expression Stack at time 17 = [ [ ], [ [ __setitem__(locations, "ES", "Spain"), [ ] ], [ ] ] ]
  • Value Stack at time 17 = [ [ "Spain", [ "ES", [ Python reference 0, [ ] ] ] ], [ [ ], [ ] ] ]
  • Python Object Store at time 17 = [ {"ES": "Estonia", "MX": "Mexico"}, [ ] ]

We claim that:

the element at index 0 of stack (Python Object Store at time 17) = {"ES": "Estonia", "MX": "Mexico"}

Then we can conclude that:

Python Object Store at time (17 + 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 17)

We claim that:

result of storing "Spain" at key: "ES" in map: [ entry "ES": "Estonia", [ entry "MX": "Mexico", [ ] ] ] = [ entry "ES": "Spain", [ entry "MX": "Mexico", [ ] ] ]

Then using substitution, we conclude that:

Python Object Store at time (17 + 1) = [ {"ES": "Spain", "MX": "Mexico"}, [ ] ]

In the Value Stack, 0 is the location of the dictionary in the Object Store, "ES" is the key, and "Spain" is the value that we want to set. LW Python first looks for the dictionary at index 0, then updates the value for "ES" to "Spain" and stores this dictionary back in the Object Store (at the same location).

See here for the full proof.

Try stepping through the simulator to see LW Python update the dictionary in the Object Store.

Code Editor
LW Python State
Current Line1Current Tab0Time0
LW Python Simulator

Comments

Please log in to add comments