Caso de Estudo: Insertion Sort

Um algoritmo de ordenação deve reorganizar os elementos de uma lista de modo a obter uma lista totalmente ordenada. Assim, o resultado da ordenação deve ser uma lista ordenada que seja uma permutação da lista original.

Neste caso de estudo analisamos um algoritmo bem conhecido — o Insertion Sort. Este algoritmo baseia-se na aplicação iterativa de uma função insert, que insere um elemento numa lista já ordenada. Por simplicidade, iremos considerar apenas listas de números inteiros.

Sessão Laboratorial

Carregue o arquivo insertionSort.v no Rocq Prover para correr os exemplos que a seguir de apresentam. Analise as respostas obtidas e resolva os exercícios propostos.

Numa lista ordenada cada dois elementos consecutivos são compatíveis com a relação ≤.

Podemos codificar isso definindo indutivamente o predicado Sorted.

Como sabemos, a lista produzida por um algoritmo de ordenação deve ser uma permutação da lista original. Para codificar a relação de permutação, em vez de uma definição indutiva, definiremos a relação utilizando uma função auxiliar que conta o número de ocorrências dos elementos.

Uma lista é uma permutação de outra quando contém exatamente o mesmo número de ocorrências de para cada elemento.

A relação de permutação é uma relação de equivalência.

Estas outras propriedades serão úteis.

Exercícios: Complete as provas em falta.

Começamos por definir a função insert que insere um elemento numa lista ordenada.

O insertion sort é definido aplicando iterativamente a função insert-

A correção deste algoritmo ficará demonstrada pela prova do seguinte teorema:

Para realizar esta prova vamos certamente precisar de lemas auxiliares… Façamos uma tentativa preliminar de prova.

Parece claro que serão úteis os seguintes lemas:

Para prová-los, os seguintes lemas sobre a função count podem também ser úteis.

Podemos agora terminar a prova de correção do insertion sort

Usando tipos Σ (specification types)

Uma abordagem alternativa consiste em usar tipos Σ (specification types) ao defeiir a função de ordenação. Isto forçará à prova de que o tipo Σ é habitado.

A função insort definida contém uma parte computacional (que diz como se ordena a lista de entrada) e um certiticado da sua correção (uma prova de que a lista produzida é um apermitação da lista de entrada e é ordenada).