形式陈述

可变状态语言的运行状态通常写成配置 $\langle e,\sigma\rangle$$⟨e,\sigma ⟩$，其中存储 $\sigma$$\sigma$ 是从位置到值的有限映射。求值关系同时变换表达式和存储，例如分配产生新位置 $\ell\notin\operatorname{dom}(\sigma)$$\ell \notin \mathrm{dom}(\sigma )$，读取得到 $\sigma(\ell)$$\sigma (\ell )$，写入把存储更新为 $\sigma[\ell\mapsto v]$$\sigma [\ell \mapsto v]$。静态语义还需存储类型 $\Sigma$$\mathrm{\Sigma }$ 记录每个位置的值类型，并证明配置归约保持 $\Gamma;\Sigma\vdash e:T$$\mathrm{\Gamma };\mathrm{\Sigma }⊢e:T$，必要时允许新分配扩展 $\Sigma$$\mathrm{\Sigma }$。

直觉

表达式的结果不再只由自身语法决定，还取决于一个持续演化的外部存储；位置是可共享的身份，而不是把值直接代入变量。

例子与边界

若 r 与 s 指向同一位置，对 r := 1 的写入也改变随后读取 s 的结果，这就是别名。分配需选择新鲜位置，但具体地址通常只在重命名意义下重要。把赋值简单解释为变量替换会遗漏别名、求值顺序和生命周期。并发状态还需额外的内存模型与同步规则，不能由单线程存储语义自动推出。

推论与应用

状态语义支撑引用、数组、对象、闭包环境和命令式程序验证。它也是分离逻辑、效果系统、垃圾回收正确性以及状态 monad 等抽象的语义起点。

参考资料

• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Chs. 34–36, state, references, and store typing。
• Glynn Winskel, The Formal Semantics of Programming Languages, MIT Press, 1993，Chs. 2–5, transition semantics with stores。