Page 36 - profile2014.indd

程式語言與形式方法實驗室

Lab

研究人員
王柏堯 Bow-Yaw Wang 程式語言與形式方法實驗室發展保證程式正確性之技術。我們在程式語言方面
Research Fellow 的研究，著重於發展正確程式之語法、語意、及實務上之議題;在形式方法方面
莊庭瑞 Tyng-Ruey Chuang 的研究,強調分析真實程式中演算法、計算、以及實際方面之課題。我們應用數
Associate Research Fellow 學及形式技術，以探討我們的研究問題。我們亦致力於發展工具及方法論，以
陳郁方 Yu-Fang Chen 幫助程式開發者寫作正確程式。
Associate Research Fellow
穆信成 Shin-Cheng Mu 多核處理器現在被廣泛使用於桌上電腦、筆記型電腦、甚至是智慧型手機。程
Associate Research Fellow 式開發者自然想要利用並行性，以提昇應用程式之效率。但是並行程式寫作卻
相當困難。就算是有經驗的程式開發者，也會在寫作並行程式時出錯。因此，
雖然並行電腦已廣為普及，並行程式之數量仍非常地有限。為了要幫助程式開
發者利用現今處理器之計算能力，程式語言與形式方法實驗室故致力於並行程
式之語言與驗證技術。

型別系統已廣泛地應用於現代程式語言，以確保型別安全。舉例而言，一個型
別不良運算式可能會將數字 0 和字元 ’0’ 相加，而產生一個不正確的結果。
型別系統允許程式開發者，在編譯時就能指認此類型別錯誤。並行程式寫作易
出錯已廣為人知。而程式開發者的挑戰，在現今由數百甚至數千交互溝通線程
所組成之程式下，更形艱鉅。現代程式語言便採用型別系統，以保證程式中某
類性質。「會話型別」是一個為傳遞消息並行系統所發展之型別系統，它能確
保線程之間的溝通遵循某些協議。較先進的變化也能保證無死鎖。現在已做了
些努力，藉由嵌入到現有程式語言，以實現會話型別。不過，由於宿主語言型
別系統表達能力上之限制，這些實現仍然遠遠落後於現在理論上之發展。我們
計劃將會話型別嵌入到 Agda ─ 一個具有豐富的依賴型別系統之程式語言。希
望建立一個程式開發者寫作 Agda/Haskell 程式之綜合性環境，並使用型別系
統以保證正確性及終止性。

我們對於以「證明即程式」方式達到程式正確性要求的程式設計方法與工具(
如: Coq )，深感興趣，將探究這類工具的細節、功能以及限制。我們選定了三
項應用領域的題目來作為研習的標的：一、正規表達式的導數，二、結構化內
容的轉換，三、軟體元件間的互動。這三項應用領域內的題目，與一般應用程
式的開發與正確性，有相當關聯。例如，網頁程式是否能安全執行、正確輸出、
以及良好互動，分別和以上一、二、三項應用領域中的一些問題相關。

模型檢測是一種指認程式設計錯誤之技術。給定一個有關設計的屬性，模型檢
測工具藉由搜索設計行為，以決定性地驗證給定之屬性。對並行系統而言，設
計的行為與設計組件之數量成指數增長。這是眾所周知的狀態爆炸問題。局部
推理是一種為減緩在驗證並行系統中狀態爆炸問題，所發展之組合分析技術。
異於探索全局之狀態，此組合技術合成局部屬性，並在設計組件中驗證這些屬
性。除了古典有限並行程式，局部推理亦被用來分析參數系統。

局部屬性之合成，是局部推理成功的關鍵。傳統上，局部屬性乃由定點計算獲
得。然而，迭代計算可能是不必要的昂貴。我們計劃將演算式學習，應用於在

36 研究群 Research Laboratories