Introdução

Motivação: Verificar o processamento de dados em programas sequenciais.

Método: Baseada em provas; são construídas demonstrações de que o programa verifica as propriedades indicadas.

Automatismo: Semi-automático; alguns passos dessas provas podem ser mecanizados mas outros dependem de supervisão humana — o que frequentemente proporciona boas heurísticas para ajudar o programador.

Âmbito: Certas propriedades formais de um programa; não é feita uma especificação completa do seu comportamento.

Domínio: Os programas sequenciais transformacionais correm num único processador (sequencial, não concorrente); recebem uma entrada e terminam produzindo uma saída (transformacional).

Desenvolvimento: Aplica-se antes do desenvolvimento para formalizar o funcionamento de segmentos críticos de um sistema e durante a implementação a pequenos fragmentos de código que executam uma tarefa identificável (logo especificável);

Racional:

• Melhor documentação. A estrutura lógica de uma especificação formal organiza uma implementação que a verifica.
• Menos tempo de desenvolvimento. As especificações formais reduzem significativamente o tempo gasto na depuração e nos testes. Também contribuem para reduzir erros de planeamento e clarificar os papéis e contributos estruturais das várias componentes de um sistema.
• Refatorização mais simples. Componentes propriamente especificadas e verificadas são mais facilmente reutilizadas e re-implementadas.
• Certificações em auditorias. A prova que um programa está conforme a sua especificação é uma das garantias solicitadas durante a certificação de sistemas críticos.