有人質疑PL研究，比如program slicing的價值。如何解釋？

01-05

看這個問題長時間閑置，我就來答一下吧。其實主要原因是旁邊一對情侶秀恩愛啊，神煩啊，這滿圖書館的橘子味，有能耐你也喂我一顆吃啊。

正題：

program slicing 從1981年被Weiser（是的，就是那個提出普適計算的Weiser）在ICSE上提出後，還是在軟體工程界引起不小的影響的，但是題主暗含它是PL的研究內容我也是認同的，因為它的很多後續關鍵性的發展是由一些搞PL的人貢獻的。比如1988年的PLDI（1990年的TOPLAS）由Reps大神等人提出用SDG做slicing的方法一提出來，引起了不小的騷動，各種會議當時和slicing技術相關的論文都是香餑餑啊，包括後來的Reps他們自己回憶，現在在PL界很知名的tabulation演算法，CFL reachability方法，都是有受到做slicing的影響的。

這一點也恰恰表達了我對題主問題的一部分觀點，那就是科研的價值不是說研究的這個東西一定要在實際當中有什麼大用，應用的多麼廣，而是它本身可能對這個領域或其它人有著怎樣的影響，這些影響對後世的價值是不可估量的。那麼多的科研經費不是說投出去都要有成效的，經過幾年或幾十年，這些研究的知識能夠直接或間接地促生像internet這種類似的東西能夠推動改變世界就是值得的投資了。

slicing技術的提出恰恰體現了這一點，光關於slicing的survey的文章就有好多，有的都是上千的引用，你也可以在各種編譯，分析，優化，驗證（包括model checking），還有很多軟體工程技術比如維護，理解，調試等看到關於slicing技術的應用。像Grammatech這種公司就是直接靠slicing技術發家創業的，IBM，Oracle很多公司的分析工具裡面都有slicing及其變種的實現。當然，我需要承認自從2006年以後，關於slicing技術的討論已經不多了，論文數量也變的很少了，但是從81年到06年這20多年的時間，slicing的貢獻是不可小覷的，其實，你可以看到一個research topic能堅持這麼長的熱潮期也不是很多見的。但是這並不意味著slicing以後不會再度興起，因為它在等著某一個enbaling技術或特性的發現，使得它再煥榮光，有些像SMT solver的進步再一次推動symbolic execution的那種感覺。

期望題主和在知乎的各位對計算機知識渴望的人，能成為提出這些enabling技術，推動未來計算機世界發展的人！就像開篇提到的Weiser一樣，雖然已長眠（當然我希望大家長命百歲哈），但他的貢獻無論是普適計算還是slicing，都將激勵著下一個更優秀的Weiser的誕生。

誰在質疑？質疑的究竟是什麼？是 program slicing 本身？還是某個泛泛而談的「PLT」研究？

正如前面朋友 @啥玩應啊所說，program slicing 是過去幾十年很多程序分析研究的起點。但有一點，我希望特別指出——Program slicing 之所以成為歷史上的熱點，恰恰是因為它一直在試圖實踐問題：怎麼去評估（而不是證明）軟體的質量？這個問題和軟體危機的歷史同樣悠久，但是即使至今也沒有解決。這一條，使得這個領域的理論研究風格迥異於很多其他計算機「科學」分支的研究。

但是要理解這個問題，必須要對程序分析的歷史做一些回顧。出於眾所周知的原因，在這個語境中我們暫時只討論命令式語言。

熟悉早年程序開發的朋友一定還記得 Lint 以及後續的各種變種，那是最早的一套試圖解決程序正確性問題的方法論。它實際上是硬性地將程序開發過程中總結出來的現象（或者用程序世界裡的術語，best practice 或 pattern），簡單地映射到某個程序設計語言的語句上。舉個例子：程序員發現，如果變數定義時沒有正確初始化，則程序很容易出錯，於是 lint 中就添加了一條規則：如果掃描代碼時發現一條變數定義語句沒有初始化，則給出一條錯誤。Lint 工具家族在歷史上發揮了巨大的作用，但這個方法有個天生的缺陷：它本質上其實是一組基於經驗的鬆散規則，缺乏系統化理論指導。這個弱點在實踐中造成的問題就是，Lint 系工具的檢出精度很難做到恰到好處，程序員往往或者被迫為了滿足規則而扭曲代碼結構，或者書寫自然卻忍受高誤報率。而更大的問題是：這種方法本質上不是在直接檢出錯誤，而是在要求程序員以一種已知的，錯誤發生率可能性較低的方法組織代碼。換言之，即使程序員這麼寫了，程序仍然可能有 bug。

與此同時，另一條研究脈絡來自程序驗證。這個研究分支試圖將程序抽象為一個模型，並通過某種形式化的方式來驗證它的正確性。在當時那個年代，這種追求絕對程序正確的思想很有誘惑力，但卻在程序複雜性面前挨了當頭一棒——八十年代前後，軟體的規模隨著應用的需求飛速擴大，大型程序的形式化驗證耗時很長，進而導致其工程上的實用性被大幅度削弱，這是很多當時的實踐者對形式驗證的觀點。而在我的個人觀點看來，形式化驗證的真正瓶頸其實有更深層的原因：程序能夠被形式化驗證的前提在於，它能夠被形式化地建模，然而程序本身並不天然地滿足某個形式化模型，那麼，究竟誰才能把代碼翻譯成模型呢？程序化工具的開發者不負責解決這個問題，因為他們不理解業務邏輯；程序員也解決不了這個問題，因為他們缺乏足夠的數學基礎。所以實踐中的結果是，除了硬體設計（模型相對簡單）和國家級基礎工業（軟體正確性要求極高）等部分領域，工業界的軟體開發最終沒有廣泛接受這種方法。

Program slicing 就是在這種條件下出現的。它在試圖解決早年的程序驗證解決不了的兩個問題：在軟體複雜性飛漲的情況下怎樣降低複雜度，以及如何去除程序到模型的轉化步驟。Weiser 的理論選擇通過代碼的「取值」來切入：通過關注代碼中讀寫某個指定變數的所有語句，我們可以有效地抽離出我們需要關注的部分（即所謂的 slicing，「切片」），從而顯著地降低被分析的程序的複雜度；而「取值」本身天然地是程序的一部分，它不需要翻譯的步驟。這就使得它的實用性有望超越程序驗證。因此，Weiser 的理論是一個根據基於當時研究水平的現實情況作出的，極具實用主義風格的分析思路。

在我的眼中，program slicing 方法最大的價值不在於它的創新性，而在於它的實踐性：它試圖關注程序中最直接的部分，即「取值」，來理解程序的正確性。雖然理論上程序錯誤應該首先是邏輯錯誤，但是實踐表明，我們當時還沒有足夠有效的工具，通過將代碼映射到模型從而復原程序員的設計意圖（即使是現在，我個人也很懷疑這種工具是否真的存在）。這個思路的影響是如此深遠，以至於後來一些嚴格說並不屬於這個分支的其他程序分析理論，也一定程度上接受了它的思想，即始終直面代碼，而不是在分析之前要求代碼服從某個理論模型（熟悉 model checking 的朋友也許會理解我在說什麼）。這是一個觀念上的巨大進步，其意義絕不亞於這個理論本身的應用價值。

也因為它的實踐性，Program slicing 技術發展到現在，已經成了程序分析領域的一個基礎性工具，正如快速傅立葉變換之於信號分析。比如我求學時曾工作過的 C++ 靜態程序分析工具項目中，切片操作貫穿了整個分析過程：我們就利用切片來分離出參數變數在函數中經歷的所有分支，進而推導出它在這個函數中執行後可能對參數造成的狀態變化，再繼續參與跨函數間的狀態變化。而函數間的部分，仍然可以通過切片來降低分析的複雜度。

所以如果有人試圖質疑 program slicing 的價值，我只能說他們很可能並不了解程序分析這個領域的發展脈絡，甚至也不理解程序分析這個研究分支的研究風格。或許質疑者自認為自己掌握了什麼「威力十足」的新技術，不巧最近我在不少場合也見了很多這樣的「大神」或者「大牛」。不過呢，如果他們的水準也就是在會議上寫那些口水論文，或者把數學領域裡的某個術語拿來重新定義一下就算是發明了一門新「技術」，那還是洗洗睡吧。

黑Program Slicing還不如黑CFA啊，王垠講Olin Shivers的徒子徒孫們研究了快三十年CFA，都在解決不存在的問題，然而就連0CFA都沒有編譯器敢用（逃