Lógica para Computação (IF61B) Lógica para Computação: Especificação e Verificação de Programas Prof. Celso Antônio Alves Kaestner, Dr. Eng. [email protected]

Lógica para Computação (IF61B)

Lógica para Computação:Especificação e Verificação

de ProgramasProf. Celso Antônio Alves Kaestner, Dr. Eng.

[email protected]

Alterado e complementado por

Prof. Adolfo Neto, D.Sc.

[email protected]


25/05/09 Prof. Celso A A Kaestner 2

Especificação de programas• Uma tarefa típica em Computação:

• Especificações em linguagem natural exigem que se assuma o significado de diversos termos, e por isto são “imprecisas / vagas / inconsistentes” permitindo diversas interpretações;

• Este é um problema amplamente estudado em Engenharia de Software, que busca métodos e formalismos tenta eliminar / reduzir este problema.

Modelagemproblema computacionalproblema real



Especificação de programasVisão operacional de um programa:

Programas como transformadores de estados:

...

programa

1 = {v1

1,v12...v1

m} = {v2

1,v22...v2

m} = {vn

1,vn2...vn

m}

dados de entrada

dados de saída



Especificação de programas Especificação de propriedades de programas:• Exemplo: dados dois valores (x e y) inteiros maiores

ou iguais a 10 calcular sua soma (z);

• Especificação 1: – sobre o estado inicial: x 10 y 10– sobre o estado final: z = x + y

• Especificação 2 (superespecificação):– sobre o estado inicial: x 10 y 10 (x + y) 0 – sobre o estado final: z = x + y z 20



Especificação de programas• Especificação 3 (especificação pouco clara):

– sobre o estado inicial: x 10 (x + y) (10 + x)– sobre o estado final: z = x + y

• Especificação 4 (especificação incompleta):– sobre o estado inicial: x 10 – sobre o estado final: z = x + y

• “Especificação” 5 (não é especificação ...):– sobre o estado inicial: x 10 y 10– sobre o estado final: z = x + y z < 10



Especificação de programas

• Vantagens de se ter uma especificação definida por formalismo matemático:

1. Precisão;

2. Verificação de consistência;

3. Simulação;

4. Verificação de programas.

• Pode-se usar a Lógica Matemática como linguagem de especificação (SILVA; FINGER; MELO, 2006, p. 165);




Sistematização das propriedades de programas:

1. Pré-condições: válidas sobre os dados de entrada;

2. Pós-condições: válidas sobre os dados de saída;

3. Invariantes: válidas sempre, durante toda a execução do programa.



• Exemplo: fatorial.

1 se n=0

n! = 1 sen=1

n*(n-1)! se n>1

• PRE: n 0 n0 = n

• POS: fat = n! fat > 0

• INV: fat > 0



Verificação de Programas

• Os erros são comuns em programação;

• O funcionamento correto de um programa depende também dos dados fornecidos ao programa, isto é, se sua variação foi corretamente prevista;

• Deseja-se verificar se o programa desenvolvido atende à especificação e corrigi-lo se for o caso.




• Exemplo (SILVA; FINGER; MELO, 2006, p.179-183): (Merge) dadas duas seqüências ordenadas de inteiros produzir nova sequência ordenada que entrelace os números das duas sequências:

• Entradas: V1 = {1,3,6,9} e

V2 = {2,3,3,7,10}

• Saída: V3 = {1,2,3,3,3,6,7,9,10}



Verificação de Programasvoid merge(int V1[],V2[],V3[],int t1,int t2)

{int p1=0,p2=0,p3=0;

while(t1+t2>0)

{if (V1[p1] > V2[p2])

{V3[p3]=V2[p2];

p2=p2+1; t2=t2-1;}

else {V3[p3]=V1[p1];

p1=p1+1; t1=t1-1;}

p3++;}

}




• Erro: se uma das sequências for vazia há uma comparação indevida:

if (v1[p1] > V2[p2])

• Numa execução real haveria erro.

• Para a correção ... Novo programa



Verificação de programasvoid merge(int V1[],V2[],V3[],int t1,int t2)

{int p1=0,p2=0,p3=0;

while(t1>0 && t2>0)

{if (V1[p1] > V2[p2])

{V3[p3]=V2[p2];

p2=p2+1; t2=t2-1;}


p1=p1+1; t1=t1-1;}

p3++;}

}



Verificação de programas

• Agora a comparação só ocorre se houver elementos nas listas;

• Porém, quando uma lista termina deixa-se de colocar os elementos restantes da outra lista na lista de saída.

• Um novo erro é introduzido ao se corrigir o erro inicial.

• Para a correção ... Novo programa



Verificação de Programasvoid merge(int V1[],V2[],V3[],int t1,int t2)

{int p1=0,p2=0,p3=0;

while(t1>0 && t2>0)

{if (V1[p1] > V2[p2])

{V3[p3]=V2[p2];

p2=p2+1; t2=t2-1;}


p1=p1+1; t1=t1-1;}

p3++;}

; (continua)



Verificação de Programaswhile (t1>0) {V3[p3]=V1[p1];

p1=p1+1; t1=t1-1;

p3++;}

while (t2>0) {V3[p3]=V2[p2];

p2=p2+1; t2=t2-1;

p3++;}

}

• O programa agora está OK.




• Se tantos erros ocorrem em um programa tão simples, como proceder no caso de sistemas complexos ?

• Como determinar se um programa está correto ?

• Solução: minimizar os erros, por meio de alguns procedimentos.




• Procedimentos utilizados para verificação:1. Inspeção: segue-se a lógica do programa

em busca de situações incorretas ou não previstas. Forma subjetiva de julgamento!

2. Teste de programas: alguns casos de teste são selecionados, em conjunto com dados de teste, sobre os quais o programa é executado e os resultados são verificados; não garante a correção total do programa.




• “Para garantir que um programa responda adequadamente aos dados do domínio, precisamos verificar se ele é, de fato, uma implementação particular da especificação do problema. Para isso, precisamos provar que o programa satisfaz a especificação do problema” (SILVA; FINGER; MELO, 2006, p. 183)




Estratégias para produzir programas corretos (SILVA; FINGER; MELO, 2006, p. 183):

1.Síntese: dada um especificação , um programa P é construído de forma automática ou semi-automática, por meio de transformação da especificação em P;– Se tal problema estivesse resolvido por

completo, não precisaríamos mais programar...




Estratégias para produzir programas corretos (SILVA; FINGER; MELO, 2006, p. 184):2. Verificação: Dada uma especificação e um programa P, mostrar que P é um modelo para (P satisfaz ).– “Vários desenvolvimentos têm sido realizados

nesta área, inclusive com aplicação na indústria”




Uso da verificação formal na prática (SILVA; FINGER; MELO, 2006, p. 185-186):

1) Análise: Dado um programa P, encontrar uma especificação que defina o problema para o qual P é a solução. – Usada para sistemas prontos– Permite corrigir e/ou documentar sistemas





2) Correção: Dada uma especificação e um programa P que NÃO satisfaz , construir P’ que satisfaça e seja próximo de P (considerando medida de proximidade – código, por exemplo).

– Usada quando se escreve programa que não satisfaz a especificação

– Usada quando os requisitos mudam





3) Otimização: Dada uma especificação e um programa P que satisfaz , obter P’ equivalente a P que seja ótimo sob determinada medida de complexidade.

– O novo programa P’ pode ser comparado tanto com P (equivalência) quanto com a especificação (satisfazibilidade)




• “Na verificação formal, faz-se necessária a comparação entre a especificação e o programa correspondente.”

• “Se a especificação for escrita em linguagem natural, não há como compará-la com o programa de forma matemática”

(SILVA; FINGER; MELO, 2006, p. 185-186)




• “Para que provemos que um programa satisfaz uma dada especificação, precisamos construir um sistema de provas, e não há como construir tal sistema baseado em linguagem natural pela falta de precisão e ambiguidades da sentenças na linguagem.”

(SILVA; FINGER; MELO, 2006, p. 185-186)25/05/09 Prof. Celso A A Kaestner 26



• “Portanto, para verificarmos programas, necessitamos de:

1)Uma especificação escrita em uma linguagem com fundamento matemático para que seja precisa e não ambígua

2)Um programa escrito em uma linguagem que tem o significado de seus comandos definido de forma precisa – semântica formal da linguagem de programação”





• “Portanto, para verificarmos programas, necessitamos de:

3) Uma forma de associar e comparar as asserções da especificação com os comandos do programa; as linguagens de especificação e programação devem, portanto, ser comparáveis

4) Um sistema de provas que usamos para mostrar que um programa satisfaz uma dada especifcação”





Exemplo de uma linguagem de programação (SILVA; FINGER; MELO, 2006, p. 186);

• Um programa sequencial é basicamente um transformador de dados do estado inicial ao estado final;

• Semântica operacional: indica o funcionamento de cada comando como transformador de estados;




• Semântica operacional (notação):

<C,> → ’

• A execução de C sobre o estado produz o estado ’;

• Exemplo: <x:=E, > → [m/x]




• Tripla de Hoare:

<> P <>

para todo estado que satisfaz , se a execução de P sobre termina produzindo um estado ’ que satisfaz ;

• Prova de programas: construir um sistema de provas para asserções do tipo

꜔ <> P <> ?




• Correção parcial: <> P <> é satisfeita sob correção parcial se para todos os estados que satisfazem o estado resultante da execução de P satisfaz , se P parar;

• Correção total: <> P <> é satisfeita sob correção total se para todos os estados que satisfazem o estado resultante da execução de P satisfaz e é garantido que P pára.




Correção parcial de programas (SILVA; FINGER;

MELO, 2006, p. 195);

Sistema de inferência com regras de Hoare para a linguagem de programação apresentada, sob a forma de uma lógica e suas regras de inferência (SILVA; FINGER; MELO,

2006, p. 196);

Exemplos de provas (SILVA; FINGER; MELO, 2006, p.

200-225).25/05/09 Prof. Celso A A Kaestner 33


Referências• SILVA, Flávio S. C. da; FINGER, M.;

MELO, Ana C. V. de. Lógica para Computação. São Paulo: Thomson Learning, 2006.

Documents

Lógica para Computação (IF61B) Lógica para Computação: Especificação e Verificação de Programas Prof. Celso Antônio Alves Kaestner, Dr. Eng. [email protected]