Projeto - Formalização da equivalência entre diferentes noções de permutação, e da correção do algoritmo bubblesort.
A proposta deste projeto é formalizar a equivalência entre duas noções distintas de permutação, e alternativamente, formalizar a correção do algoritmo bubblesort.
Objetivos:
- (20 pontos) Formalizar a equivalência entre as diferentes noções de permutação denominadas perm e equiv, OU
- (20 pontos) Formalizar a correção do algoritmo bubblesort, ou seja, enunciar e provar o teorema que estabelece que para qualquer lista
l
, o algoritmo bubblesort vai retornar uma permutação del
que está ordenada, E - (10 pontos) Escrever um relatório sobre o projeto.
Etapas do projeto:
- Formação dos grupos: O primeiro passo consiste na formação dos grupos. Cada grupo pode ter até 4 pessoas. Se preferir fazer o projeto sozinho, basta acessar o link e criar o seu grupo. Caso contrário, primeiro combine a formação do grupo com os colegas. Em seguida, apenas um participante do grupo clica no link acima e em seguida no botão "Create team". Uma vez criado o grupo, os outros participantes devem clicar no botão "Join" do grupo criado.
- Desenvolva as tarefas citadas nos objetivos acima da forma como achar mais adequado.
- (Opcional) Fundamentos de Git e GitHub: link
Prazo:
. Nesta data, o repositório de cada grupo deve conter 2 arquivos no ramo principal:- O arquivo
lc1_2022_1_projeto.v
contendo toda a formalização em Coq; - O arquivo
lc1-2022-1-relatorio.pdf
contendo o relatório do grupo.