Projeto e Análise de Algoritmos I

Aula 03 - Correção de Algoritmos e Invariantes

Lucas Nunes Alegre

Universidade Federal do Rio Grande do Sul
Instituto de Informática
Departamento de Informática Teórica


Estes slides utilizam conteúdo adaptado da bibliografia da disciplina e também de notas de aula e slides prévios dos professores Bruno Grisci, Rodrigo Machado e André Grahl.

Programa

  • Correção de Algoritmos
  • Problema da Ordenação de Vetores
  • Princípio da Invariante
  • Algoritmos Iterativos de Ordenação
  • Algoritmos Recursivos de Ordenação

Correção de Algoritmos

“

Uma demonstração de correção convincente será impossível enquanto o algoritmo seja visto como uma caixa preta, nossa única esperança é não considerar o algoritmo como uma caixa preta.

— Edsger W. Dijkstra
“Notes On Structured Programming”, 1970

Introdução

Def. Um algoritmo é qualquer procedimento computacional bem definido que recebe um conjunto de valores como entrada e produz um conjunto de valores como saída.

Obs. Um algoritmo pode ser visto como uma ferramenta para resolver um problema.

Def. Um algoritmo resolve um problema se para toda entrada:
- Ele pára.
- Retorna a saída correta.


P. Um algoritmo que não pára é útil? Um algoritmo incorreto é útil?

Problemas e Instâncias

Problema. Especificação abstrata e genérica da relação entre um conjunto de entradas válidas e as saídas desejadas.

Instância. Um caso concreto ou entrada específica (com dados fixos) que satisfaz as restrições do problema.

Exemplo de Problema:
Ordenação de Vetores

  • Entrada: Sequência de n números \langle a_1, a_2, \dots, a_n \rangle.
  • Objetivo: Permutação \langle a_1', a_2', \dots, a_n' \rangle tal que a_1' \le a_2' \le \dots \le a_n'.

Exemplo de Instância:
Uma entrada específica

  • Entrada: \langle 31, 41, 59, 26, 41, 58 \rangle
  • Solução: \langle 26, 31, 41, 41, 58, 59 \rangle

Obs. Um algoritmo correto deve produzir a solução esperada para todas as instâncias possíveis do problema.

Correção de Algoritmos

  • Como discutido, um algoritmo é uma sequência de passos para a resolução de um problema ou cálculo de uma quantidade.
  • Um algoritmo está correto quando a sua respectiva saída corresponde à solução ou quantidade esperada para todas as possíveis entradas.
  • Exemplo de algoritmo (incorreto) para calcular números primos f(n) = n^2 + n + 41 (gera números primos somente enquanto n < 40)
  • Antes de pensarmos no custo do algoritmo, é importante confirmar que ele realmente resolve o problema!

Testando a Correção de Algoritmos

  • Determinar a correção de algoritmos/programas pode depender muito da descrição do mesmo e de seu estilo.
  • Uma primeira forma de aferir correção é testar o algoritmo para diversas entradas.
  • Contudo, testes podem aferir a presença de erros, mas não a ausência dos mesmos (a menos que cubram todas as possíveis entradas - o que normalmente é impossível por questão de infinitude)
  • Dessa forma, provas de correção são necessárias para garantir que algoritmos estejam corretos em relação ao problema que visam resolver.

Provando a Correção de Algoritmos

Algumas técnicas importantes para provar a correção de algoritmos:

  • Manipulação de identidades matemáticas e algébricas
  • Técnicas de dedução da lógica formal (dedução direta, redução ao absurdo, contraposição, etc.)
  • Técnicas envolvendo recursão e indução matemática
  • Determinação de pré-condições, pós-condições, e aferição de invariantes de laços

Além da resposta do algoritmo estar correta, é também necessário estipular a garantia de terminação do algoritmo (i.e. variantes para laços)

Correção dos Algoritmos Vistos Previamente

Problema do Troco (Greedy Cashier’s Algorithm):

  • Correção baseada em propriedades matemáticas do conjunto de moedas usados para fornecer o troco.

Emparelhamento Estável (Gale-Shapley):

  • Correção baseada em um raciocínio por contradição (se a resposta do algoritmo não for um emparelhamento estável, é possível deduzir uma contradição lógica)

Problema da Ordenação de Vetores

Ordenação de Vetores

Entrada. Uma sequência de k números \langle a_1,a_2, \dots, a_k \rangle.


Objetivo. Encontrar uma permutação \langle a_1',a_2', \dots, a_k' \rangle em que a_1' \leq a_2' \leq \dots \leq a_k'.


Instância: \langle 31,41,59,26,41,58 \rangle

  • Satisfaz todas as restrições impostas pela definição do problema.


Solução. \langle 26, 31, 41, 41, 58, 59 \rangle.

Algoritmos Iterativos de Ordenação

Ordenação por Inserção

Funciona da forma que um humano organiza uma mão jogando cartas:

  • Inicia com a mão da esquerda vazia e com as cartas viradas para baixo na mesa.
  • Remove uma carta de cada vez e insere na posição correta na mão esquerda.
  • Para encontrar a posição correta da carta, compara com as cartas que já estão na mão esquerda.
  • Invariante: Em todo momento todas as cartas na mão esquerda estão ordenadas.

Ordenação por Inserção (InsertionSort)

\begin{algorithmic} \Procedure{InsertionSort}{$A$} \State $n \gets \text{length}(A)$ \For{$j \gets 2$ \To $n$} \State $\text{key} \gets A[j]$ \State $i \gets j - 1$ \While{$i > 0$ \textbf{ and } $A[i] > \text{key}$} \State $A[i + 1] \gets A[i]$ \State $i \gets i - 1$ \EndWhile \State $A[i+1] \gets \text{key}$ \EndFor \EndProcedure \end{algorithmic}

Obs. Nos pseudocódigos de todos os algoritmos desta aula, assumimos indexação de 1 a n (para vetores de tamanho n).

Princípio da Invariante

Corretude

Def. Uma execução de um algoritmo é uma sequência de estados com a propriedade de que:

  • Tem um estado inicial; e
  • Se q e r são estados consecutivos na sequência, então q \longrightarrow r.

Def. Um estado é alcançável se aparece em alguma execução.

Def. Uma invariante é uma propriedade \textcolor{#2e7d32}{P} para estados:

  • Tal que se \textcolor{#2e7d32}{P}(q), o estado q possui a propriedade \textcolor{#2e7d32}{P}; e
  • q \longrightarrow r; então
  • \textcolor{#2e7d32}{P}(r), o estado r possui a propriedade \textcolor{#2e7d32}{P}.

Princípio da Invariante

Def. Uma invariante é uma propriedade \textcolor{#2e7d32}{P} para estados:

  • Tal que se \textcolor{#2e7d32}{P}(q), o estado q possui a propriedade \textcolor{#2e7d32}{P}; e
  • q \longrightarrow r; então
  • \textcolor{#2e7d32}{P}(r), o estado r possui a propriedade \textcolor{#2e7d32}{P}.

Princípio da Invariante. Se o estado inicial possui a invariante, então todos os estados alcançáveis possuem a invariante.

Princípio da Invariante


Item 1. Define a propriedade.

Item 2. Prova que a propriedade se mantém para q \longrightarrow r.

Item 3. Prova que a propriedade se mantém para qualquer estado alcançável.

  • Prova por indução.
  • Caso Base.
  • Passo de Indução.
  • Assume P(n) prova P(n+1).

Item 4. Prova que o algoritmo termina.

Item 5. Conclui que o algoritmo resolve o problema.

Busca Linear - Invariante

\begin{algorithmic} \Procedure{Busca-Linear}{$A, n, x$} \For{$i \gets 1$ \To $n$} \If{$A[i] = x$} \Return $i$ \EndIf \EndFor \Return \textsc{Não-Encontrado} \EndProcedure \end{algorithmic}

Invariante do Laço. No início de cada iteração do laço For, se x está presente no vetor A, então x está presente no subvetor A[i \dots n].

Terminação e Corretude.

  • Se A[i] = x: O algoritmo retorna o índice i imediatamente (correto).
  • Se i = n + 1 (fim do laço): Considere a contrapositiva do invariante:
  • \text{“Se } x \text{ não está em } A[i \dots n] \implies x \text{ não está em } A\text{”}
  • Para i = n + 1, o subvetor A[n+1 \dots n] é vazio.
  • Como x não pode estar em um subvetor vazio \implies x não está em A.
  • Logo, retornar Não-Encontrado está correto. \blacksquare

Invariantes: Algoritmos de Ordenação Iterativos

Corretude: InsertionSort


Def. Ordenado(q): A subsequência representada pelo estado q de j-1 números \langle a_1', a_2', \dots, a_{j-1}'\rangle obedece a restrição de que a_1' \leq a_2' \leq \dots \leq a_{j-1}'.

Lema 1. Para qualquer transição q \longrightarrow r do algoritmo de Ordenação por Inserção, se Ordenado(q) então Ordenado(r).

Prova. A demonstração do lema segue da construção do loop while.

Durante a execução do loop, o algoritmo move para a direita A[j - 1], A[j - 2], A[j - 3], e assim por diante, até que a posição correta de key é encontrada.

Nesse ponto key é colocada na posição correta e a subsequência está ordenada.

\blacksquare

InsertionSort: Terminação


Lema 2. O algoritmo de Ordenação por Inserção termina.

Prova. O loop externo termina quando j > n, isso ocorre quando j > A.length e j é apenas incrementado durante o algoritmo.

\blacksquare

Corolário. O algoritmo de Ordenação por Inserção resolve o problema de ordenação.

Prova. Pelo Lema 2, sabemos que o algoritmo termina depois de n iterações. Pelo Lema 1 sabemos que toda subsequência alcançada pelo algoritmo está ordenada, como na iteração n+1 a subsequência corresponde a todo o vetor, então podemos concluir que o algoritmo resolve o problema.

\blacksquare

Princípio da Invariante


Item 1. Define a propriedade.

Item 2. Prova que a propriedade se mantém para q \longrightarrow r.

Item 3. Prova que a propriedade se mantém para qualquer estado alcançável.

  • Prova por indução.
  • Caso Base.
  • Passo de Indução.
  • Assume P(n) prova P(n+1).

Item 4. Prova que o algoritmo termina.

Item 5. Conclui que o algoritmo resolve o problema.

Princípio da Invariante: Criador

  • Formulado por Robert W. Floyd na Carnegie-Mellon University em 1967.
  • Jovem prodígio que nunca concluiu o doutorado.
  • Princípio simples e amplamente aplicável.
  • Professor em Stanford e Prêmio Turing em 1978.
  • Robert W Floyd, por Donald E. Knuth: http://oldwww.acm.org/pubs/membernet/stories/floyd.pdf.

Exercício 1: Soma dos Elementos

Qual é o invariante do laço no algoritmo a seguir?

\begin{algorithmic} \Procedure{Soma}{$A, n$} \State $s \gets 0$ \For{$i \gets 1$ \To $n$} \State $s \gets s + A[i]$ \EndFor \Return $s$ \EndProcedure \end{algorithmic}

Exercício. Determine a propriedade invariante do laço For e o argumento de terminação.

Exercício 1: Solução

Solução.

  • Invariante do laço: No início de cada iteração i (1 \le i \le n+1), a variável s contém a soma dos elementos da subsequência A[1 \dots i-1]: s = \sum_{k=1}^{i-1} A[k]
    • Base (i=1): s = 0 (soma de conjunto vazio).
    • Passo (i \to i+1): adiciona-se A[i] a s, mantendo s = \sum_{k=1}^{i} A[k].
  • Terminação: O laço termina quando i = n+1. Pelo invariante, s = \sum_{k=1}^{n} A[k], ou seja, a soma de todo o vetor A. \blacksquare

Exercício 2: Maior Elemento

Qual é o invariante do laço no algoritmo a seguir?

\begin{algorithmic} \Procedure{MaiorElemento}{$A, n$} \State $m \gets A[1]$ \For{$i \gets 2$ \To $n$} \If{$A[i] > m$} \State $m \gets A[i]$ \EndIf \EndFor \Return $m$ \EndProcedure \end{algorithmic}

Exercício. Determine a propriedade invariante do laço For e o argumento de terminação.

Exercício 2: Solução

Solução.

  • Invariante do laço: No início de cada iteração i (2 \le i \le n+1), a variável m armazena o maior valor presente no subvetor A[1 \dots i-1]: m = \max(A[1 \dots i-1])
    • Base (i=2): m = A[1] = \max(A[1 \dots 1]).
    • Passo (i \to i+1): se A[i] > m, m é atualizado para A[i], mantendo m = \max(A[1 \dots i]).
  • Terminação: O laço termina quando i = n+1. Pelo invariante, m = \max(A[1 \dots n]), garantindo que m é o maior elemento de todo o vetor A. \blacksquare

Ordenação por Seleção (SelectionSort)

\begin{algorithmic} \Procedure{SelectionSort}{$A$} \State $n \gets \text{length}(A)$ \For{$i \gets 1$ \To $n$} \State $m \gets i$ \For{$j \gets i$ \To $n$} \If{$A[j] < A[m]$} \State $m \gets j$ \EndIf \EndFor \State $\text{Swap}(A, i, m)$ \EndFor \EndProcedure \end{algorithmic}
\begin{algorithmic} \Procedure{Swap}{$A, x, y$} \State $tmp \gets A[x]$ \State $A[x] \gets A[y]$ \State $A[y] \gets tmp$ \EndProcedure \end{algorithmic}

SelectionSort: Correção e Terminação

Qual a intuição por trás da construção do SelectionSort?


Determine:

  1. O invariante do corpo do laço
  2. O respectivo argumento de terminação

SelectionSort: Correção e Terminação (Resolução)

  • Invariante do laço: No início de cada iteração i (do laço externo), o subvetor A[1 \dots i-1] contém os i-1 menores elementos do vetor original, e encontra-se ordenado.
  • Terminação: O laço externo termina após i = n. Neste ponto, o subvetor A[1 \dots n] conterá os n menores elementos, significando que logo todo o vetor A está ordenado. \blacksquare

BubbleSort

\begin{algorithmic} \Procedure{BubbleSort}{$A$} \State $n \gets \text{length}(A)$ \For{$i \gets 1$ \To $n-1$} \For{$j \gets 1$ \To $n-i$} \If{$A[j] > A[j+1]$} \State $\text{Swap}(A, j, j+1)$ \EndIf \EndFor \EndFor \EndProcedure \end{algorithmic}

BubbleSort: Correção e Terminação

Qual a intuição por trás da construção do BubbleSort?


Determine:

  1. O invariante do corpo do laço
  2. O respectivo argumento de terminação

BubbleSort: Correção e Terminação (Resolução)

  • Invariante do laço: No início da iteração i do laço externo (1 \le i \le n-1), os i-1 maiores elementos do vetor original já estão em suas posições finais, ocupando exatamente as posições A[n-(i-1)+1], A[n-(i-1)+2], \dots, A[n], isto é, o subvetor A[n-i+2 \dots n], e esses elementos estão ordenados.

  • Terminação: O laço externo executa para i=1,2,\dots,n-1. Quando ele termina, os n-1 maiores elementos estão em suas posições finais (A[2],\dots,A[n]). O único elemento restante ocupa A[1], portanto todo o vetor A está ordenado. \blacksquare

Algoritmos Recursivos de Ordenação

MergeSort

  • MergeSort é um dos mais famosos e eficientes algoritmos de ordenação baseado em comparações.


  • A sua ideia fundamental é uma rotina que une duas listas ordenadas em uma lista maior ordenada (merge).


  • O algoritmo divide a entrada ao meio até chegar ao caso base (vetor de tamanho 1 – trivialmente ordenado), e após recombina os vetores ordenados.

MergeSort: Ideia Principal

\begin{algorithmic} \Procedure{MergeSort}{$A$} \If{$\text{length}(A) < 2$} \Return $A$ \Else \State $r_1 \gets \text{MergeSort}(\text{FirstHalf}(A))$ \State $r_2 \gets \text{MergeSort}(\text{SecondHalf}(A))$ \Return $\text{Merge}(r_1, r_2)$ \EndIf \EndProcedure \end{algorithmic}


  • No pseudocódigo acima, as rotinas \text{FirstHalf} e \text{SecondHalf} extraem a primeira e segunda metade do vetor, respectivamente, e \text{Merge} une dois vetores ordenados em um único vetor ordenado.


  • Implementações eficientes de MergeSort requerem o uso de um vetor auxiliar e manipulação de índices (para que os cortes tenham custo constante).

MergeSort: Main (Eficiente)

\begin{algorithmic} \Procedure{MergeSort}{$A, \textit{start}, \textit{end}$} \If{$\textit{start} < \textit{end}$} \State $\textit{mid} \gets \lfloor (\textit{start} + \textit{end}) / 2 \rfloor$ \State $\text{MergeSort}(A, \textit{start}, \textit{mid})$ \State $\text{MergeSort}(A, \textit{mid}+1, \textit{end})$ \State $\text{Merge}(A, \textit{start}, \textit{mid}, \textit{end})$ \EndIf \EndProcedure \end{algorithmic}


Obs. \textit{start} e \textit{end} representam os índices de início e fim da parte do vetor a ser ordenado. Para ordenar o vetor inteiro, chame \text{MergeSort}(A, 1, \text{length}(A)).

MergeSort: Merge (Eficiente)

\begin{algorithmic} \Procedure{Merge}{$A, \textit{start}, \textit{mid}, \textit{end}$} \For{$i \gets \textit{start}$ \To $\textit{end}$} \State $\textit{Aux}[i] \gets A[i]$ \EndFor \State $i \gets \textit{start}$ \State $j \gets \textit{mid}+1$ \State $k \gets \textit{start}$ \While{$i \leq \textit{mid}$ \textbf{ and } $j \leq \textit{end}$} \If{$\textit{Aux}[i] < \textit{Aux}[j]$} \State $A[k] \gets \textit{Aux}[i]$ \State $i \gets i+1$ \Else \State $A[k] \gets \textit{Aux}[j]$ \State $j \gets j+1$ \EndIf \State $k \gets k+1$ \EndWhile \While{$i \leq \textit{mid}$} \State $A[k] \gets \textit{Aux}[i]$ \State $i \gets i+1$ \State $k \gets k+1$ \EndWhile \While{$j \leq \textit{end}$} \State $A[k] \gets \textit{Aux}[j]$ \State $j \gets j+1$ \State $k \gets k+1$ \EndWhile \EndProcedure \end{algorithmic}
  • Há um vetor auxiliar \textit{Aux} que recebe a porção do vetor a ser ordenada (linhas 1-2), contendo os dois subvetores já ordenados (de \textit{start} a \textit{mid}, e de \textit{mid}+1 a \textit{end})
  • i aponta para o início do primeiro subvetor ordenado em \textit{Aux} (inicia com \textit{start})
  • j aponta para o início do segundo subvetor ordenado em \textit{Aux} (inicia com \textit{mid}+1)
  • k aponta para a posição onde os elementos dos dois subvetores serão inseridos em A (inicia com \textit{start})
  • o laço das linhas 6-12 compara o menor de cada subvetor, inserindo na posição correta do vetor de saída (e atualizando os índices)
  • o laço das linhas 13-16 e 17-20 copiam os elementos de um dos subvetores quando o outro subvetor já terminou.

MergeSort: Correção e Terminação

Para determinar a correção do MergeSort utilizamos indução estrutural em sequências de números.

  • determinar que o algoritmo é correto para os casos-base (onde a recursão não é chamada)
  • assumindo que chamadas do algoritmo sobre sequências menores que a atual provêm a resposta correta, provar que a saída calculada para a sequência atual é correta.

QuickSort

QuickSort é outro algoritmo famoso e bastante utilizado.


  • Pivô: escolha de um elemento arbitrário da sequência.
  • Particionamento: formação de dois subvetores (elementos \le pivô e elementos > pivô).
  • Recursão: ordenação recursiva dos subvetores utilizando o próprio algoritmo.
  • Desempenho: caso médio similar ao MergeSort; pior caso com custo O(n^2).
  • Espaço: não requer alocação de memória adicional.

QuickSort: Ideia Principal

\begin{algorithmic} \Procedure{QuickSort}{$A$} \If{$\text{length}(A) < 2$} \Return $A$ \Else \State $p \gets \text{ExtraiPivo}(A)$ \State $m_1 \gets \text{QuickSort}(\text{MenoresOuIguais}(A, p))$ \State $m_2 \gets \text{QuickSort}(\text{Maiores}(A, p))$ \Return $m_1 \mathbin{+\!\!+} \langle p \rangle \mathbin{+\!\!+} m_2$ \EndIf \EndProcedure \end{algorithmic}
  • No pseudocódigo acima, a operação +\!\!+ significa concatenação de vetores e \langle p \rangle um vetor unitário contendo p.


  • Similarmente ao MergeSort, implementações eficientes de QuickSort requerem a minimização da movimentação de dados por meio do uso de índices e reaproveitamento do espaço do próprio vetor sendo ordenado.

QuickSort: Main (Eficiente)

\begin{algorithmic} \Procedure{QuickSort}{$A, \textit{start}, \textit{end}$} \If{$\textit{start} < \textit{end}$} \State $p \gets \text{Partition}(A, \textit{start}, \textit{end})$ \State $\text{QuickSort}(A, \textit{start}, p-1)$ \State $\text{QuickSort}(A, p+1, \textit{end})$ \EndIf \EndProcedure \end{algorithmic}

Obs. A rotina \text{Partition} executa ao mesmo tempo a extração do pivô e o particionamento dos demais valores, devolvendo o índice p do pivô. Os elementos anteriores a p são menores que o pivô, e os posteriores a p, maiores. Para ordenar todo o vetor, a chamada inicial é \text{QuickSort}(A, 1, \text{length}(A)).

QuickSort: Partition (Eficiente)



\begin{algorithmic} \Procedure{Partition}{$A, \textit{start}, \textit{end}$} \State $x \gets A[\textit{end}]$ \State $i \gets \textit{start} - 1$ \For{$j \gets \textit{start}$ \To $\textit{end}-1$} \If{$A[j] \leq x$} \State $i \gets i + 1$ \State $\text{Swap}(A, i, j)$ \EndIf \EndFor \State $\text{Swap}(A, i+1, \textit{end})$ \Return $i+1$ \EndProcedure \end{algorithmic}
  • x é o pivô (aqui extraído da última posição)
  • i é o índice do último valor menor ou igual a x
  • o laço 3-6 faz j percorrer todo vetor do início ao fim (excluindo \textit{end}). Se encontra um valor menor ou igual a x, o joga para o início por meio de uma troca e ajusta o índice i
  • ao final, faz uma troca para posicionar o pivô após i e devolve o seu índice

QuickSort: Correção e Terminação

Tal qual no caso do MergeSort, utilizamos indução para demonstrar a correção do QuickSort.


Determine:

  1. Argumentos para a correção do QuickSort
  2. Argumentos para a terminação do QuickSort

Ordenação em Python

Implementação em Python

Ferramentas de Verificação

Ferramentas de Verificação

A verificação formal de software utiliza invariantes de laço, pré/pós-condições e Lógica de Hoare para provar matematicamente que programas atendem a suas especificações:

  • Dafny: Linguagem desenvolvida pela Microsoft Research voltada para verificação formal. Exige anotações de invariantes (invariant) e pré/pós-condições (requires/ensures), provando a corretude de algoritmos automaticamente via Z3.
  • Frama-C / ACSL: Plataforma para análise e verificação formal de programas C. Utiliza anotações ACSL (loop invariant) para comprovação matemática de propriedades e ausência de bugs.
  • SPARK / Ada: Conjunto de ferramentas de verificação para Ada, utilizado em sistemas críticos (aeroespacial, ferroviário e médico) para provar matematicamente a corretude usando invariantes.
  • KeY: Sistema de verificação dedutiva para Java que provê verificação baseada em invariantes especificados em JML (Java Modeling Language).
  • CBMC: Bounded Model Checker para C/C++ que analisa e verifica automaticamente invariantes de laço, asserções e segurança de memória.

?