Set Key and Value Property 1

result of storing value at key: key in map: entries = output of function store_compute where input key is key, value is value, map is entries, and processed map is [ ]

This property says that setting a key to a value in a map is equivalent to a set operation that tracks a few other inputs:

• Entries we already processed ("processed").
• Remaining entries ("remaining").

Initially, "processed" is empty, since we haven't processed any entries yet (hence [ ] in the property). "Remaining" is the map entries, and "key found" is false.

Other properties will allow us to move entries from "remaining" to "processed" as we search for key.

Examples

result of storing "Texas" at key: "TX" in map: [ entry "FL": "Florida", [ entry "AZ": "Arizona", [ ] ] ] = output of function store_compute where input key is "TX", value is "Texas", map is [ entry "FL": "Florida", [ entry "AZ": "Arizona", [ ] ] ], and processed map is [ ]

result of storing "Eastern Time" at key: "EST" in map: [ entry "PST": "Pacific Time", [ ] ] = output of function store_compute where input key is "EST", value is "Eastern Time", map is [ entry "PST": "Pacific Time", [ ] ], and processed map is [ ]

Comments

Please log in to add comments