7月 11, 2010

【雜記】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 所說:「能體會,就能產生質變」。或許在之後就會發現,現在學過的這些,其實都有潛移默化的作用也說不定。

2 回覆:

pf 提到...

加油哦,我參加過,不過只去一個星期,看到一堆112的,就棄考啦~~沒修過…慚愧啊…

C.E.W. 提到...

謝謝啦:)

其實我原本因為期末考請太多假,還不能去考試的(缺課含請假超過九小時)。結果後來是講師們決議讓我補簽三小時,好不容易才有考試資格。

雖然如此,會不會考過.....其實我還滿沒信心的耶XD

張貼留言