Linguagem de especificação
 | Este artigo não cita fontes confiáveis. (Setembro de 2021) |
Uma linguagem de especificação é uma linguagem formal usada na ciência da computação. Diferente de linguagens de programação, que são linguagens usadas para implementar sistemas executáveis, linguagens de especificação são usadas durante as fases de análise de requisitos e especificação de programa, parte do processo de desenvolvimento de software.
As linguagens de especificação geralmente não são executadas diretamente. Elas descrevem o sistema em alto nível em comparação a uma linguagem de programação. Dessa forma, é considerado um erro a existência de detalhes de implementação em uma especificação, pois deve-se descrever o que deve ser feito, não como.
As especificações devem sofrer um processo de refinamento antes de serem implementadas de fato, isto é, a adição de detalhes de implementação. O resultado de tal refinamento é um algoritmo executável, que é tanto formatado em uma linguagem de programação ou em um subconjunto executável da linguagem de especificação.
Um uso importante de linguagens de especificação é a possibilidade de criar provas matemáticas da validade de um programa.