Pré/Pós-condições

Pré/Pós-condições

Segundo Ghezzi (Guezzi e Jazayeri, 1991), pré/pós-condições são um tipo de especificação lógica que mostra como um processo é classificado construindo-se fórmulas lógicas que relacionam as entradas e saídas do processo. A utilização de pré/pós-condições é uma maneira prática de descrever a função de um processo, sem dar informações sobre seu algoritmo. Uma especificação pré/pós é composta de duas partes principais: Pré-Condições e Pós-Condições.

As Pré-condições propõem de uma maneira geral tudo que deve ser verdadeiro antes que o processo (função) inicie, desta forma é possível especificar:

• As estradas que devem estar disponíveis, exemplo: pode acontecer um acumulo de fluxos de dados ingressando em um processo, mas somente um é necessário para ativá-lo;

• Os relacionamentos entre as entradas, exemplo: pode haver a necessidade de especificar que os fluxos de entrada precisam ter um valor em comum, os códigos das disciplinas que aparecem no fluxo disciplinas oferecidas deve aparecer também no fluxo de informação das disciplinas cadastradas para serem considerados válidos.

• Os valores de um elemento de dados, exemplo: um elemento de dados deve estar dentro de um intervalo, tal como a nota do aluno entre 0 e 10.

• Os relacionamentos entre depósitos de dados, exemplo: pode ser especificando uma pré-condição que estipula que, para cada numero do aluno do deposito de dados de matriculados, existe o número do aluno no deposito externo, que contém, entre outras coisas, os dados cadastrais dos alunos da universidade.

As funções não devem ser executadas se não se reunirem todas as pré-condições. As descrições das pré-condições que não são utilizadas pelo compilador são de grande utilidade para o programador, elas facilitam a compreensão da forma correta de utilizar o código já predefinido. Estas descrições devem encontrar-se junto do protótipo das funções, de forma a facilitar a compreensão das funções através de uma única consulta aos seus protótipos, que devem encontrar-se no ficheiro “hpp".

As pré-condições podem ser implementadas nas funções membro através de condições que devem ser sempre verdadeira. A utilização da macro “assert(condição)”, permite verificar a condição e no caso de falhar termina a aplicação indicando a condição que falhou. Esta macro só existe na versão de “debugger”, não existindo na versão final compilada “release”.

Na linguagem C para utilizar a macro “assert(condição)”, é necessário incluir a biblioteca “cassert”, conforme exemplo apresentado:

#include <cassert> // ou #include <assert.h>

Exemplos sobre a utilização pré-condições:

Exemplo 1:

double celsius(double fahrenheit);

//pré-condições: a variável fahrenheit tem que ser um número maior que zero.

// A variável fahrenheit deve expressar uma temperatura em graus fahrenheits.

//--- Implementação ---

double celsius(double fahrenheit)

{

assert(fahrenheit >0);

return (5.0 / 9.0) * (fahrenheit – 32);

}

Exemplo 2:

void f_resolvente(double a, double b, double c, double & x1, double & x2);

// ----- Formula Resolvente -----

//Pré-condições:

// (b*b - 4*a*c) > 0

// a != 0

//--- Implementação ---

void f_resolvente(double a, double b, double c, double & x1, double & x2)

{

assert(b*b - 4*a*c >= 0);

assert(a != 0);

x1 = (b + sqrt(b*b - 4*a*c)) / (2*a);

x2 = (-b + sqrt(b*b - 4*a*c)) / (2*a);

}

As Pós-condições descrevem o que deve ser verdadeiro quando a função do processo termina após terem sido certificadas as pré-condições. Desta forma é possível especificar:

• As saídas que devem ser geradas pelo processo;

• Os