B方法，也被稱為B語言，是一種用於描述和設計計算機軟體的嚴格方法。它建立在Zermelo-Frankel集合理論的基礎上，使用符號表示法（廣義代換）來表達狀態的轉換，使程式及其規格說明處於統一的數學框架之下，減少了出現語義錯誤的可能性。B方法根據功能需求進行正確性驗證，保證軟體產品具有高可靠性、可移植性、可維護性。該方法使用AMN（Abstract Machine Notation）作為軟體開發過程中的規約、設計及實現語言，AMN是Dijkstra的衛式命令語言的改進和擴展，在大型軟體系統構造中，具有一種內置的結構化機制。B方法的主要思想包括一種「抽象機」的結構化機制，這種開發方法建立在數學理論基礎上，還包括了廣義替換、精化、軟體的層次體系結構理論。AM是B方法中的一種基本的封裝機制，類似於class，abstract data type，module，package，object等概念，涉及的一些重要思想：數據規約：AM中的數據通過一組數學概念（諸如集合、關係、函式、序列、樹等）說明，這些數據通過某些確定條件規定必須遵守的不變法規和不變式。操作規約：通過不包含定序和循環的非執行的偽代碼表示。每一條操作被描述為一個前置條件和一個原子行為，前置條件是此操作被激活的必要條件，原子行為通過廣義置換方式來形式化表示。所有的原子行為符合不確定性選擇策略。