compiler-construction - 程序分析和单调函数

Question

有人可以在执行程序分析时解释单调函数的目的吗？

我目前正在阅读 Hankin 的“程序分析原理”，但不太了解它的目的。

根据定义，单调函数是任何函数，使得对于集合 S 中的所有元素 x 和 y，如果 x <= y => f(x) <= f(y)。

Answer 1

Knaster-Tarski 不动点定理说明如下：

令 L 为完全格，令 f : L → L 为保序函数。那么L中f的不动点集也是一个完全格。

由于 L 中 f 的不动点集是一个完全格，因此 L 中存在 f 的最小不动点。此外，可能存在无限多个其他不动点。

为什么固定点对程序分析很重要？如果格 L 超过抽象程序状态，则循环语义的固定点 f 在逻辑上表示归纳不变量，或者在集合中表示特定程序位置处的一组程序状态，以便从该位置执行程序程序位置从那组状态中的一个状态开始返回到同一位置，将产生那组状态中的一个状态。这些状态集（或归纳不变量）是抽象解释试图找到的。

对于抽象解释的直观描述，我强烈推荐论文 Cousot, P. 和 Cousot, R.: Static Determination of Dynamic Properties of Programs；ISOP 1976。它早于“著名的” Cousot 和 Cousot '77论文，但在高等数学方面的泥潭较少。