Sistemas multimidias

Especificação Formal em Z de um IPOD
Universidade do Estado do Rio Grande do Norte
Daiane Saíze de Araújo C. Soares
Ronaldo Vagner Araujo Fernandes
José Salustiano Filho

Introdução
Este trabalho apresenta a documentação da especificação funcional básica de um
IPOD através do formalismo Z, bem como algumas tarefas básicas que o usuário pode realizar com o aparelho. Como por exemplo, incluir e excluir uma agenda; incluir e excluir uma coleção, incluir e excluir uma mídia, enfim funções simples e características de um
IPOD, mas antes veremos uma breve descrição do formalismo Z.

Formalismo Z
Z é uma linguagem formal cujo objetivo é a especificação de sistemas. Por ser uma linguagem formal ela possui: um alfabeto, uma sintaxe e uma semântica precisa.
Uma especificação em Z consiste de um modelo matemático do estado do sistema e da definição de operações sobre o estado, descrevendo, também, certas operações correspondentes dessa estrutura. Essas operações correspondem às interações do sistema com o meio externo. Quando operações são aplicadas a componentes da estrutura lógica, o estado do sistema se altera, refletindo o efeito da interação do novo estado assumido pelo sistema. A notação pode ser usada também para descrever propriedades desejáveis, que os estado do sistema devem satisfazer. Isso permite que certas propriedades de sistemas especificados na notação Z possam ser validadas de maneira simbólica, usando apenas o texto das especificações sem necessidade de testes sobre algum código compilado
[MOU01].
Uma especificação em Z é formada de um número de esquemas (diagramas), os quais possuem uma parte declarativa e uma parte de predicados em lógica de 1ª ordem.
Estes esquemas podem ser combinados e usados em outros esquemas.
A especificação de um IPOD pode ser bem mais complexa lavando em consideração as novas tecnologias inclusas em novos IPODs, como é o caso do IPOD TOUCH, mais aqui tratamos apenas de especificar ações simples de IPODS anteriores.
Mostraremos a