ATS：使用定理證明進行程式設計/前言

本書旨在使用 ATS 教授實用的程式設計技能：我們專注於實際編寫程式，本書不涵蓋程式設計的其他方面，例如制定問題描述、思考問題以及使用各種解決問題技巧。ATS 與其他程式語言（即 Standard ML 和 OCaml）共享某些方面，但在使用其型別系統支援安全（就型別安全性而言）和高效（就執行時間和記憶體佔用而言）的多種正規化程式設計方面非同尋常。

ATS 支援命令式、函式式和併發程式設計正規化。指令式程式設計是大多數程式設計師熟悉的。函數語言程式設計可以與指令式程式設計形成對比，因為它使程式設計師能夠專注於手頭的任務，而不必過多擔心（無關緊要的）某種實現細節，例如顯式記憶體管理。一些函式式程式可以被視為可執行的規範，這使得它們適合於教學和推理。

眾所周知，程式設計容易出錯（“錯誤”是指“不希望的程式行為”）。緩解問題的一種方法是進行廣泛的測試，但有時，您會想要使用其他方法，例如在型別系統的幫助下，正式宣告前置條件、後置條件和其他不變式。

型別系統已成為一種工具，用於消除某些類別的程式錯誤（例如，確保為物件分配記憶體並正確初始化）。

典型的型別安全程式語言（例如 Pascal 和 Java）不會嘗試將整數型別的變數視為布林型別的變數；這類錯誤在編譯時（早期，在測試之前）被排除。其他錯誤，例如陣列越界訪問，無法在編譯時檢查，因此這些檢查將移至下一階段，即執行程式。該程式保持安全（從某種意義上說），因為即使它出錯，它也不會繼續出錯。

此外，公共 API 通常會在其使用中設定某些限制以使其正常執行。例如，如果將 NULL 傳遞給格式字串，[printf] 會做什麼？在典型的靜態型別程式語言中，不可能強制執行對 [printf] 的編譯時約束：它只接受非 NULL 格式字串。此外，還有一些規則必須在構建格式字串時遵循。

這就是 ATS 的用武之地：它允許您，程式設計師，使用其型別系統正式指定約束。然後，編譯器會在沒有人為干預的情況下檢查這些約束。例如，在 ATS 中，您可以選擇（權衡）證明您的程式永遠不會越界訪問陣列，從而使執行時邊界檢查變得多餘，並增加我們的信心。在這種特定情況下，您無需透過測試來解決此問題。

我們強烈建議我們的讀者不要考慮他們對常見靜態型別程式語言（尤其是 C/C++）的經驗，因為這種經驗在很大程度上不適用於使用 ATS 進行程式設計（因為您不會在這些語言中使用型別來表達約束）；並保持開放的心態，接受新的想法和概念，這些想法和概念起初可能看起來令人困惑，但我們希望在練習一段時間後就能理解。

第一章介紹了 ATS 的純函式式子集，從基本算術開始，一直到函式和資料結構。在本章中，讀者將熟悉沒有賦值和迴圈的程式設計。第二章介紹了基本的指令式程式設計（可變變數和資料結構、顯式控制流運算子），並將其與第一章介紹的語言相關聯。第三章將介紹型別方面的知識，然後介紹一些高階型別，例如單例型別、依賴型別和線性型別。第四章向用戶介紹了使用型別進行程式驗證。