抽象釋義

在計算機科學中，抽象釋義是基於在有序集合特別是格上的單調函數，計算機程序的語義的可靠逼近理論。它可以被看作對計算機程序的部分執行，獲取關於它的語義信息(比如，控制結構、信息流)而不進行所有計算。

它的主要具體應用是形式靜態分析，關於計算機程序的可能執行的信息的自動提取；比如這種分析有兩個主要用途:

在編譯器內部，分析程序來確定特定優化或變換是否是可適用的；
針對缺陷類的程序的調試甚至校驗。

抽象釋義是 Patrick Cousot 和 Radhia Cousot 所形式化的。

直覺[編輯]

我們現在展示一下抽象釋義在現實世界中非計算例子的意味着什麼。

讓我們考慮在會議室中人們。如果我希望證明某個人不在場，一個具體的方式是查看所有參與者的名字和唯一於他們的某種標識符比如美國的社會保障編號的列表。因為沒有兩個人有相同的編號，有可能證明或反證一個參與者的出席，簡單的通過在列表中查找他的名字或他的編號。

但是我們可以限制自己只登記他們的名字。如果一個人的名字在列表中沒有找到，我們可以安全的結論說這個人不在場；但是如果有這個名字，我們不能明確的結論而不做進一步的質詢，原因是有可能重名。我們要注意這個不精確的信息對多數用途是足夠的，因為實踐中重名是很少見的。但是在嚴格的情況下，我們不能確切的說某個人在屋子裡；我們只能說他可能在這裡。如果我們查找的這個人是罪犯，我們將發出「警報」；但是當然有可能發出「假警報」。類似的現象將出現在程序的分析中。

如果我們只感興趣於某些特定信息，比如「有年齡 n 歲的人在屋子中嗎？」，則必須保存所有人的名字和生日的列表是不必需的。我們可以安全和不損失精確的限制自身保存參與者的年齡的列表。如果這處理起來太多了，我們可以只保存極小年齡 m 和極大年齡 M。如果問題是關於嚴格小於 m 或嚴格大於 M 的年齡，則我們可以安全的回應沒有這個參與者在場。否則，我們只能說不知道。

在計算的情況下，具體的精確的信息在有限時間和內存內一般是不能計算的(參見Rice定理和停機問題)。抽象被用來把問題一直簡化到有職能自動解答的問題。減少精度的一個關鍵要點是使問題易於處理而對回答你感興趣的問題(比如「程序會崩潰嗎?」)仍保持足夠的精度。

計算機程序的抽象釋義[編輯]

給定一個編程或規定語言，抽象釋義一般由抽象關係連接的一些語義所構成。語義是程序的可能行為的數學特徵化。描述了非常接近程序的實際執行的最精確的語義被稱為具體語義。例如，指令式編程語言的具體語義可能對每個程序關聯上它可以生成的執行跟蹤的集合 – 執行跟蹤是程序執行的一序列的可能的連續狀態；狀態典型的構成自程序計數器和內存位置(全局、棧和堆)的值。更抽象的語義是導出的，比如你可以只考慮在執行中可觸及的狀態的集合(相當於考慮在有限跟蹤中的最後狀態)。

靜態分析的目標是在某些點上導出可計算的語義釋義。例如，可以選擇表示操縱整數變量的程序的狀態，通過忘記變量的實際值並只保持它們的符號(+, - 或 0)。對於某些基本運算比如乘法，這種抽象不丟失任何精度: 要得到乘積的符號，知道操作數的符號就足夠了。對於某些其他運算，抽象可能丟失精度: 比如不可能知道操作數分別是正和負的求和的符號。

有時精度的丟失對使語義成為可決定性的是必需的(參見Rice定理, 停機問題)。一般的說，在分析的精度和它的可決定性(可計算性)或可跟蹤性(複雜性)之間要做出妥協。

在實踐中定義的抽象適合於想要分析的程序性質和目標程序的集合二者。

形式化[編輯]

設 L 是叫做具體集合的有序集合，並設 L′是叫做抽象集合的另一個有序集合。通過定義映射一個的元素到另一個的元素的全函數，把這兩個集合相互聯繫起來。

函數 α 叫做抽象函數，如果它映射在具體集合 L 中的元素 x 到抽象集合 L′中的元素 α(x)。就是說，在 L′中的元素 α(x) 是 L 中的元素 x 的抽象。

函數 γ 叫做具體化函數，如果它映射在抽象集合 L′中的元素 x′到具體集合 L 中的元素 γ(x′)。就是說，在 L 中的元素 γ(x′) 是 L′中的元素的 x′的具體化。

設 L₁, L₂, L′₁ 和 L′₂ 是有序集合。具體語義 f 是從 L₁ 到 L₂ 的單調函數。從 L′₁ 到 L′₂ 的函數 f′被稱為 f 的有效抽象，如果對於所有 L′₁ 中的 x′有 (f ∘γ)(x′) ≤ (γ∘f′)(x′)。

程序語義在循環或遞歸過程在場的情況下一般使用不動點來描述。我們設 L 是完全格並設 f 是從 L 到 L 的單調函數。則任何 x′使得 f′(x′) ≤ x′是 f 的最小不動點的抽象，它依據 Knaster-Tarski定理而存在。

困難現在是獲得這樣的 x′。如果 L' 是有限高度的，或最多檢驗「升鏈條件」(所有上升序列最終都固定)，則這樣的 x′可獲得為通過如下歸納法定義的上升序列 x′_n 的固定極限: x′₀=⊥ (L′的最小元素) 並且 x′_n+1=f′(x′_n)。

在其他情況，仍有可能通過拓寬算子∇ 來的得到這種 x′: 對於所有的 x 和 y，x ∇ y 應當大於等於 x 和 y 二者，並且對於所有序列 y′_n，定義自 x′₀=⊥ 並且 x′_n+1=x′_n ∇ y′_n 的序列最終是固定的。我們接着選取 y′_n=f(x′_n)。

在某些情況，有可能使用伽羅瓦連接 (α, γ) 來定義抽象，這裡的 α 是從 L 到 L′而 γ 是從 L′到 L 的單調函數。這假定了最好抽象的存在性，這不是必然的情況。例如，如果我們通過套入凸多面體抽象實數對 (x,y) 的集合，則對於 x²+y² ≤ 1 定義的圓盤沒有最優抽象。

抽象域的例子[編輯]

在一個給定程序點上可以向每個變量 x 指派一個區間 [l_x,h_x]。指派值 v(x) 到變量 x 的狀態是這些區間的具體化，如果對於所有 x 有 v(x) 在 [l_x,h_x] 中。從給變量 x 和 y 的區間 [l_x,h_x] 和[l_y,h_y]，可以輕易的獲得 x+y 的區間([l_x+l_y,h_x+h_y]) 和 x-y 的區間([l_x-h_y,h_x-l_y])；注意這些是精確抽象，因為可能結果比如 x+y 的集合，精確的是區間 ([l_x+l_y,h_x+h_y])。可以為乘法、除法等推導出更複雜的公式，生成所謂的區間算術。

現在我們考慮下列非常簡單的程序:

y = x;
z = x - y;

帶有合理的算術類型，z 的結果應當是零。但是如果我們做區間算術開始於 x 在 [0,1] 中。我們得到 z 在 [-1,1]。儘管進行的每個運算都單獨的精確抽象了，它們的複合不是。

問題是顯然的: 我們不跟蹤在 x 和 y 之間的相等關係；實際上，這個區間的域不考慮在變量間的任何關係，因此是非關聯域。非關聯域趨向更快和實現簡單但不精確。

關聯數值抽象域的某些例子有:

凸多面體 – 帶有某種高計算代價
「八角形」
difference-bound 矩陣
線性方程

和它們的組合。

在選擇抽象域的時候，典型必須在保持精細關聯和高計算代價之間作出權衡。

參見[編輯]

工具[編輯]

ASTRÉE （頁面存檔備份，存於網際網路檔案館）
PolySpace Technologies （頁面存檔備份，存於網際網路檔案館）
PAG （頁面存檔備份，存於網際網路檔案館） and PAG/WWW （頁面存檔備份，存於網際網路檔案館）
Sparrow （頁面存檔備份，存於網際網路檔案館）
Goanna

外部連結[編輯]