程序分析和單調函數

Question

有人可以在執行程序分析時解釋單調函數的用途嗎？

我目前正在閱讀漢金的「程序分析原理」，但不太明白它的目的。根據定義，單調函數是任何函數，使得對於集合S中的所有元素x和y，如果x（x）= y（f）（x）< = f（y）。

Answer 1

的Knaster-Tarski fixed point theorem說以下內容：

設L是完全格並設f：L→L爲順序保留功能。那麼L中f的不動點集也是一個完整的格。

因爲L中f的不動點集是一個完整的格，所以在L中存在一個f的最小不動點。此外，還有可能有無數個其他不動點。

爲什麼固定點對程序分析很重要？如果格L超過抽象編程狀態，則循環語義的固定點f在邏輯上表示歸納不變量，或者在組中表示特定程序位置處的一組編程狀態，從而從該處執行程序將程序位置從該狀態組中的狀態開始回到同一位置，將在該組狀態內產生狀態。這些狀態集（或歸納不變量）是抽象解釋試圖找到的東西。

對於抽象解釋的直觀描述，我強烈推薦這篇論文，Cousot，P.和Cousot，R .: Static Determination of Dynamic Properties of Programs;它早於「着名的」Cousot and Cousot '77論文，但在高等數學方面略遜一籌。