Apresentação - Inscrições - Disciplinas - Docentes - Livros - FAQs - Eventos - Alunos e Ex-Alunos - Vídeos
Especificações em Z: uma introdução
Este livro é o terceiro volume da série Títulos em Engenharia de Software, editada pela Editora da Unicamp. O texto é autocontido no que diz respeito à notação Z e aos princípios matemáticos que a suportam. Não pressupõe nenhum conhecimento prévio específico por parte do leitor. Todas as noções matemáticas necessárias ao bom uso da notação Z são tratadas em considerável detalhe no texto. Apresentada cada parte matemática básica, a fração da notação Z que dela depende é introduzida em seguida, junto com exemplos de seu uso. Por outro lado, alguma experiência com linguagens de programação de alto nível, como C ou Pascal, seria vantajosa. Há várias semelhanças e analogias entre o uso da notação Z e o ato de programar nestas linguagens que podem ser usadas de forma proveitosa. Também seria conveniente, porém não essencial, que o leitor dispusesse de algum tipo de maturidade matemática. Sendo este um texto introdutório ao uso da notação Z, optou-se por privilegiar os aspectos mais ligados a esta, ficando contidos em exemplos específicos tanto considerações sobre a verificação formal de propriedades do modelo quanto comentários acerca do desenvolvimento automático de código-fonte a partir da especificação construída.
-
-
-
-
-
-
-
-
- PREÇO PARA ALUNO DO INSTITUTO DE COMPUTAÇÃO - UNICAMP: R$ 38,00
- NÚMERO DE PÁGINAS: 306 páginas
Sumário
|
Lista de figuras
|
19
|
|
Lista de tabelas
|
21
|
|
1 Especificações formais
|
23
|
|
1.1 Especificações e precisão
|
23
|
|
1.2 Métodos formais
|
24
|
|
1.3 Um cálculo de programas
|
27
|
|
1.4 Software como produto de engenharia
|
29
|
|
1.5 O formalismo Z
|
30
|
|
1.6 Provas em Z
|
32
|
|
1.7 Transformações e geração de código
|
33
|
|
1.8 Ambientes de especificação e extensões
|
34
|
|
2 Conjuntos
|
35
|
|
2.1 A noção de conjunto
|
35
|
|
2.2 Relação entre elementos e conjuntos
|
38
|
|
2.3 Relações entre conjuntos
|
39
|
|
2.4 Operações sobre conjuntos
|
41
|
|
2.5 Diagramas de Venn
|
44
|
|
2.6 O conunto potência
|
48
|
|
2.7 O produto cartesiano
|
50
|
|
2.8 Exercícios
|
51
|
|
3 Noções de lógica
|
55
|
|
3.1 Conectivos
|
56
|
|
3.1.1 A conjunção
|
56
|
|
3.1.2 A disjunção
|
57
|
|
3.1.3 A implicação
|
57
|
|
3.1.4 A equivalência
|
58
|
|
3.1.5 A negação
|
59
|
|
3.2 Expressões e tautologias
|
59
|
|
3.3 Notação abreviada
|
63
|
|
3.4 Parâmetros formais e declarações
|
64
|
|
3.5 Predicados e conjuntos
|
68
|
|
3.6 Conectivos e conjuntos característicos
|
69
|
|
3.7 Quantificadores
|
70
|
|
3.8 Exercícios
|
79
|
|
4 Tipos em Z
|
85
|
|
4.1 Conjuntos heterogêneos
|
86
|
|
4.2 O paradoxo de Russell
|
87
|
|
4.3 A noção de tipos em Z
|
88
|
|
4.4 Tipos iniciais
|
88
|
|
4.5 Variáveis em Z
|
89
|
|
4.6 Predicados e expressões em Z
|
89
|
|
4.7 Tipos enumerados
|
91
|
|
4.8 O tipo primitivo Z
|
93
|
|
4.9 Construindo conjuntos e o tipo potência
|
95
|
|
4.10 A relação de pertinência
|
99
|
|
4.11 Operando com conjuntos
|
100
|
|
4.12 Subintervalos
|
102
|
|
4.13 Uma abreviação útil
|
103
|
|
4.14 O tipo produto em Z
|
106
|
|
4.15 Algumas extensões da notação
|
109
|
|
4.16 Objetos definidos
|
110
|
|
4.17 Elementos de especificações em Z
|
112
|
|
4.18 Tipos, tipos enumerados e variáveis
|
112
|
|
4.19 Variáveis de entrada, de saída e de estado
|
115
|
|
4.20 Exercícios
|
117
|
|
5 Relações e Funções
|
125
|
|
5.1 A noção de relação
|
125
|
|
5.2 Algumas relações importantes
|
127
|
|
5.3 O domínio e a imagem
|
132
|
|
5.4 Operações sobre relações
|
132
|
|
5.5 A noção de função
|
140
|
|
5.6 Classes de funções
|
141
|
|
5.7 Operações sobre funções
|
143
|
|
5.8 Exercícios
|
145
|
|
6 Relações e funções em Z
|
151
|
|
6.1 A notação relacional em Z
|
151
|
|
6.2 Operações sobre relações em Z
|
154
|
|
6.3 A notação funcional em Z
|
155
|
|
6.4 Definições parametrizadas
|
158
|
|
6.5 Seqüências
|
161
|
|
6.6 Pacotes
|
168
|
|
6.7 Exemplos
|
171
|
|
6.7.1 Inicialização do sistema
|
176
|
|
6.7.2 Locação de fitas
|
177
|
|
6.7.3 Restituição de fitas
|
181
|
|
6.7.4 Inserção e remoção de fitas no acervo
|
184
|
|
6.7.5 Cadastramento de clientes
|
185
|
|
6.7.6 Emissão de relatórios
|
185
|
|
6.7.7 Extensões
|
186
|
|
6.8 Notação lambda
|
186
|
|
6.9 Tipos construídos em Z
|
193
|
|
6.10 Exercícios
|
197
|
|
7 Esquemas em Z
|
211
|
|
7.1 A noção de esquema
|
212
|
|
7.2 Inclusão
|
216
|
|
7.3 As variantes
|
220
|
|
7.4 Revisitando exemplos
|
225
|
|
7.5 Disjunção, conjução e negação
|
229
|
|
7.6 Substituição de nomes
|
237
|
|
7.7 Encapsulamento e quantificação
|
238
|
|
7.8 Composição
|
243
|
|
7.9 Seqüenciamento
|
248
|
|
7.10 Exercícios
|
252
|
|
8 Esquemas e tipos em Z
|
257
|
|
8.1 Criando novos tipos
|
258
|
|
8.2 Valorações
|
261
|
|
8.3 O tipo de um esquema
|
263
|
|
8.4 Exemplos
|
265
|
|
8.5 A notação
|
270
|
|
8.6 Promoção
|
275
|
|
8.7 Esquemas e declarações
|
279
|
|
8.8 Exercícios
|
287
|
|
Referências
|
293
|
|
Índice de símbolos
|
299
|
|
Índice remissivo
|
301
|
