Corretude

Universidade Estadual de Santa Cruz - UESC
Departamento de Ciˆncia Exatas e Tecnol´gicas - DCET e o
CET 640 - Fundamentos Matem´ticos para Ciˆncia da Computa¸ao a e c˜ Cap. III - Corretude de programas

Observa¸˜o: Este texto foi baseado no livro da Judith, fundamentos matem´ticos para ciˆncia da ca a e computa¸ao, e no livro do Cormen, Algoritmos. c˜ CAP´
ITULO III - Corretude de Programas
1

Introdu¸˜o ca Foi apresentado no cap´ ıtulo I alguns conceitos relacionados ` provas de implica¸oes (P → Q) e no a c˜ cap´ ıtulo II falou-se sobre indu¸ao matem´tica. c˜ a
O objetivo deste cap´ ıtulo ´ apresentar uma aplica¸˜o, no contexto da ciˆncia da computa¸˜o, dos e ca e ca temas abordados nos dois primeiros cap´ ıtulos. 1.1

Programas

Programas devem ser confi´veis e sem erros. a A verifica¸˜o de um programa tenta garantir que esse esteja correto. Um programa est´ correto ca a se ele se comporta de acordo com suas especifica¸˜es. Isso, n˜o indica que o programa resolve o co a problema, pois a especifica¸ao pode n˜o atender as necessidades do cliente. c˜ a
A valida¸˜o tenta garantir que o programa atenda as necessidades do cliente. N˜o ´ o foco desta ca a e disciplina. 2

Verifica¸˜o ca Pode ser abordada atrav´s de: e • Testes: tentam mostra que valores particulares de dados geram respostas aceit´veis. Podem a mostrar a existˆncia de erros, nunca a sua ausˆncia. e e
• Demonstra¸˜o de corre¸˜o: ´ uma abordagem mais matem´tica para ”provar” que um proca ca e a grama est´ correto. Essa demonstra¸ao usa t´cnicas de um sistema de l´gica formal na prova. a c˜ e o

2.1

Demonstra¸˜o de corre¸˜o ca ca

Conceitos preliminares
Seja:
• P um programa ou segmento de c´digo o qual ser´ verificado a corretude; o a
• E uma cole¸ao arbitr´ria e1 , e2 , · · · , en de valores de entrada para P . c˜ a
• D o dom´ ınio de E. Todas as poss´ ıveis configura¸oes de E. c˜ • S uma cole¸ao s1 , s2 , ·