400 (resettable variable) A resettable variable is defined as follows. There are three new names: value (of type X ), set (a procedure with one parameter of type X ), and reset (a program). Here are the axioms:
valueʹ=x ⇐ set x valueʹ=value ⇐ set x. reset reset. reset = reset
Implement this data structure, with proof.
§ Let value: X be a user’s variable, and let old: X be an implementer’s variable. set = 〈x: X→ old:= value. value:= x〉
reset = value:= old Proof:
(valueʹ=x ⇐ set x)
= (valueʹ=x ⇐ old:= value. value:= x)
= (valueʹ=x ⇐ oldʹ=value ∧ valueʹ=x)
= ⊤(valueʹ=value ⇐ set x. reset)
= (valueʹ=value ⇐ old:= value. value:= x. value:= old)
= (valueʹ=value ⇐ oldʹ=valueʹ=value)
= ⊤(reset. reset = reset)
= (value:= old. value:= old = value:= old) =⊤