課程大綱、講義、習題等將於課程網頁更新：
https://scmu.github.io/plip/
===========

「命令」(imperative) 程式語言意指把程式視為「給電腦一個個指令」的語言。我們常用的 C, Python, Java 等語言都可歸屬在此類別下。這類程式語言中，該怎麼寫程式、該怎麼證明程式的正確性？

本課程為「程式語言(Programming Languages)」系列課程之一，著眼點並不是教特定程式語言，而是討論設計程式解決問題的思考方式、設計程式使用的數學與邏輯基礎、以及程式語言與形式符號在其中扮演的角色。本課程以命令程式為主角，其核心概念包括：

* 程式語言是一種形式語言，作為思考的工具。我們用程式語言表達概念，也用程式語言中的形式規則檢驗程式的正確性。


*「寫程式」不只是把程式碼生出來的動作 --- 我們還得確定程式是「對」的。而確定程式正確的唯一方法是證明。

* 「程式推導」：由問題的規格開始，一邊推導出解決該問題的程式，一邊做該程式為何正確的證明。

* 當我們不知一個程式該怎麼寫，「這個程式該怎麼證明」這件事可以反過來透露一些「這個程式該怎麼寫」的提示。

* 「寫程式」是一個數學行為。

* 為了討論使用指標的程式，我們發明了相對應的「分離邏輯」，藉以證明這類程式的正確性。

本課程將討論的具體工具包括

* Dijkstra 的 Guarded Command Language.
* 命題邏輯 (propositional logic)、一階邏輯 (first-order logic)
* Hoare Logic.
* The "weakest precondition" predicate transformer.
* Separation logic.

本課程與「程式語言：函數程式設計」有可呼應之處，但兩者都可獨立修習。本課程亦與「軟體規格與驗證（Software Specification and Verification）」非常相關：命題邏輯、Hoare Logic, predicate transformer 等都是兩堂課共同的元素。該課程談驗證 (verification), 本課程則較注重推導(derivation)，有較多手動計算與演算法問題的推導，而不會嚴謹地談到語意、函數呼叫、concurrency 等課題。