Institute of Information Science
程式語言與形式方法實驗室
Principal Investigators:
王柏堯 Bow-Yaw Wang (Chair) 莊庭瑞 Tyng-Ruey Chuang 陳郁方 Yu-Fang Chen
穆信成 Shin-Cheng Mu

[研究群介紹]

程式語言與形式方法實驗室發展保證程式正確性之技術。 我們在程式語言方面的研究,著重於發展正確程式之語 法、語意、及實務上之議題;在形式方法方面的研究,強 調分析真實程式中演算法、計算、以及實際方面之課題。 我們應用數學及形式技術,以探討我們的研究問題。我們 亦致力於發展工具及方法論,以幫助程式開發者寫作正確 程式。

多核處理器現在被廣泛使用於桌上電腦、筆記型電腦、甚 至是智慧型手機。程式開發者自然想要利用並行性,以提 昇應用程式之效率。但是並行程 式寫作卻相當困難。就算是有經 驗的程式開發者,也會在寫作並 行程式時出錯。因此,雖然並行 電腦已廣為普及,並行程式之數 量仍非常地有限。為了要幫助程 式開發者利用現今處理器之計算 能力,程式語言與形式方法實驗 室故致力於並行程式之語言與驗 證技術。
排版插圖
型別系統已廣泛地應用於現代程 式語言,以確保型別安全。舉例 而言,一個型別不良運算式可能會將數字0和字元’0’相加, 而產生一個不正確的結果。型別系統允許程式開發者,在 編譯時就能指認此類型別錯誤。並行程式寫作易出錯已廣 為人知。而程式開發者的挑戰,在現今由數百甚至數千交 互溝通線程所組成之程式下,更形艱鉅。現代程式語言便 採用型別系統,以保證程式中某類性質。

「會話型別」是一個為傳遞消息並行系統所發展之型別系 統,它能確保線程之間的溝通遵循某些協議。較先進的變 化也能保證無死鎖。現在已做了些努力,藉由嵌入到現有 程式語言,以實現會話型別。不過,由於宿主語言型別系 統表達能力上之限制,這些實現仍然遠遠落後於現在理論 上之發展。我們計劃將會話型別嵌入到 Agda ─ 一個具有 豐富的依賴型別系統之程式語言。希望建立一個程式開發 者寫作Agda/Haskell程式之綜合性環境,並使用型別系統 以保證正確性及終止性。

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

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

局部屬性之合成,是局部推理成功的關鍵。傳統上,局部 屬性乃由定點計算獲得。然而,迭代計算可能是不必要的 昂貴。我們計劃將演算式學習,應用於在局部推理中之合 成問題。當有很多可行的局部屬性,演算式學習可以有效 率地推斷出其中之一。除此之外,學習型合成演算法在推 斷屬性之形式上,給我們更多彈性。這些彈性將幫助我們 了解有關程式之局部屬性。

對一般的程式開發者而言,由於缺乏訓練,運用形式化技術可能並不切 實際。然而,愈來愈多的並行程式正由一般的程式開發者所發展。並行 程式之驗證工具無疑地將幫助程式開發者提高他們的生產力。現有並行 程式的一大部分,是由 C++ 和 Java 等現代程式語言所編寫而成。為 了這些現有的程式,我們還打算開發自動驗證方法,以保證其正確性。 準確地說,我們打算開發並行軟體模型檢測方法。而模型檢測之核心技 術,則是高效率地探索欲驗證程式的狀態空間。

對並行程式而言,由於各個線程交織之行為,造成要被探索之狀態空間 非常之大。為了有效地探索狀態空間,採用抽象技術是必須的。我們計 劃結合現有並行程式之抽象化技術。例如,線程模組化抽象以簡化控制 部分,而謂詞抽象以簡化數據部分。我們的目標是規模化並行軟體模型 檢測,以驗證無法以現有方式處理之程式。

除了我們的研究活動外,我們同時也奉獻顯著的資源於教育。為了介紹 我們的研究給學生,我們自2007年以來,每年舉辦「台灣邏輯,語言和 計算暑期學校(FLOLAC)」。藉由FLOLAC,鼓勵越來越多的台灣學生至 程式語言和形式方法此一領域,學習並進行研究。

相關資訊

Academia Sinica 資訊科學研究所 Academia Sinica