Nos últimos vinte anos, houve um progresso lento, porém constante, no uso de especificação formal, no desenvolvimento de software. Nos métodos de especificação formal, o objetivo de se produzir especificações consistentes, completas e corretas é obtido por meio de enunciados matematicamente prováveis. Uma especificação formal pode assim ser checada, em termos de inconsistências e contradições, antes de ser codificada, utilizando-se uma linguagem de programação. A lógica de primeira ordem pode ser uma base para se descrever uma especificação formal. Para isso, são utilizados símbolos matemáticos que expressam um significado importante. Uma lista dos principais símbolos é mostrada abaixo.

Asserções são utilizadas para expressar pré-condições e pós-condições de um determinado procedimento. As pré-condições e as pós-condições são condições que devem ser obedecidas, respectivamente, para que o procedimento possa ser realizado com sucesso e para indicar que o procedimento foi realizado com sucesso. A forma geral para se especificar um procedimento funcional, utilizando a especificação formal, é definir, na ordem, as pré-condições, o processo e as pós-condições dentro da sintaxe e da semântica da linguagem formal que se está utilizando. Abaixo são mostradas três especificações, utilizando-se a lógica, cujos símbolos são mostrados no texto, como linguagem formal, e utilizando-se, igualmente, asserções de pré-condições e pós-condições.

A especificação 3 representa a classificação ou o ordenamento descendente ou decrescente em valor de uma lista de números inteiros e positivos. O processo não garante que o conteúdo de !$ \alpha [i] !$, para !$ 0 < i < n !$, sendo !$ n>0 !$, será preservado do início ao fim do processo.