人读程序时，很容易顺着代码从上往下看；分析器却不能只走眼前这一条路。一次条件判断会产生分支，一个循环会把执行带回原处，异常和返回语句还可能让程序提前离开。 要分析程序，首先得把所有可能的去向画出来，再说明每走一步，程序状态会发生什么变化。这篇文章就从这两个问题出发：程序能走到哪里，以及到达那里时状态变成了什么。 上一篇文章已经把程序状态理解为“变量到值”的映射： [\sigma:X\r...

读软件工程论文时，最让人泄气的时刻，往往不是看不懂算法，而是读到一半突然被一行符号挡住：每个字母似乎都见过，连在一起却不知道该从哪里读起。 这种停顿通常与数学能力无关。论文只是把研究对象、程序状态和分析步骤压缩进了几行定义，却省略了初学者最需要的阅读顺序。本文要做的，就是把这些定义重新展开，翻译成自然语言和熟悉的程序操作。 先看两种常见写法： [\sigma\in\Sigma=X\ri...

本文记录如何在 VMware Fusion 中，让 Ubuntu 虚拟机通过 Mac 上的 VPN/代理软件访问 Google、GitHub、apt 源等外网资源。 实验环境示例： 宿主机：macOS 虚拟机软件：VMware Fusion 虚拟机系统：Ubuntu Server VMware 网络模式：Share with my Mac Mac 代理软件：Flyi...

As the last article of this series, today we will discuss the denotational semantics for imperative programs. Specifically, we will check out how to apply CPO model on the $\text{while}$ programs i...

In this article, we consider the domain-theoretic semantics of PCF. This provides some insight into the properties of CPOs, and also provides the basis for semantic reasoning about PCF. We show so...

Fixed Points and the Full Continuous Hierarchy Our current motivation for studying domain-theoretic models is to construct Henkin models of typed lambda calculi with fixed-point operators. The t...

In the last article, we provides a full set-theoretic interpretation for typed lambda calculus based on the Henkin model. However, the function recursion in PCF is hard to model from a pure set vie...

In this series, let us check out the denotational semantics of typed lambda calculus, which uses models to express the meaning of terms. For most logical systems, a model provides a mechanism for ...

In preceding articles, we considered functional programs that do not contain assignment or other operations that change the values of identifiers. In computer science, of course, it is more common ...

In this article, we introduce a new mathematical framework which is simpler than typed lambda calculus, called universal algebra (or equational logic). This framework will be useful when we model i...