「Program=Proof筆記」修訂間的差異
跳至導覽
跳至搜尋
Tankianting（討論 | 貢獻） （`） |
Tankianting（討論 | 貢獻） |
||
| （未顯示同一使用者於中間所作的 8 次修訂） | |||
| 行 1： | 行 1： | ||
{{Nav|程式語言、邏輯學}} | |||
: 題名：Program=Proof | : 題名：Program=Proof | ||
: | : 中譯（暫）：證明=程式 | ||
:作者：Samuel Mimram | :作者：Samuel Mimram | ||
:{{isbn|9798615591839}} | :{{isbn|9798615591839}} | ||
--- | --- | ||
== Ch0 序言 == | |||
開頭作者舉例一個式子在數字很大的時候會出錯的案例，來說明證明的重要性。 | 開頭作者舉例一個式子在數字很大的時候會出錯的案例，來說明證明的重要性。 | ||
| 行 24： | 行 26： | ||
* Agda 與 Coq 幫助漸次展開證明 | * Agda 與 Coq 幫助漸次展開證明 | ||
* 證明時間 > 測試時間 | * 證明時間 > 測試時間 | ||
* | * 重要的軟體使用之驗證 | ||
== Ch1 有型別的函數式程設 == | |||
* [[Program=Proof筆記-第1章]] | |||
[[分類:資訊]] | |||
[[分類:邏輯學]] | |||
[[ | |||
[[ | |||
於 2024年3月3日 (日) 21:36 的最新修訂
- 題名：Program=Proof
- 中譯（暫）：證明=程式
- 作者：Samuel Mimram
- ISBN 9798615591839
---
Ch0 序言
開頭作者舉例一個式子在數字很大的時候會出錯的案例，來說明證明的重要性。
之後提到證明即程式（利用程式的性型別）的概念。
檢查程式：
空中巴士公司使用形式方法來驗證程式是否出錯誤。
CompCert 用 coq 來造出證明程式符合語義的C編譯器。
自動化證明：
- 特定問題會比較快
- 但不代表能一定求解出證明
證明數學是一種藝術。和驗證是否錯誤比，較難。就如積分比微分難一樣。
依值型別：
- Agda 與 Coq 幫助漸次展開證明
- 證明時間 > 測試時間
- 重要的軟體使用之驗證