2008/05/10

Why naive program transformation systems are unlikely to work

這篇是 E.W. Dijkstra 對於 program transformation 的小評論,編號 EWD 636。(Dijkstra 的 manuscripts 收集在 E.W. Dijkstra Archive,有空可以上去逛逛。)前面一半介紹 program transformation 並和傳統方法比較,後面一半是 Dijkstra 的質疑。他的主要論點大概有三:

  • Derivation 的過程太長,因為已發現的 transformation steps 太過瑣細;
  • 正確的 specification 並不見得好寫;
  • 從 specification 不一定能透過一條 semantic-preserving path 而抵達理想的演算法。
Dijkstra 針對的應該是(至少接近)「自動的」(機械式的)程式轉換系統,所以第一個論點對 AoP-style derivation 並不造成絕大的衝擊(雖然我覺得的確需要發展更強的定理)。後面兩個就真的比較麻煩,特別是第三個。不知道有沒有人做過這種 "completeness" 的證明?

--
我猜不外乎要重整到 formal logic 或 / 和 lambda calculus 吧?

Labels:

<< 回到主頁