※ 本文是否可提供台大同学转作其他非营利用途？（须保留原作者 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