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]
Alterado e complementado por
Prof. Adolfo Neto, D.Sc.
[email protected]
Lógica para Computação (IF61B)
Especificação de programas
•
Uma tarefa típica em Computação:
problema real
•
•
Modelagem
problema computacional
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.
25/05/09
Prof. Celso A A Kaestner
2
Lógica para Computação (IF61B)
Especificação de programas
Visão operacional de um programa:
dados de
entrada
programa
dados de saída
Programas como transformadores de estados:
...
1 = {v11,v12...v1m}
25/05/09
 = {v21,v22...v2m}
Prof. Celso A A Kaestner
 = {vn1,vn2...vnm}
3
Lógica para Computação (IF61B)
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
25/05/09
Prof. Celso A A Kaestner
4
Lógica para Computação (IF61B)
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
25/05/09
Prof. Celso A A Kaestner
5
Lógica para Computação (IF61B)
Especificação de programas
•
Vantagens de se ter uma especificação
definida por formalismo matemático:
1.
2.
3.
4.
Precisão;
Verificação de consistência;
Simulação;
Verificação de programas.
•
Pode-se usar a Lógica Matemática como
linguagem de especificação (SILVA; FINGER;
MELO, 2006, p. 165);
25/05/09
Prof. Celso A A Kaestner
6
Lógica para Computação (IF61B)
Especificação de programas
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.
25/05/09
Prof. Celso A A Kaestner
7
Lógica para Computação (IF61B)
Especificação de programas
• 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
25/05/09
Prof. Celso A A Kaestner
8
Lógica para Computação (IF61B)
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.
25/05/09
Prof. Celso A A Kaestner
9
Lógica para Computação (IF61B)
Verificação de Programas
• 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}
25/05/09
Prof. Celso A A Kaestner
10
Lógica para Computação (IF61B)
Verificação de Programas
void 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++;}
}
25/05/09
Prof. Celso A A Kaestner
11
Lógica para Computação (IF61B)
Verificação de Programas
• 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
25/05/09
Prof. Celso A A Kaestner
12
Lógica para Computação (IF61B)
Verificação de programas
void 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;}
else {V3[p3]=V1[p1];
p1=p1+1; t1=t1-1;}
p3++;}
}
25/05/09
Prof. Celso A A Kaestner
13
Lógica para Computação (IF61B)
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
25/05/09
Prof. Celso A A Kaestner
14
Lógica para Computação (IF61B)
Verificação de Programas
void 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;}
else {V3[p3]=V1[p1];
p1=p1+1; t1=t1-1;}
p3++;}
; (continua)
25/05/09
Prof. Celso A A Kaestner
15
Lógica para Computação (IF61B)
Verificação de Programas
while (t1>0)
p1=p1+1;
p3++;}
while (t2>0)
p2=p2+1;
p3++;}
}
{V3[p3]=V1[p1];
t1=t1-1;
{V3[p3]=V2[p2];
t2=t2-1;
• O programa agora está OK.
25/05/09
Prof. Celso A A Kaestner
16
Lógica para Computação (IF61B)
Verificação de Programas
• 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.
25/05/09
Prof. Celso A A Kaestner
17
Lógica para Computação (IF61B)
Verificação de Programas
• 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.
25/05/09
Prof. Celso A A Kaestner
18
Lógica para Computação (IF61B)
Verificação de Programas
• “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)
25/05/09
Prof. Celso A A Kaestner
19
Lógica para Computação (IF61B)
Verificação de Programas
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 semiautomática, por meio de transformação da
especificação  em P;
– Se tal problema estivesse resolvido por
completo, não precisaríamos mais
programar...
25/05/09
Prof. Celso A A Kaestner
20
Lógica para Computação (IF61B)
Verificação de Programas
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”
25/05/09
Prof. Celso A A Kaestner
21
Lógica para Computação (IF61B)
Verificação de Programas
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
25/05/09
Prof. Celso A A Kaestner
22
Lógica para Computação (IF61B)
Verificação de Programas
Uso da verificação formal na prática (SILVA;
FINGER; MELO, 2006, p. 185-186):
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
25/05/09
Prof. Celso A A Kaestner
23
Lógica para Computação (IF61B)
Verificação de Programas
Uso da verificação formal na prática (SILVA;
FINGER; MELO, 2006, p. 185-186):
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)
25/05/09
Prof. Celso A A Kaestner
24
Lógica para Computação (IF61B)
Verificação de Programas
• “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)
25/05/09
Prof. Celso A A Kaestner
25
Lógica para Computação (IF61B)
Verificação de Programas
• “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
Lógica para Computação (IF61B)
Verificação de Programas
• “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”
(SILVA; FINGER; MELO, 2006, p. 185-186)
25/05/09
Prof. Celso A A Kaestner
27
Lógica para Computação (IF61B)
Verificação de Programas
• “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”
(SILVA; FINGER; MELO, 2006, p. 185-186)
25/05/09
Prof. Celso A A Kaestner
28
Lógica para Computação (IF61B)
Verificação de Programas
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;
25/05/09
Prof. Celso A A Kaestner
29
Lógica para Computação (IF61B)
Verificação de Programas
• Semântica operacional (notação):
<C,> → ’
• A execução de C sobre o estado  produz
o estado ’;
• Exemplo: <x:=E, > → [m/x]
25/05/09
Prof. Celso A A Kaestner
30
Lógica para Computação (IF61B)
Verificação de Programas
• 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 <> ?
25/05/09
Prof. Celso A A Kaestner
31
Lógica para Computação (IF61B)
Verificação de Programas
• 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.
25/05/09
Prof. Celso A A Kaestner
32
Lógica para Computação (IF61B)
Verificação de Programas
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
Lógica para Computação (IF61B)
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.