O SISTEMA OPERA
Por: VictO SouzA • 6/10/2021 • Trabalho acadêmico • 791 Palavras (4 Páginas) • 100 Visualizações
/* BIBLIOTECA
* Author: Italo
* Creation date: 05/10/2021
*/
MACHINE
BIBLIOTECA (USUARIO, LIVRO, ANAIS, REVISTAS)
VARIABLES
usuarios, livros, anais, revistas, emprestimo, limite
INVARIANT
livros : POW(LIVRO) &
usuarios : POW(USUARIO) &
anais : POW(ANAIS) &
revistas : POW(REVISTAS) &
limite : NAT1 &
emprestimo : livros +-> usuarios
INITIALISATION
livros, anais, revistas, usuarios, emprestimo, limite := {}, {}, {}, {}, {}, 3
SETS
AVISO = {SUCESSO, FALHA}
OPERATIONS
resp <-- inserirUsuario (novo_usuario) =
PRE
novo_usuario : USUARIO &
novo_usuario /: usuarios
THEN
CHOICE
usuarios := usuarios \/ {novo_usuario} ||
resp := SUCESSO
OR
resp := FALHA
END
END;
resp <-- removerUsuario (novo_usuario) =
PRE
novo_usuario : USUARIO &
novo_usuario : usuarios
THEN
CHOICE
usuarios := usuarios - {novo_usuario} ||
resp := SUCESSO
OR
resp := FALHA
END
END;
resp <-- inserirLivro (novo_livro) =
PRE
novo_livro : LIVRO & novo_livro /: livros
THEN
CHOICE
livros := livros \/ {novo_livro} ||
resp := SUCESSO
...