在計算機科學中，形式化規范是基于數學的技術，其目的是為了幫助系統和軟件的實現。它們被用來描述一個系統，分析它的行為，并通過嚴格和有效的推理工具驗證感興趣的關鍵屬性來幫助其設計。這些規范是正式的，因為它們有一個語法，它們的語義屬于一個領域，并且它們能夠被用來推斷有用的信息。

在每一個過去的十年中，計算機系統變得越來越強大，因此，它們對社會的影響也越來越大。正因為如此，我們需要更好的技術來幫助設計和實現可靠的軟件。已有的工程學科使用數學分析作為創建和驗證產品設計的基礎。形式化的規范是在軟件工程可靠性中實現這種曾經預言的方式之一。其他方法，如測試，更常用于提高代碼質量。

給予這樣的規范，就有可能使用形式化驗證技術來證明系統設計相對于其規范是正確的。這使得不正確的系統設計可以在實際實施的任何重大投資之前被修改。另一種方法是使用可能正確的細化步驟來將規范轉化為設計，而設計最終會被轉化為一個構造正確的實現。值得注意的是，正式的規范不是一個實現，而是可以用來開發一個實現。形式化規范描述了一個系統應該做什么，而不是系統應該如何做。一個好的規范必須具有以下一些屬性：充分的、內部一致的、不含糊的、完整的、滿意的、最小的一個好的規范將具有。可構建性、可管理性和可進化性可用性可交流性強大而有效的分析對形式化規范感興趣的主要原因之一是，它們將提供一種對軟件實現進行證明的能力。這些證明可以用來驗證一個規范，驗證設計的正確性，或者證明一個程序滿足規范。

一個設計（或實現）不能單獨被宣布為"正確"。它只能是"相對于一個給定的規范而言是正確的"。形式化的規范是否正確描述了要解決的問題是一個單獨的問題。這也是一個難以解決的問題，因為它最終涉及到構建非正式具體問題域的抽象形式化表示的問題，而這樣的抽象步驟是無法進行形式化證明的。然而，通過證明有關規范預期表現的屬性的"挑戰"定理來驗證一個規范是可能的。如果正確的話，這些定理會加強規范制定者對規范的理解以及它與基本問題領域的關系。如果不正確，規范可能需要改變，以更好地反映那些參與制作（和實現）規范的人的領域理解。軟件開發的形式化方法在工業界并沒有被廣泛使用。大多數公司認為在他們的軟件開發過程中應用這些方法是不經濟的。這可能是由于各種原因，其中一些是。

初始啟動成本高，可衡量的回報低靈活性很多軟件公司使用注重靈活性的敏捷方法。對整個系統進行正式的規范往往被認為是靈活性的反面。然而，有一些研究表明在敏捷開發中使用形式化規范的好處復雜性它們需要高水平的數學專業知識和分析技能來有效地理解和應用它們解決這個問題的方法是開發工具和模型，使這些技術得以實施，但隱藏基礎數學范圍有限它們不能捕獲項目中所有利益相關者感興趣的屬性它們不能很好地指定用戶界面和用戶交互不具成本效益這并不完全正確，通過將它們的使用限制在關鍵系統的核心部分，它們已被證明具有成本效益其他限制。

范例形式化規范技術在不同領域和不同規模上已經存在了相當長的時間。形式化規范的實現會因其試圖建模的系統種類、應用方式以及在軟件生命周期的哪個階段被引入而有所不同。這些類型的模型可以分為以下幾類