簡介
形式程式測試是指在程式測試中採用形式化方法。形式程式測試可以從形式語義方面設計測試程式，測試程式是否有操作語義、指稱語義、代數語義錯誤。形式程式測試是建立在嚴格數學基礎上，比一般程式測試更科學，更嚴謹。
形式化方法
定義
形式概念分析是德國 Will 教授1982 年在數據格理論上通過數據集中對象與屬性之間的二元關係建立概念層次結構，生動簡潔地體現了概念之間的泛化和特化關係，再運用格代數理論進行研究的分析方法。軟體形式化方法是指建立在嚴格數學基礎上的軟體開發方法 。形式化方法模型的主要活動是生成計算機軟體形式化的數學規格說明。形式化方法使軟體開發人員可以套用嚴格的數學符號來說明、開發和驗證基於計算機的系統。 形式化方法的本質是基於數學的方法來描述目標軟體系統屬性的一種技術。不同的形式化方法的數學基礎是不同的，有的以集合論和一階謂詞演算為基礎（如Z和VDM），有的則以時態邏輯為基礎。形式化方法需要形式化規約說明語言的支持。這樣的形式化方法提供了一個框架，可以在框架中以系統的而不是特別的方式刻劃、開發和驗證系統。如果一個方法有良好的數學基礎，那么它就是形式化的，典型地以形式化規約語言給出。這個基礎提供一系列精確定義的概念，如：一致性和完整性，以及定義規範的實現和正確性。形式化方法模型的主要活動是生成計算機軟體形式化的數學規格說明。形式化方法使軟體開發人員可以套用嚴格的數學符號來說明、開發和驗證基於計算機的系統。這種方法的一個變型是淨室軟體工程（cleanroom software engineering），這一軟體工程方法目前已套用於一些軟體開發機構。
軟體形式化方法的分類
根據說明目標軟體系統的方式，形式化方法可以分為兩類：
面向模型的形式化方法。面向模型的方法通過構造一個數學模型來說明系統的行為。
面向屬性的形式化方法。面向屬性的方法通過描述目標軟體系統的各種屬性來間接定義系統行為。
根據表達能力，形式化方法可以分為五類：
基於模型的方法：通過明確定義狀態和操作來建立一個系統模型（使系統從一個狀態轉換到另一個狀態）。用這種方法雖可以表示非功能性需求（諸如時間需求），但不能很好地表示並發性。如：Z語言，VDM，B方法等。
基於邏輯的方法：用邏輯描述系統預期的性能，包括底層規約、時序和可能性行為。採用與所選邏輯相關的公理系統證明系統具有預期的性能。用具體的編程構 造擴充邏輯從而得到一種廣譜形式化方法，通過保持正確性的細化步驟集來開發系統。如：ITL（區間時序邏輯），區段演算（DC），hoare 邏輯，WP演算，模態邏輯，時序邏輯，TAM（時序代理模型），RTTL（實時時序邏輯）等。
代數方法：通過將未定義狀態下不同的操作行為相聯繫，給出操作的顯式定義。與基於模型的方法相同的是，沒有給出並發的顯式表示。如：OBJ， Larch族代數規約語言等；
過程代數方法：通過限制所有容許的可觀察的過程間通信來表示系統行為。此類方法允許並發過程的顯式表示。如：通信順序過程（CSP），通信系統演算 （CCS），通信過程代數（ACP），時序排序規約語言（LOTOS），計時CSP(TCSP），通信系統計時可能性演算（TPCCS）等。
基於網路的方法：由於圖形化表示法易於理解，而且非專業人員能夠使用，因此是一種通用的系統確定表示法。該方法採用具有形式語義的圖形語言，為系統開發和再工程帶來特殊的好處。如 Petri圖，計時Petri圖，狀態圖等。
程式測試
程式測試(program testing)是指對一個完成了全部或部分功能、模組的電腦程式在正式使用前的檢測，以確保該程式能按預定的方式正確地運行。常見測試方法如下：
灰盒測試
灰盒測試，確實是介於白盒測試與黑盒測試之間的，可以這 樣理解，灰盒測試關注輸出對於輸入的正確性，同時也關注內部表現，但這種關注不象白盒那樣詳細、完整，只是通過一些表征性的現象、事件、標誌來判斷內部的運行狀態，有時候輸出是正確的，但內部其實已經錯誤了，這種情況非常多，如果每次都通過白盒測試來操作，效率會很低，因此需要採取這樣的一種灰盒的方法。
白盒測試
白盒測試，又稱結構測試。他的前提是可以把程式看成在一個透明的白盒子裡，測試者完全知道程式的結構和處理算法。這種方法按照程式內部邏輯設計測試用例，檢測程式中的主要執行通路是否能按照預定要求正確工作。
白盒測試根據軟體的內部邏輯設計設施用例，常用的技術是邏輯覆蓋，即考察用測試數據運行被測程式是對程式邏輯的覆蓋程度。主要的覆蓋標準有：語句覆蓋、判定覆蓋、條件覆蓋、判定/條件覆蓋、組合條件覆蓋和路徑覆蓋。
黑盒測試
黑盒測試根據關鍵需求說明書所規定的功能來設計測試用例，它不考慮軟體的內部結構和處理算法。常用的黑盒測試技術包括等價類劃分、邊值分析、錯誤推測和因果圖等。
回歸測試
回歸測試是軟體測試的一種，旨在檢驗軟體原有功能在修改後是否保持完整。回歸測試過程：
識別出軟體中被修改的部分；從原基線測試用例庫“T”中，排除所有不再適用的測試用例，確定對新版本依然有效的測試用例，創建新的基線測試用例庫“TN”；依據一定的策略從TN中選擇測試用例測試被修改的軟體；如果必要，生成新的測試用例集“T1”，用於測試TN無法充分測試的軟體部分；用T1執行修改後的軟體。
