可变状态语义

纯 λ 演算中，变量可由值替换；一旦引入可变引用，同一个位置的内容会随时间改变，程序含义便依赖“现在的存储是什么”。最有效的图像是两层映射：变量名找到一个抽屉编号，存储记录每个抽屉此刻装什么。别名使两个不同表达式指向同一抽屉，因此局部赋值可能被远处代码观察到。闭包理路程序语言闭包Programming-language closure · Function closure · Lexical closure将函数代码与其定义位置的词法环境配对而成的运行时函数值。捕获可变变量时也通常保存这个位置，而非复制某一时刻的内容。

程序 let r = ref 0 in r := 1; !r 先分配新位置 $\ell$ 并存入 $0$，赋值把存储更新为 $\sigma [\ell \mapsto 1]$，最后读取结果 $1$。若再令 s = r，则 s := 2 后 !r 也为 $2$，因为 r 与 s 是同一位置的别名。

边界是把赋值误作普通代换。表达式 f(r); !r 的结果取决于 f 是否能写入该位置，不能把 r 在源码中简单替换为初始值。垃圾回收通常不改变可观察语义，但若语言暴露地址、终结器或弱引用，就需要更细致的等价条件。

可变状态语义为命令式语言、对象、数组和函数共享可变位置提供基础。分离逻辑理路分离逻辑Separation logic以分离合取表达互不重叠资源并局部推理堆内存的程序逻辑。以堆的可分资源结构支持局部推理，所有权与借用理路所有权与借用Ownership and borrowing · Ownership type system · Borrow checking以所有者、移动、共享或独占借用及生命周期约束静态组织资源责任与别名访问。则用静态 owner、loan 和生命周期限制别名访问；两者都建立在位置与存储之上，却不是运行配置本身。

静态分析可把许多具体位置归入有限抽象单元。Andersen分析理路Andersen 包含式指针分析Andersen pointer analysis · Inclusion-based points-to analysis地址获取、复制、解引用读写如何生成只增的points-to包含约束。从取地址、复制和间接读写生成包含约束；Steensgaard分析理路Steensgaard 合一式指针分析Steensgaard pointer analysis · Unification-based points-to analysis把可能别名合成等价类为什么更快，又会在哪个小程序上丢掉精度。则用存储形状合一压缩目标表示。二者都要覆盖真实别名，但合一可能把只经一个汇合变量相遇的两个目标传播回其他变量，精度差别可在四条赋值上手算出来。

面向对象程序还可用对象敏感分析理路对象敏感指针分析Object-sensitive pointer analysis · Object sensitivity为什么用接收者的分配身份区分方法实例，比仅记调用位置更适合某些面向对象程序。，按接收者的抽象身份区分同一方法的调用上下文。这与按字段名区分存储槽是两项选择；若两个真实对象已被合并到同一抽象堆名，方法上下文也无法凭空恢复它们的区别。

在并发环境中，多个线程共享 $\sigma$ 会产生数据竞争理路数据竞争Data race · 数据竞态不同线程对同一内存位置的冲突访问既未按模型同步排序、也未通过原子操作协调的情形。和原子性问题；事务、内存模型与并发对象语义都可看作对这套基本配置的扩展。证明有状态程序等价或表示独立时，有状态逻辑关系理路逻辑关系Logical relation · Logical predicate · Reducibility relation按类型结构定义值与计算之间的关系，用于把局部类型规则提升为终止、等价或参数性结论。还需用 possible worlds 或 step index 记录两边堆单元的持续对应，而不能只比较当前返回值。