fix stupid typo

Author: Forever-CodingNoob

source/_posts/2025-02-20-113-1-大三上修課心得.md

@@ -123,7 +123,7 @@ figure > figcaption {
 課程分為四個單元(各一份投影片)，每個單元會介紹一個或多個logic system(s)，後面再介紹它的應用。按教的順序列出為(藍綠色的部份是理論，黃色部份是應用)：
 1. <font color="#87ffd3">Propositional logic(definitions, proof rules, semantics, CNF, validity, satisfiability, Horn clause), SAT Solvers(Tseitin transformation(這個蕭班ADA有教), SAT algorithms(Davis Putnam, DLL))</font>。有修過[偶數年FLOLAC](https://flolac.iis.sinica.edu.tw/zh/2024/)或ADA的人應該會對部份的內容感到熟悉。
 2. <font color="#87ffd3">Predicate logic(definitions, proof rules, semantics, undecidability of validity problem), expressiveness(reachability problem, existential second-order logic, universal second-order logic)</font>, <font color="#fff285">Coq</font>
-3. Proof-based program verification: <font color="#87ffd3">Hoare logic(Hoare triple, proof rules, proof tableaux, loop invariant)</font>, <font color="#fff285">Z3 solver</font>。Hoare logic部份的內容幾乎是穆信成開授的[程式語言：命令程式設計](https://scmu.github.io/plip/)教的東西的subset，只是兩者視角與強調的重點不一樣。前者使用natral deduction來描述proof rules(像[維基百科](https://en.wikipedia.org/wiki/Hoare_logic#Rules)這樣)，後者則使用calculational logic(先定義weakest precondition，再定義程式語言裡的各種語句組成的Hoare triple與什麼東西等價)。(我對邏輯還是不太熟，有錯請不吝指正。)我覺得還蠻有趣的。
+3. Proof-based program verification: <font color="#87ffd3">Hoare logic(Hoare triple, proof rules, proof tableaux, loop invariant)</font>, <font color="#fff285">Z3 solver</font>。Hoare logic部份的內容幾乎是穆信成開授的[程式語言：命令程式設計](https://scmu.github.io/plip/)教的東西的subset，只是兩者視角與強調的重點不一樣。前者使用natural deduction來描述proof rules(像[維基百科](https://en.wikipedia.org/wiki/Hoare_logic#Rules)這樣)，後者則使用calculational logic(先定義weakest precondition，再定義程式語言裡的各種語句組成的Hoare triple與什麼東西等價)。(我對邏輯還是不太熟，有錯請不吝指正。)我覺得還蠻有趣的。
 4. Model Checking: <font color="#87ffd3">LTL</font>, <font color="#fff285">Promela & Spin</font>, <font color="#87ffd3">CTL, CTL*, LTL model-checking algorithm, CTL model-checking algorithm</font>。LTL model-checking algorithm與自動機有關(有用到NFA)，而CTL model-checking algorithm部份教到的fixpoint theorem其實高等編譯器設計的助教課也有教，只是後者教得很爛就是了。
 
 這門課是我到目前為止在台大修過品質最高的課之一，同樣優質的課程好像只有蔡國榮教授的線性代數導論一/二。除了教授講課講得十分清楚外，教授與助教也都很熱心地回答同學問題。我在上完課後幾乎都會問問題{%spoiler 前提是我沒蹺課%}，感謝他們讓我占用寶貴的時間。此外，這門課的高品質也體現於投影片上。教授的投影片內容充實、編排精美、格式工整，即使有些小缺陷，它還是能排在台大課程投影片排行榜的S tier。老實說，我常常因睡過頭而蹺課，但我都能在課後只靠著啃投影片吸收當週十成甚至九成的課程內容。可能有人會問我怎麼沒去上課也能知道教授教了什麼，這是因為教授上課講的東西幾乎都有寫在投影片上，但這並不表示教授上課時是照著投影片唸的——他是用自己的話解釋投影片的內容。