「Program=Proof筆記」修訂間的差異

於 2024年3月3日 (日) 21:36 的最新修訂

題名：Program=Proof

中譯（暫）：證明=程式

作者：Samuel Mimram

---

開頭作者舉例一個式子在數字很大的時候會出錯的案例，來說明證明的重要性。

之後提到證明即程式（利用程式的性型別）的概念。

檢查程式：

空中巴士公司使用形式方法來驗證程式是否出錯誤。

CompCert 用 coq 來造出證明程式符合語義的C編譯器。

自動化證明：

證明數學是一種藝術。和驗證是否錯誤比，較難。就如積分比微分難一樣。

依值型別：

@@ 行 1： / 行 1： @@
 {{Nav|程式語言、邏輯學}}
 : 題名：Program=Proof
-: 中譯：證明=程式
+: 中譯（暫）：證明=程式
 :作者：Samuel Mimram
 :{{isbn|9798615591839}}
@@ 行 29： / 行 29： @@
 == Ch1 有型別的函數式程設 ==
-===1.1介紹===
-<pre>(* 我是註解 *)
-print_endline "string" (*  函數使用，一般寫法：print_endline("string")*)
+* [[Program=Proof筆記-第1章]]
-</pre>
-ocamlopt 可以編譯
-<pre>
-# 2 + 2 ;;
--: int = 4
-(* 對結果做型別推導 *)
-let s = string_to_int 3.2
-(* -> 這會型別錯誤 *)
-</pre>
-; Type annotation（型別顯式標記）
-比較：
-<pre>
-let f x = x + 1
-let f (x : int ) : int = x + 1
-</pre>
-;型別
-List.map 的型別：<code>('a -> 'b) -> 'a list -> 'b list</code>
-<code>let mapped_list = List.map (fun x -> 2 * x) a_list</code>
-; 可變變數(reference)
-<pre>
-let () =
-  let r = ref 0 in (* 可變 reference *)
-  for i = 0 to 9 do
-     r := !r + 1 (* 刷新 r 值，使其 + 1）
-  done
-</pre>
-另外還有 record、array、GADT、垃圾回收等等。
 [[分類:資訊]]
 [[分類:邏輯學]]