Meeting 24 - Mutable State
Links
Announcements
Anish leading Thursday’s class which will be a review session
- Fill out this piazza poll to vote on which questions to go over
Today
Triage your questions
-
Let’s add updatable variables to our language.
This will require keeping track of memory and thus, a new judgment form.
We will implement this with encapsulated effects.
Mutable Variables Syntax
- What do we need to add to our syntax to include mutable variables?
Our New Syntax
\[ \begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& n \mid x \mid\mathbf{var}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \mid e_1 \mathrel{\texttt{=}}e_2 \\ & & & \mid\mathord{\texttt{*}}e_1 \mid a \\ \text{variables} & x \\[1ex] \text{values} & v& \mathrel{::=}& n \\ \text{location values} & l& \mathrel{::=}& \mathord{\texttt{*}}a \\ \text{addresses} & a \end{array} \]
Memories
- Why do we need memory to handle mutable variables?
- How can we represent memory in our semantics?
New Judgment Form
\[ \langle e, m \rangle \longrightarrow \langle e', m' \rangle \]
\[ \begin{array}{rrrl} \text{states} & \sigma& \mathrel{::=}& \langle e, m \rangle \end{array} \]
Some Inference Rules
\[ \inferrule[DoDeref]{ [a \mapsto v] \in m }{ \langle \mathord{\texttt{*}}a , m \rangle \longrightarrow \langle v, m \rangle } \]
\[ \inferrule[DoAssignVar]{ ??? }{ \langle \mathord{\texttt{*}}a \mathrel{\texttt{=}} v , m \rangle \longrightarrow \langle ??? , ??? \rangle } \]
Variable Decleration
\[ \inferrule[DoVarDecl]{ ??? }{ \langle \mathbf{var}\;x\;\texttt{=}\;v_1\texttt{;}\;e_2 , m \rangle \longrightarrow \langle ??? , ??? \rangle } \]
How do we represent that \(a\) must be a new address?
How do we update the memory?
Considering the \(\TirName{DoDeref}\) rule, how should we modify \(e_2\)?
Updates
- Now, we see that the user has no reason to write \(\mathord{\texttt{*}}a\) on the left side of an assignment. We are abstracting the memory manipulation away, and can update our syntax and semantics to reflect that.
\[ \inferrule[DoAssignVar]{ }{ \langle \mathord{\texttt{*}}a \mathrel{\texttt{=}} v , m \rangle \longrightarrow \langle v, m[a \mapsto v] \rangle } \]
\[ \begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& x \mathrel{\texttt{=}}e_1 \end{array} \]
Inference Rules - Do Rules
\(\fbox{$ \langle e, m \rangle \longrightarrow \langle e', m' \rangle $}\)
\(\inferrule[DoDeref]{ }{ \langle \mathord{\texttt{*}}a , m \rangle \longrightarrow \langle m(a) , m \rangle }\)
\(\inferrule[DoAssignVar]{ }{ \langle \mathord{\texttt{*}}a \mathrel{\texttt{=}} v , m \rangle \longrightarrow \langle v, m[a \mapsto v] \rangle }\)
\(\inferrule[DoVarDecl]{ a\notin \operatorname{dom}(m) }{ \langle \mathbf{var}\;x\;\texttt{=}\;v_1\texttt{;}\;e_2 , m \rangle \longrightarrow \langle {}[ \mathord{\texttt{*}}a /x]e_2 , m[a \mapsto v_1] \rangle }\)
Inference Rules - Search Rules
\(\inferrule[SearchAssign]{ \langle e_2', m \rangle \longrightarrow \langle e_2', m' \rangle }{ \langle l_1 \mathrel{\texttt{=}} e_2 , m \rangle \longrightarrow \langle l_1 \mathrel{\texttt{=}} e_2' , m' \rangle }\)
\(\inferrule[SearchVarDecl]{ \langle e_1, m \rangle \longrightarrow \langle e_1', m' \rangle }{ \langle \mathbf{var}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 , m \rangle \longrightarrow \langle \mathbf{var}\;x\;\texttt{=}\;e_1'\texttt{;}\;e_2 , m' \rangle }\)