基本介紹
直覺,電腦程式的抽象釋義,形式化,
直覺
我們現在展示一下抽象釋義在現實世界中非計算例子的意味著什麼。
讓我們考慮在會議室中人們。如果我希望證明某個人不在場，一個具體的方式是查看所有參與者的名字和唯一於他們的某種標識符比如美國的社會保障編號的列表。因為沒有兩個人有相同的編號，有可能證明或反證一個參與者的出席，簡單的通過在列表中查找他的名字或他的編號。
但是我們可以限制自己只登記他們的名字。如果一個人的名字在列表中沒有找到，我們可以安全的結論說這個人不在場；但是如果有這個名字，我們不能明確的結論而不做進一步的質詢，原因是有可能重名。我們要注意這個不精確的信息對多數用途是足夠的，因為實踐中重名是很少見的。但是在嚴格的情況下，我們不能確切的說某個人在屋子裡；我們只能說他可能在這裡。如果我們查找的這個人是罪犯，我們將發出“警報”；但是當然有可能發出“假警報”。類似的現象將出現在程式的分析中。
如果我們只感興趣於某些特定信息，比如“有年齡n歲的人在屋子中嗎？”，則必須保存所有人的名字和生日的列表是不必需的。我們可以安全和不損失精確的限制自身保存參與者的年齡的列表。如果這處理起來太多了，我們可以只保存極小年齡m和極大年齡M。如果問題是關於嚴格小於m或嚴格大於M的年齡，則我們可以安全的回應沒有這個參與者在場。否則，我們只能說不知道。
在計算的情況下，具體的精確的信息在有限時間和記憶體內一般是不能計算的(參見Rice定理和停機問題)。抽象被用來把問題一直簡化到有職能自動解答的問題。減少精度的一個關鍵要點是使問題易於處理而對回答你感興趣的問題(比如“程式會崩潰嗎?”)仍保持足夠的精度。
電腦程式的抽象釋義
給定一個編程或規定語言，抽象釋義一般由抽象關係連線的一些語義所構成。語義是程式的可能行為的數學特徵化。描述了非常接近程式的實際執行的最精確的語義被稱為具體語義。例如，指令式程式語言的具體語義可能對每個程式關聯上它可以生成的執行跟蹤的集合 – 執行跟蹤是程式執行的一序列的可能的連續狀態；狀態典型的構成自程式計數器和記憶體位置(全局、棧和堆)的值。更抽象的語義是導出的，比如你可以只考慮在執行中可觸及的狀態的集合(相當於考慮在有限跟蹤中的最後狀態)。
靜態分析的目標是在某些點上導出可計算的語義釋義。例如，可以選擇表示操縱整數變數的程式的狀態，通過忘記變數的實際值並只保持它們的符號(+, - 或 0)。對於某些基本運算比如乘法，這種抽象不丟失任何精度: 要得到乘積的符號，知道運算元的符號就足夠了。對於某些其他運算，抽象可能丟失精度: 比如不可能知道運算元分別是正和負的求和的符號。
在實踐中定義的抽象適合於想要分析的程式性質和目標程式的集合二者。
形式化
設L是叫做具體集合的有序集合，並設L′是叫做抽象集合的另一個有序集合。通過定義映射一個的元素到另一個的元素的全函式，把這兩個集合相互聯繫起來。
函式 α 叫做抽象函式，如果它映射在具體集合L中的元素x到抽象集合L′中的元素 α(x)。就是說，在L′中的元素 α(x) 是L中的元素x的抽象。
函式 γ 叫做具體化函式，如果它映射在抽象集合L′中的元素x′到具體集合L中的元素 γ(x′)。就是說，在L中的元素 γ(x′) 是L′中的元素的x′的具體化。
設L1,L2,L′1和L′2是有序集合。具體語義f是從L1到L2的單調函式。從L′1到L′2的函式f′被稱為f的有效抽象，如果對於所有L′1中的x′有 (f∘γ)(x′) ≤ (γ∘f′)(x′)。
程式語義在循環或遞歸過程在場的情況下一般使用不動點來描述。我們設L是完全格並設f是從L到L的單調函式。則任何x′使得f′(x′) ≤x′是f的最小不動點的抽象，它依據Knaster-Tarski定理而存在。
困難現在是獲得這樣的x′。如果 L' 是有限高度的，或最多檢驗“升鏈條件”(所有上升序列最終都固定)，則這樣的x′可獲得為通過如下歸納法定義的上升序列x′n的固定極限:x′0=⊥ (L′的最小元素) 並且x′n+1=f′(x′n)。
在其他情況，仍有可能通過拓寬運算元∇ 來的得到這種x′: 對於所有的x和y，x∇y應當大於等於x和y二者，並且對於所有序列y′n，定義自x′0=⊥ 並且x′n+1=x′n∇y′n的序列最終是固定的。我們接著選取y′n=f(x′n)。
