Lógica para Computação
Prof. Celso Antônio Alves Kaestner, Dr. Eng.
celsokaestner (at) utfpr (dot) edu (dot) br
Lógica para Computação (IF61B)
Especificação de programas

Engenharia de Requisitos: como entender e
modelar um problema real para obter uma
solução computacional;

Engenharia de Software: é uma área da
Computação voltada à especificação,
desenvolvimento e manutenção de sistemas
de software, com aplicação de tecnologias
e práticas de gerência de projetos e outras
disciplinas, visando organização,
produtividade e qualidade.
2
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Especificação de programas

Uma tarefa típica em Computação:
problema
real
problema
Modelagem
computacional
3
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Especificação de programas

Especificações em linguagem natural exigem
que se assuma o significado de diversos
termos, e por isto são “imprecisas / vagos /
inconsistentes” permitindo diversas
interpretações;

Este é um problema amplamente estudado
em Engenharia de Software, que busca de
métodos e formalismos tenta eliminar /
reduzir este problema.
4
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Especificação de programas
Visão operacional de um programa:
dados de
programa
dados de
entrada
saída
Programas como transformadores de estados:
1 = {v11,v12...v1m}
 = {v21,v22...v2m}
 = {vn1,vn2...vnm}
...
5
Prof. Celso A A Kaestner
05/11/2015
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
6
Prof. Celso A A Kaestner
05/11/2015
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 2 (superespecificação):

sobre o estado inicial: x  10  y  10  (x + y)  0

sobre o estado final: z = x + y  z  20
7
Prof. Celso A A Kaestner
05/11/2015
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 3 (especificação pouco clara):

sobre o estado inicial: x  10  (x + y)  (10 + x)

sobre o estado final: z = x + y
8
Prof. Celso A A Kaestner
05/11/2015
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 4 (especificação incompleta):

sobre o estado inicial: x  10

sobre o estado final: z = x + y
9
Prof. Celso A A Kaestner
05/11/2015
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” 5 (não é especificação ...):

sobre o estado inicial: x  10  y  10

sobre o estado final: z = x + y  z < 10
10
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Especificação de programas

1.
2.
Vantagens de se ter uma especificação definida
por formalismo matemático:
Precisão: a linguagem matemática é precisa e
identifica um significado único para cada
propriedade;
Verificação de consistência: a linguagem
matemática nos possibilita verificar
inconsistências nas especificações quando há
propriedades contraditórias sobre um mesmo
objeto;
11
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Especificação de programas
3.
Simulação: especificações em algumas
linguagens matemáticas podem ser
parcialmente executáveis, auxiliando a
verificação;
4.
Verificação de programas: após a construção de
um programa é possível – de forma automática
ou semiautomática – verificar se esta é uma
solução (ou satisfaz) a especificação do
problema.
12
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Especificação de programas

Pode-se usar o Lógica Matemática como
linguagem de especificação;

Ver na referência (da Silva, Finger, de Melo) às
páginas 165 a 169 o uso da Lógica Matemática
como linguagem de especificação.
13
Prof. Celso A A Kaestner
05/11/2015
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.
14
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Especificação de programas

Exemplo: fatorial.
1
se
n=0
n! = 1
se
n=1
n*(n-1)!
se

PRE: n  0

POS: fat = n!  fat > 0

INV:
n>1
fat > 0
15
Prof. Celso A A Kaestner
05/11/2015
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.
16
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Verificação de programas

Exemplo: (Merge) dadas duas seqüências
ordenadas de inteiros produzir nova seqüência
ordenada que entrelace os números das duas
seqüências:

Entradas:
V1 = {1,3,6,9} e
V2 = {2,3,3,7,10}

Saída:
V3 = {1,2,3,3,6,7,9,10}
17
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Verificação de programas
void merge(int V1[],V2[],V3[],t1,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++;}
}
18
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Verificação de programas

Erro: se uma das seqüê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
19
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Verificação de programas
void merge(int V1[],V2[],V3[],t1,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++;}
}
20
Prof. Celso A A Kaestner
05/11/2015
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
21
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Verificação de programas
void merge(int V1[],V2[],V3[],t1,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)
22
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Verificação de programas
while (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.
23
Prof. Celso A A Kaestner
05/11/2015
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.
24
Prof. Celso A A Kaestner
05/11/2015
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;
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
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Verificação de programas
 Estratégias para produzir programas corretos
(pg. 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;
2. Verificação: Dada uma especificação  e um
programa P, mostrar que P é um modelo para
 (P satisfaz ).
26
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Verificação de programas
Uso da verificação formal na prática:
1) Análise: Dado um programa P, encontrar uma
especificação  que defina o problema para o qual
P é a solução;
2) Correção: Dados uma especificação  e um
programa P que não satisfaz , construir P’ que
satisfaça  e que seja “próximo” a P;
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.
27
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Verificação de programas
 Exemplo
de uma linguagem de
programação (pg. 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;
28
Prof. Celso A A Kaestner
05/11/2015
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]
29
Prof. Celso A A Kaestner
05/11/2015
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 <> ?
30
Prof. Celso A A Kaestner
05/11/2015
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.
31
Prof. Celso A A Kaestner
05/11/2015
Lógica para Computação (IF61B)
Verificação de programas
 Correção
parcial de programas (pg. 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 (pg. 196);
 Exemplos
de provas (pg. 200 em diante).
32
Prof. Celso A A Kaestner
05/11/2015