【雜記】FLOLAC '10

　　2010 Formosan Summer School on Logic, Language, and Computation（FLOLAC ’10），是辦在台大進修推廣部的暑期碩士學分班。雖然是碩士學分班，但由於剛好符合相關學系大二以上的報名資格，又在半自願被網友 yen3 「騙來」的狀態下還是報名了XD。




　　對於一個語言，我們可以從兩個觀點來看它：一個是語法（syntax），即語言本身的規則（rule）與形式（form）；另一個則是語意（semantics），為語言本身所表達的意義（meaning）。

　　寫出可以執行的程式也許不難，要寫出正確的程式卻不簡單。當我們得到一段程式，我們該如何分析、驗證這個程式的結果，以確保其確實符合我們的預期？更甚者，我們該如何在撰寫程式的同時，也確保我們建構出來的程式一定是正確的？

　　對於程式語法上的錯誤（syntax error）可以經由編譯器（compiler）或直譯器（interpreter）來幫我們檢查出來。但是，語意上的錯誤（logic error 或稱 semantic error）卻難以經由其他工具來協助我們察覺。

　　一般我們也許習慣利用測試資料來確認程式的正確性：只要程式能通過所有的測試資料（即輸出結果符合預期），我們就可以「假設」程式是正確的了。不過，要產出全面性的測試資料本身有其難度，再加上此種方式必須仰賴於程式的實作（implement），作為驗證並不是一種非常好的方式。

　　而 FLOLAC '10 這一系列的課程，主要的內容就是教導如何以邏輯推理為基礎，從語意的角度將程式形式化（formalize）並進行分析。以及用以輔助的 Frama-C 分析工具的使用。



　　不過 FLOLAC ’10 的時程有兩天跟期末考撞期，所以一開始就請了兩天假。直到第三天的 Logic 跟 Op 課都已經是第二堂課，FP 課甚至已經結束了。要在沒聽過第一堂課的情況下銜接上內容，一開始還真是一個頭兩個大。還好後來漸漸跟上了，總算有種進入狀況的感覺。

　　歷經了兩週八點準時起床出門上課，直到下午五點下課，比暑假前還規律的暑假生活，水深火熱的 FLOLAC '10 終於順利結束了。雖然課程有點辛苦，不過接觸了不少人、也接觸了不少新東西，感覺收獲也相當多。

　　遇見了 yen3、GSR、dryman，還有其他周圍的人、努力想搞懂 Frama-C 到底在做什麼、跟 dryman 一起到麥當勞邊念書邊聊天、期末考前在 Google Wave 上熱烈的討論。對於整個 FLOLAC 的課程，我想我還滿樂在其中的。


　　雖然不知道自己能學到多少，又能應用多少。不過也許就像 yen3 所說：「能體會，就能產生質變」。或許在之後就會發現，現在學過的這些，其實都有潛移默化的作用也說不定。