Corretude de Algoritmos
,
Parte 1: Provar que a propriedade é válida para
.
Parte 2: Provar que se a propriedade é válida para
, então a propriedade
é válida para
Seja
Vamos assumir que
(hipótese da indução).
Temos que provar que:
(pela hipótese da indução)
Uma árvore binária completa com
níveis tem exatamente
nós.
Parte 1: Para
, a propriedade é válida pois a árvore binária completa
com um único nível possui um único nó.
Parte 2: Assumindo que uma árvore binária completa com
níveis possui
nós (hipótese da indução), temos que provar que uma árvore
binária completa com
níveis possui
nós.
Uma árvore binária completa com
níveis é formada por um nó
raiz e duas sub-árvores com
níveis. Logo, pela hipótese da indução,
o número total de nós é
Considere um tabuleiro formado por quadrados de um mesmo
tamanho (como no tabuleiro de xadrez). O tabuleiro tem
quadrados
em cada linha e
quadrados em cada coluna.
é potência de
.
Um dos quadrados é considerado especial, sendo diferenciado dos
demais. Uma L-peça é semelhante a um tabuleiro
,
removendo-se um dos quadrados. É possível cobrir o tabuleiro usando
L-peças, considerando que cada quadrado só é coberto uma
única vez, com exceção do quadrado especial que não é coberto por
nenhuma L-peça?
O problema do quebra-cabeça do tabuleiro é sempre resolvível. A prova
utiliza indução matemática sobre o inteiro
, onde
.
Parte 1: Caso base quando
(tabuleiro
) ou
(tabuleiro
).
Parte 2: Vamos considerar qualquer
. A hipótese da indução é
que o problema é resolvível para
, ou seja, o tabuleiro
. Dividindo-se o tabuleiro
em
4 partes iguais, o quadrado especial vai ficar em um dos 4
sub-tabuleiros. Colocar uma L-peça no meio do tabuleiro original,
de modo a ficar um quadrado especial em cada um dos sub-tabuleiros.
O problema se reduziu a 4 sub-tabuleiros
,
cada um com um quadrado especial. Pela nossa hipótese da indução,
cada um dos sub-tabuleiros pode ser resolvido. Logo, o tabuleiro
original pode ser resolvido considerando uma L-peça no meio.
,
, e
,
.
Algoritmo:
Provar que
,
retorna
.
Caso base: Para
,
retorna
ou
, como pretendido.
Para
,
retorna
ou
, como pretendido.
Hipótese da indução:
e
,
retorna
.
O que temos que provar:
retorna
.
retorna
.
(pela hipótese da indução)
.
Algoritmo:
Provar que
,
retorna
.
Caso base: Para
,
retorna
, como pretendido.
Hipótese da indução:
e
retorna
.
O que temos que provar:
retorna
.
retorna
.
(pela hipótese da indução)
.
Considerar algoritmos com um laço.
O valor do identificador
imediatamente após a
-ésima
interação em um laço é denotada por
(
indica o valor imediatamente
antes de iniciar a primeira interação). Por exemplo,
denota o valor
do identificador
após a sexta ocorrência do laço.
,
, e
,
.
Algoritmo:
Provar que
,
retorna
.
Fatos sobre o algoritmo:
Invariante de Laço:
Para todos os números naturais,
,
,
,
e
.
A prova é por indução sobre
. O caso base,
, é trivial, uma vez
que
,
, e
.
Hipótese da indução:
,
,
e
.
O que temos que provar:
,
e
.
(pela hipótese da indução)
.
(pela hipótese da indução)
(pela hipótese da indução)
.
Prova de Corretude:
Provar que o algoritmo termina com
contendo
.
Para
está OK. Se
, então nós entramos no laço.
Uma vez que
, eventualmente
será igual a
e o laço vai terminar. Vamos supor que isto acontece depois de
interações. Uma vez que
e
, podemos concluir
que
.
Pelo invariante de laço,
.