規格語言

規格語言（英語：Specification language），或稱規範語言，是在計算機科學領域的使用的一種形式語言。程式語言是用於系統實現的、可以直接運行的形式語言。與之不同，規格語言主要用於系統分析和設計的過程中。

規格語言通常是不能直接運行的，雖然有人在進行這方面的研究。規格語言在比程式語言更抽象層次上描述系統，因此，在規格語言被實際實現之前，必須經過一個精簡化（不斷添加實現細節）的過程。

規格語言的一個重要應用是允許創建程序正確性的證明（參見自動定理證明）。

一些規格語言