Please enable JavaScript.
Coggle requires JavaScript to display documents.
Funções e estruturas indexadas - Coggle Diagram
Funções e estruturas indexadas
Tipos de função
Parcial +->Nem todo elemento da origem precisa estar ligado.
Total -->Todo elemento da origem tem exatamente um destino.
Injetora >+> >->Cada destino recebe no máximo uma origem.
Sobrejetora +->> -->>Todo destino é alcançado por alguém.
Bijetora >->>Total + injetora + sobrejetora: casamento perfeito.
Sequencias
São funções totais.
De 1..n para S — o índice é o domínio.
Operações básicas
size, ^ (concatenar), rev, first, last, front, tail.
Recortes
s /|\ n pega os n primeiros; s |/ n descarta os n primeiros.
Tipos especiais
seq1 não vazia · iseq sem repetição · perm permutação.
Arrays
A mesma coisa, do zero
Função total sobre um intervalo de inteiros começando em 0.
Um elemento
r(3) := e — lê e escreve como variável comum.
O array inteiro
r := (0..3) * {f} — produto cartesiano preenche tudo.
Vários de uma vez
Só com sobrescrita: r := r <+ {0|->e, 1|->f}.
Nas maquinas
reading · leitores e livros
reader +-> copy injetora: uma cópia não fica com dois leitores.
results · corrida
Chegada é iseq. Desclassificar = (fin /|\ p-1) ^ (fin |/ p).
hotel · quartos
room --> 0..6, com o limite dos quartos pequenos no invariante — não espalhado em if.
Atelier B e ProB
Atelier B prova a consistência; ProB anima com valores concretos.