[評價] 111-1 蔡益坤 軟體規格與驗證
※ 本文是否可提供臺大同學轉作其他非營利用途？（須保留原作者 ID）
（是／否／其他條件）：n
哪一學年度修課： 111-1
ψ 授課教師 (若為多人合授請寫開課教師，以方便收錄) 蔡益坤
λ 開課系所與授課對象 (是否為必修或通識課 / 內容是否與某些背景相關) 資管系 / 資管所選修
δ 課程大概內容
Propositional Logic, First Order Logic, Intuitionistic Logic
這部份會教各種邏輯表達式的操作方法、語意及形式上的證明。
假如我們可以透過亂湊符號 (x) 不需要智慧 (o) 的方法來證明一個邏輯表達式，那代表電腦也可以做到。
Coq
這是一個自動化的邏輯證明軟體。
不過，比起自動化的部份，課程比較著重在如何把手寫的證明送給 Coq 解決。
Hoare Logic
算是課程標題中「軟體規格」的開始。
這個邏輯系統負責描述一行程式必須在什麼情況下被執行，以及執行完之後會符合哪些性質。
Weakest Precondition, Weakest Liberal Precondition (Predicate Transformers)
這兩個符號負責描述一行程式正常執行所需的最寬鬆條件。
如果符合 wp 的話，程式會正常執行，而且一定會停下來。
符合 wlp 的話，程式有可能會卡住，但是假如他停下來，就一定會是符合期望的結果。
Frama-C
這個工具可以自動化驗證 C 程式的正確性，連遞迴、迴圈等等都有辦法證明。
不過，跟數論有關的部份會證得很辛苦，需要手動用 Coq 來輔助。
Owicki-Gries Method
這個系統負責證明平行化程式的正確性。
由於兩份平行的程式可能會互相影響，所以需要在 Hoare Logic 中加入額外的技巧來確保意外不會發生。
UNITY, Linear Temporal Logic
描述一個事件發生之後，另外一個事件一定會發生、某事件不會一直發生... 等等的行為。
Ω 私心推薦指數(以五分計，很主觀) ★★★★★
課程內容 ★★★★★
上課模式 ★★★☆
涼度 ★★★☆
甜度 ★★★★
總評 ★★★★☆
η 上課用書(影印講義或是指定教科書)
都是用教授自己做的投影片，不過有附大量的 reference。雖然我沒看^H^H^H^H^H
μ 上課方式(投影片、團體討論、老師教學風格)
不確定前幾年的上課狀況，今年只有 8 個人選。
雖然班很小，但還是講解居多，發問 / 討論的環節幾乎沒有。
下課的時候滿常有人去問問題的。
投影片比較像是講課內容的重點整理。如果沒有聽過課的話，直接看投影片可能會有點謎。
教授的講話語氣偏平淡，且講話內容很少會離題 / 偏題。板上有人問同教授計算理論的評價，底下 rrro 的說法很準。
上課節奏的話... 感覺這幾年都被線上課 3 倍速養壞了。現場聽課感覺中偏慢，恍神一下下還勉強能聽懂。
σ 評分方式(給分甜嗎？是紮實分？)
HW 20%
參與度 10%
Term Project 30%
期末考 40%
教授在學期末直接把所有人的成績細項都丟到課程網站上了，而且沒有碼學號。
8 個人裡面 1 個 A+, 1 個 A，可是因為樣本數很小，不確定甜度。
ρ 考題型式、作業方式
作業共 6 份，出了之後過一週 due，教授表示要花 6hr 左右。
寫完之後就解決期末考大部分的題目了 (x
作業的寫法也大部分放在投影片 / lecture notes 裡面，先複習過之後寫起來會很快。
有些需要 syntactically 證明的部份，可能會重複擦擦寫寫很久，手很酸。
課程內容全都公佈在教授維護的 wiki site 上，包含作業與歷年期末考題。
期末考跟歷年考題有很大部份重疊，寫完考古之後應該可以秒殺。其中一題教授還說「這題出很久了，我會一直出到 50% 學生答對為止」。
Term Project 是用 Frama-C 來證明一個演算法的正確性，期末後一週交。主題自選，可以 (and 建議) 先跟教授討論好。
個人覺得，找到適合的演算法比證明還難很多。有些演算法 (e.g. DFS) 看似簡單，但證明的難度非常非常高。
ω 其它(是否注重出席率？如果為外系選修，需先有什麼基礎較好嗎？老師個性？
加簽習慣？嚴禁遲到等…)
跟計算邏輯簡介對比的話，這堂課比較著重各種知識 / 工具的應用。
隔壁計邏簡的 proof tree 可能只要寫 5 層，這堂會有 10 層以上的題目。
如果想當學分小偷的話，滿推薦同時修的。這兩堂課重複的部份不少，而且會互相講到比較少 cover 的地方。
體感要付出 4 學分的努力，總共拿到 6 學分，賺不賺就看個人。
Ψ 總結
整體來說算是 loading 低，但是收穫頗多的課。
很意外這麼好玩的課只有不到 10 個人選。如果開在資工系的話，可能會比較多人有興趣 (?
BTW 課程網站是公開的，在 http://im.ntu.edu.tw/~tsay/dokuwiki/doku.php?id=courses:ssv2022:main
--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 140.112.16.135 (臺灣)
※ 文章網址: https://www.ptt.cc/bbs/NTUcourse/M.1673454745.A.54A.html
※ 編輯: aoaaceai (140.112.16.135 臺灣), 01/12/2023 00:34:55
推
01/12 14:50,
1年前
, 1F
01/12 14:50, 1F
推
01/12 23:22,
1年前
, 2F
01/12 23:22, 2F
推
01/13 15:07,
1年前
, 3F
01/13 15:07, 3F