- Logic 邏輯 - 在這個課程之內，我學到了 Propositional Logic 與 Calculational Logic，還有 Functional Complete 的概念，與 Functional Complete 的證明（事實上，Sum of Product 應該只可以當結果，我們要證 Functional Completeness 要先確認 Propositional Letter 再做 Structural Induction）。除此之外，我還學到了 First Order Logic、Sequent Calculus、Peano Axioms 與 First-order Logic 能力的極限等等很有趣而且過去沒有聽過的東西。
- Functional Programming 函數編程 - 這應該是眾課程當中，我比較熟悉的一個。不過這一門課是教 OCaml （而不是我比較熟悉的 Haskell）。老師就從 Binding 的概念開始，一路介紹到怎麼寫一個函數（遞迴的），還有 High-order Function。另外，還有介紹到 OCaml 之中比較特別的 Parameterized Modules。所謂的 Parameterized Modules 是一個比較特別的 Module，只要你代入幾個參數，Parameterized Modules 會生產出一個新的 Module。我在上這一段的時候，心底想的是 C++ Template 與 Meta-programming。其實感覺起來還蠻像的！XD 不過這一門課的比重偏低，是比較可惜的地方！Folding/Unfolding 的部分就只有快速帶過而己，有一點可惜。
- Operational Semantics 操作語意 - 這個課程是從「操作」的角度來向我們介紹語議。這樣講有一點抽象，簡單地說就是告訴我們要怎麼做才可以達到某個語意。例如：If、While、Assign 等等。這個課程主要又分成二個部分：Natural Semantics 與 Structural Operational Semantics。前者專注於大的概念，所以在 Composited Statement 當中，我們不會考慮比較小的 Statement 的情況，然而在 Structural Operational Semantics 我們會考慮不少細微的變化，包括平行程式執行起來可能會產生的差異等等。
- Program Construction and Reasoning 程式建構與推理 - 這一門課是在教我們怎麼寫一個正確的程式，並且在建構一個程式的同時證明其正確性。在這一堂課當中，我們會用到 Hoare Logic。透過 Precondition、Postcondition、Loop Invariant 還有一些 Rules 讓我們可以知道程式是不是正確的。另外，穆老師還提到了 Goto Considered Harmful 的大論戰等等很有趣的東西！
- Frama-C - Frama-C 是一套可以幫助我們驗證 C 程式寫得對不對的軟體。不過 Frama-C 本身沒有那麼厲害，有時候我們還是必須要加入一些參數，讓參數引導證明！在 Frama-C 這一堂課就會用到 Hoare Logic 與 Loop Invariant 的概念。不同之處在於我們會親自驗證別人寫得程式！所有我們用來練習的程式碼都是取材自開放原始碼的程式，而且真槍實彈地去找 bug。不過我自己覺得要驗證別人的程式好麻煩，尤其是不知道作者的意圖的時候。不過話說回來，或許我會用 Frama-C 驗證我自己的程式。
- Denotation Semantics 指稱語意 - 這堂課和 Operational Semantics 一樣，是在探討程式的語意。然而不同的是 Denotational Semantics 比較在乎函數的 Composition，所有的 Statement 都被理解成更簡單的 Statement 的 Composition。在這個課程當中，我學到了所謂 Recursion 其實是尋找更高一層函式的 Fix Point，這對我來說是一個很特別的想法！過去我想到 Recursion 只會想到 Stack 與 Calling convention 之類的東西。
但是總結來說，FLOLAC 2010 兩個星期的課程值回票價，我很喜歡！
沒有留言:
張貼留言