功能規約語言是指用於書寫軟體功能規約的語言，通常又稱為功能性語言。軟體功能規約也稱功能規格說明，是軟體所要完成功能的精確而完整的陳述，通常只刻畫軟體系統“做什麼”的外部功能，而不涉及系統“如何做”的內部算法。典型的功能性語言有廣譜語言、Z語言等。
基本介紹
- 中文名：功能規約語言
- 外文名：Functional specification language
- 別稱：功能性語言
- 定義：於書寫軟體功能規約的語言
- 典型類型：廣譜語言、Z語言等
- 學科：軟體術語
簡述,分類,規約對象,規約方法,
簡述
軟體功能規約是軟體所要完成功能的精確而完整的陳述；它描述的是軟體要做什麼，以及只做什麼。功能規約是需求定義的功能抽象，它對需求定義中用戶所需的功能進行重新組織和分塊，使其表述為(接近於)數學模型的形式，以此作為軟體設計與實現的依據。功能語言通常又稱為功能規約語言。
在軟體工程發展早期，軟體功能主要採用非形式的自然語言加以描述。這樣的非形式功能規約具有易書寫、易理解和易使用的特點，一般用戶均會使用；但由於自然語言的歧義性、模糊性和不完備性而導致難以開展軟體的形式化和自動化方法研究。為了提高軟體生產率與軟體產品可靠性，出現了形式軟體功能規約語言。這種語言具有良好的數學基礎，易於研究軟體規約的各種性質和相互間的語義關係，如一致性、完備性、等價性和精化關係等，不僅避免了自然語言‘的歧義性、模糊性和不完備性，而且奠定了能保證程式正確性的各種形式化方法如WP和VDM等方法的基礎。不僅如此，形式功能規約語言還使得軟體自動化的實現成為可能。因此，形式功能規約語言逐漸為人們所接受並套用於軟體工程實踐。
分類
從形式化的角度看，功能語言可分為非形式規約語言和形式規約語言。
非形式規約語言是指未加限定的自然語言，而形式規約語言是指其語法和語義均顯式精確定義的語言。由於軟體功能的形式化描述是計算機科學中十分重要且相對成熟的領域，下文將集中討論形式功能規約語言。從理論基礎的角度看，功能規約語言可分為代數類語言和邏輯類語言。代數類語言系指以異調代數、範疇論等代數理論為主要理論基礎的規約語言，如OBJ，CLEAR等；邏輯類語言系指以一階謂詞演算等邏輯理論為主要理論基礎的規約語言，如Z，VDM-SI.等。當然，有些語言將這兩個途徑有機地結合起來，例如，Larch語言族中每一語言包括共享語言和接口語言兩部分。其中共享語言基於代數方法，而接口語言則基於邏輯方法。此外，還有一類廣譜語言。廣譜語言中不僅包含功能規約機制，還含有設計規約等較低級的成分。
規約對象
規約對象主要包括抽象數據(數據抽象)和抽象過程(過程抽象)兩類。它們分別反映了對軟體系統中所涉及的數據以及相應的處理進行抽象的結果。抽象數據區別於數據的本質特徵在於它只涉及數據及其運算的性質而與具體實現無關；而抽象過程區別於過程的本質特徵在於它只刻畫相應處理“做什麼”的外部行為而與內部的實現細節無關。所謂抽象過程是指從輸入值集到輸出值集的映射；抽象過程規約的主要問題是如何刻畫抽象過程“做什麼”的功能而不涉及“如何做”的具體算法與實現功效。抽象數據通常由抽象數據類型來反映。抽象數據類型是封裝原理和信息隱蔽原理的集中體現；其本質特徵在於與數據具體表示無關。因此，抽象數據類型規約的關鍵問題是如何體現這一特徵。
規約方法
規約方法主要研究如何對抽象過程與抽象數據類型進行規約。前後斷言方法是一種常用的對抽象過程進行規約的方法。它通過給出一對基於一階渭詞演算的斷言，來刻畫抽象過程輸入與輸出的性質及其相互間的關係，以此來描述抽象過程的功能而與具體算法無關。採用前後斷言方法，抽象過程的功能規約由兩部分組成，其一是接門描述，它刻畫了抽象過程與外界的接口，主要包括抽象過程的名、輸入、輸出以及輸入輸出的取值範圍。，其二足功能描述，它刻畫了抽象過程“做什麼”的功能，主要包括前斷言和後斷言兩部分。一般說來，前後斷言方法具有良好的數學基礎，易於研究規約的性質和相互間的關係，如規約的一致性、完備性和精化關係等，但是，前後斷言方法也有局限性，它受限於所能使用的謂詞。
抽象數據類型規約的主要方法有二：其一是代數方法，即用等式公理來商接刻畫抽象數據類型中運算的性質而與具體表示無關；其二是模型方法，即通過給出抽象數據類型的抽象模型來達到規約的目的。
