quarta-feira, 19 de novembro de 2008
Comando: Trivial rewrite
1. Usa regra de reescrita
2. Não faz reason aritmético
3. Não usa grules
4. Não faz simplificação
5. Talvez não use regra de reescrita com Generic actuals
2. Não faz reason aritmético
3. Não usa grules
4. Não faz simplificação
5. Talvez não use regra de reescrita com Generic actuals
Comando: Simplify
1. Não usa regra de reescrita.
2. Usa foward rules.
3. Usa grule
4. Faz reason aritmético
Ex: identidades
5. Não infere: A \in \power A
6. Faz simplificações lógicas
Ex: (PREDICATE \iff true) é substituído por (PREDICATE)
2. Usa foward rules.
3. Usa grule
4. Faz reason aritmético
Ex: identidades
5. Não infere: A \in \power A
6. Faz simplificações lógicas
Ex: (PREDICATE \iff true) é substituído por (PREDICATE)
domingo, 26 de outubro de 2008
Comando: Instantiate
Parte I - Uso do instante para eliminar quantificador existencial da conclusão.
Problema:
As vezes, para concluir uma prova (teorema da inicialização, por exemplo), pode ser necessário resolver um problema com o formato:
Nesta situação, o quantificador existencial precisa ser eliminado. Para realizar isto, o especificador precisa encontrar uma witness para eliminar o quantificador existencial utilizando o comando instantiate. Em alguns casos, é necessário definir a witness para depois poder utilizá-la. Na notação acima, o que está entre colchetes é opcional.
Uma vez em posse da witness, utiliza-se o comando instantiate para instrui o provador a aplicar a one-point-rule e transformar o predicado para o predicado.
O segundo passo da transformação é mostrado a seguir e é aplicado se a parte opcional destaca entre colchetes estiver presente no predicado.
Seja C um predicado contendo um quantificador existencial. Seja A um conjunto de premissas. Então, o resultado de um comando de instanciação da variável declarada em C resulta nos seguintes passos de prova:
1. A => C
2. A => B or C
3. A and NOT(B) => C
Do passo 1 para o 2 é aplicado a One-Point-Rule:
Do passo 2 para o passo 3 é aplicado transformação lógica.
Problema:
As vezes, para concluir uma prova (teorema da inicialização, por exemplo), pode ser necessário resolver um problema com o formato:
[set of premiss \implies] \exist variable : TYPE @ predicate
Nesta situação, o quantificador existencial precisa ser eliminado. Para realizar isto, o especificador precisa encontrar uma witness para eliminar o quantificador existencial utilizando o comando instantiate. Em alguns casos, é necessário definir a witness para depois poder utilizá-la. Na notação acima, o que está entre colchetes é opcional.
Uma vez em posse da witness, utiliza-se o comando instantiate para instrui o provador a aplicar a one-point-rule e transformar o predicado para o predicado.
[set of premiss \implies] witness \in TYPE \land predicate[witness/variable]
\lor \exist variable : TYPE @predicate
\lor \exist variable : TYPE @predicate
O segundo passo da transformação é mostrado a seguir e é aplicado se a parte opcional destaca entre colchetes estiver presente no predicado.
set of premiss \land (\not (witness \in TYPE \land predicate[witness/predicate])) \implies \exist variable @predicate
Seja C um predicado contendo um quantificador existencial. Seja A um conjunto de premissas. Então, o resultado de um comando de instanciação da variável declarada em C resulta nos seguintes passos de prova:
1. A => C
2. A => B or C
3. A and NOT(B) => C
Do passo 1 para o 2 é aplicado a One-Point-Rule:
Do passo 2 para o passo 3 é aplicado transformação lógica.
quarta-feira, 22 de outubro de 2008
Usando Grules
O uso de grules aumenta significativamente o grau de automação de uma prova, pois em situações específicias elimina a necessidade do especificador lidar com problemas referentes a tipos e restrições de valores durante a prova de teoremas (Domain Check e Preconditions por exemplo). Abaixo descrevo como inserir uma grule no Sistema Policial e depois apresento um conjunto de exemplos de situações em que grules podem ser utilizadas.
A quarta versão do Sistema Policial não adiciona nenhuma mudança substancial. Apenas foi adicionado na prova uma regra de automação do tipo grule. O teorema
\begin{theorem}{grule gCPFMaxType}
CPF \in \power \num
\end{theorem}
é usado para dizer ao Z/Eves qual tipo maximal de CPF, sem que seja necessário realizar a expansão de CPF. Isto é, se durante a prova de alguma operação o Z/Eves produzir como objetivo de prova o predicado:
CPF \in \power \num
Então este predicado será convertido a true sem que seja necessário invocar a definição de CPF.
O Z/Eves gera grules quando são definidas constantes em axiomatic-box e generic-box como pode ser observado no Reference Manual 1.5, pag. 20. Free types e schemas também geram grules (descobri isto mexendo). Para mais informações sobre grule consulte o Z/Eves User's Guide 2.3, pag. 41. Um link para um arquivo contendo um conjunto de exemplos ilustrando o uso de grules no Z/Eves está disponível no final da página. Abaixo, discuto estes exemplos.
Grules_Example01 - São definidos dois tipos. É apresentado um teorema em que o predicado envolve o tipo maximal dos tipos defindos antes. Note que para provar este teorema o especificador precisa instruir o Z/Eves manualmente (realizando expansão - i.e., Invoke).
Grules_Example02 - O mesmo exemplo anterior, só que agora foi criada uma grule para informar ao Z/Eves o tipo maximal de B. Para provar o teorema sobre o tipo de B não é necessário expandir B.
Voce deveria notar nos dois exemplos anteriores que o Z/Eves não criou nenhum teorema para os tipos inseridos pelo usuário. Foram inseridos given sets e abbreviations. Nestas situações o especificador deve se encarregar de criar grules para os tipos, se houver necessidade.
Grules_Example03 - Um exemplo maior, utilizando given sets e schemas. Note que quando um schema é definido e é utilizado como tipo, o Z/Eves gera automaticamente a grule SchemaName$declaration. Note também que, se um schema é definido e não é utilizado como tipo, o Z/Eves não gera a regra de automação do tipo grule para o schema. Neste exemplo, o tipo C não foi utilizado como tipo e por isso o Z/Eves não gerou uma grule associada a TIPO_C.
Grules_Example04 - O exemplo anterior, com uma grule adicionada para TIPO_C. A grule não está provada. Não consegui realizar a prova desta grule. Se conseguir, envie-me a resolução. Thanks ;-)
Grules_Example05 - Neste exemplo uma grule é utilizada para adicionar informação sobre restrição de valor. Para isto, dois valores, minvalue e maxvalue, foram definidos através de um axiomatic-box. Ainda no axiomatic-box há uma rule relacionando os dois valores através do predicado: minvalue \leq maxvalue
No teorema ListInitialisation um dos goals é mostrar que: 0 \leq minvalue. A grule foi utilizada para evitar que o especificador tivesse que lidar com a expansão de \nat ao realizar a prova de ListInitialisation.
Este teorema foi propositalmente posto em dois lugares, antes e depois da grule. Pretendeu-se assim mostrar o ganho de automação com o uso da grule.
Note que este exemplo difere bastante dos anteriores, pois usou grules para adicionar informação sobre uma restrição de valor e não sobre tipos.
A quarta versão do sistema policial está disponível em: http://www.dcc.ufba.br/~diego052/experimento/zevesblog/SistemaPolicial_v4.zip
O arquivo de exemplos de uso de grules está disponível em: http://www.dcc.ufba.br/~diego052/experimento/zevesblog/Grules_Examples_01-05.zip
A quarta versão do Sistema Policial não adiciona nenhuma mudança substancial. Apenas foi adicionado na prova uma regra de automação do tipo grule. O teorema
\begin{theorem}{grule gCPFMaxType}
CPF \in \power \num
\end{theorem}
é usado para dizer ao Z/Eves qual tipo maximal de CPF, sem que seja necessário realizar a expansão de CPF. Isto é, se durante a prova de alguma operação o Z/Eves produzir como objetivo de prova o predicado:
CPF \in \power \num
Então este predicado será convertido a true sem que seja necessário invocar a definição de CPF.
O Z/Eves gera grules quando são definidas constantes em axiomatic-box e generic-box como pode ser observado no Reference Manual 1.5, pag. 20. Free types e schemas também geram grules (descobri isto mexendo). Para mais informações sobre grule consulte o Z/Eves User's Guide 2.3, pag. 41. Um link para um arquivo contendo um conjunto de exemplos ilustrando o uso de grules no Z/Eves está disponível no final da página. Abaixo, discuto estes exemplos.
Grules_Example01 - São definidos dois tipos. É apresentado um teorema em que o predicado envolve o tipo maximal dos tipos defindos antes. Note que para provar este teorema o especificador precisa instruir o Z/Eves manualmente (realizando expansão - i.e., Invoke).
Grules_Example02 - O mesmo exemplo anterior, só que agora foi criada uma grule para informar ao Z/Eves o tipo maximal de B. Para provar o teorema sobre o tipo de B não é necessário expandir B.
Voce deveria notar nos dois exemplos anteriores que o Z/Eves não criou nenhum teorema para os tipos inseridos pelo usuário. Foram inseridos given sets e abbreviations. Nestas situações o especificador deve se encarregar de criar grules para os tipos, se houver necessidade.
Grules_Example03 - Um exemplo maior, utilizando given sets e schemas. Note que quando um schema é definido e é utilizado como tipo, o Z/Eves gera automaticamente a grule SchemaName$declaration. Note também que, se um schema é definido e não é utilizado como tipo, o Z/Eves não gera a regra de automação do tipo grule para o schema. Neste exemplo, o tipo C não foi utilizado como tipo e por isso o Z/Eves não gerou uma grule associada a TIPO_C.
Grules_Example04 - O exemplo anterior, com uma grule adicionada para TIPO_C. A grule não está provada. Não consegui realizar a prova desta grule. Se conseguir, envie-me a resolução. Thanks ;-)
Grules_Example05 - Neste exemplo uma grule é utilizada para adicionar informação sobre restrição de valor. Para isto, dois valores, minvalue e maxvalue, foram definidos através de um axiomatic-box. Ainda no axiomatic-box há uma rule relacionando os dois valores através do predicado: minvalue \leq maxvalue
No teorema ListInitialisation um dos goals é mostrar que: 0 \leq minvalue. A grule foi utilizada para evitar que o especificador tivesse que lidar com a expansão de \nat ao realizar a prova de ListInitialisation.
Este teorema foi propositalmente posto em dois lugares, antes e depois da grule. Pretendeu-se assim mostrar o ganho de automação com o uso da grule.
Note que este exemplo difere bastante dos anteriores, pois usou grules para adicionar informação sobre uma restrição de valor e não sobre tipos.
A quarta versão do sistema policial está disponível em: http://www.dcc.ufba.br/~diego052/experimento/zevesblog/SistemaPolicial_v4.zip
O arquivo de exemplos de uso de grules está disponível em: http://www.dcc.ufba.br/~diego052/experimento/zevesblog/Grules_Examples_01-05.zip
quarta-feira, 9 de julho de 2008
Construindo uma especificação do zero - Sistema Policial v.3
A terceira versão além de corrigir a falha da segunda versão, propõe uma mudança no TAD que armazena os atributos de uma pessoa, PERSON. Ao inves de tratar uma pessoa somente como um registro numerico (CPF), o registro da pessoa também deve conter o seu nome. Na especificação está mudança reflete a alteração do tipo PERSON, anteriormente definido como abreviacao de CPF, para um tipo definido em um schema.
Foi adicionado um teorema que prova que o predicado foreign? \notin population, adicionado à parte predicativa de REGISTRATION, é a precondição de REGISTRATION.
A terceira versão da especificação deste sistema pode ser encontrada em:
http://www.dcc.ufba.br/~diego052/experimento/zevesblog/Sistema_Policial_v3.zip
Problemas da especificação anterior
Há um erro na especificação anterior (sistema_policial_v2) na operação REGISTRATION. Esta operação não verifica se o elemento que está sendo cadastrado já está cadastrado. O problema do elemento já estar cadastrado é que, foreign? pode pertencer ao conjunto offenders e a operação REGISTRATION o adicionará ao conjunto innocents. Esta operação pode, portanto, produzir um estado inválido para o sistema, onde innocents e offenders não são disjuntos. Para solucionar este problema, foi adicionado mais um predicado à parte predicativa de REGISTRATION. O predicado adicionado é: foreign? \notin population.
Construindo uma especificação do zero - Sistema Policial v.2
Para corrigir o problema da versão anterior existem duas vertentes, a primeira é assumir que PERSON não está contido em population. Esta abordagem sugere a retirada da terceira invariante do sistema (shema DATABASE).
Outra solução é assumir todas pessoas já são conhecidas pelo sistema (population), e forçar que o sistema tenha uma visão pessimista das pessoas, isto é, todas pessoas são inicialmente alocadas com antecedentes criminais. Desta forma, o ato de cadastrar uma pessoa corresponde a remove-la do conjunto offenders e coloca-la no conjunto innocents.
A primeira solução é a mais adequada, pois em um sistema computacional os dados são entrados a medida que são colhidos, isto é, as pessoas vão sendo cadastradas a medida surge esta necessidade. Não existe, a priori, um cadastro de todas pessoas com o qual o sistema policial irá operar.
Para conferir se o estado sugerido é factível, vamos propor um estado inicial INIT_DATABASE e provar o teorema da inicialização para DATABASE. Para provar este teorema utilizamos poucos comandos de prova. O comando Invoke é utilizado para realizar a expansão de um schema. Este comando pode ser utilizado recebendo ou não parâmetros.
A segunda versão da especificação deste sistema pode ser encontrada em:
http://www.dcc.ufba.br/~diego052/experimento/zevesblog/Sistema_Policial_v2.zip
Problemas da especificação anterior
Há um problema nesta especificação (sistema_policial_v1). Para registrar uma pessoa, assume-se que esta pessoa não pertence ao conjunto da população. No entanto, esta noção não é condizente com a invariante do sistema que afirma que toda pessoa existente já pertence a população. Note inclusive, que uma pessoa nesta especificação é um número. Assim, a invariante afirma que todo elementode Z (\num) é também elemento de population.
Construindo uma especificação do zero - Sistema Policial v.1
A partir desta postagem, é esperado que o leitor já tenha realizado a leitura dos 14 primeiros capítulos do Using Z. Por ora, não é necessário ler o capitulo 13 (Promotion) nem ler e o trecho do capitulo 14 que utiliza Promotion.
Esta especificação foi desenvolvida recentemente por mim. Meu propósito foi avaliar a dificuldade de escrever uma especificação a partir do zero. Abaixo descrevo um problema fictício, que motiva o desenvolvimento da especificação:
Descrição do problema: Sistema Policial
Deve ser especificado um sistema que gerencie uma base de dados de pessoas. A chave primaria utiliza para identificar as pessoas é o número do CPF. O sistema deve permitir a classificação das pessoas cadastradas em dois grupos:
Grupo 1: pessoas sem histórico criminal.
Grupo 2: pessoas com histórico criminal.
A partir desta definição, propus a primeira versão da especificação. A especificação é apresentada utilizando as conveções LaTex para Z. Estas convenções podem ser encontradas no Reference Card, distribuido junto com o Z/Eves. A sequencia de passos para compor esta especificação foi:
1. Definir um tipo dado para o nome das pessoas:
[NOME]
2. Para armazenar os numeros de CPF, é adequado utilizar números inteiros. Para tornar mnemonica a especificação defini uma abreviação para inteiros:
CPF == \num
3. Para representar as pessoas é utilizado o número do CPF. Para tornar mnemonica a especificação defini uma abreviação para CPF:
PERSON == CPF
4. O sistema deve armazenar as pessoas e classificá-las nos dois grupos. Os grupos 1 e 2 são distintos. O schema DATABASE foi usado para modelar o estado do sistema. Os atributos utilizados foram:
population - conjunto de todas pessoas cadastradas no sistema
offenders - conjunto de pessoas com antecendentes criminais
innocents - conjunto de pessoas sem ntecedentes criminais
5. Uma operação de registro de pessoas foi especificada. O schema REGISTRATION foi usado para modelar esta operação. Esta operação tem como entrada uma pessoa, denotada por foreign?. Quando uma pessoa é registrada ela é inserida nos conjuntos population e innocents. O conjunto offenders não sofre modificação nesta operação.
6. Uma operação de mudança de status foi especificada. Esta operação tem como entrada uma pessoa, denotada por p?. Se esta pessoa pertencer ao conjunto offenders, ela será removida do conjunto offenders e inserida no conjunto innocents. Se esta pessoa pertencer ao conjunto innocents, ela será removida do conjunto innocents e inserida no conjunto offenders.
7. Foi provado um teorema que afirma que toda pessoa satisfazendo as condições do estado do sistema, deve pertencer ao conjunto innocents ou então deve pertencer ao conjunto offenders.
A primeira versão da especificação deste sistema pode ser encontrada em:
Esta especificação foi desenvolvida recentemente por mim. Meu propósito foi avaliar a dificuldade de escrever uma especificação a partir do zero. Abaixo descrevo um problema fictício, que motiva o desenvolvimento da especificação:
Descrição do problema: Sistema Policial
Deve ser especificado um sistema que gerencie uma base de dados de pessoas. A chave primaria utiliza para identificar as pessoas é o número do CPF. O sistema deve permitir a classificação das pessoas cadastradas em dois grupos:
Grupo 1: pessoas sem histórico criminal.
Grupo 2: pessoas com histórico criminal.
A partir desta definição, propus a primeira versão da especificação. A especificação é apresentada utilizando as conveções LaTex para Z. Estas convenções podem ser encontradas no Reference Card, distribuido junto com o Z/Eves. A sequencia de passos para compor esta especificação foi:
1. Definir um tipo dado para o nome das pessoas:
[NOME]
2. Para armazenar os numeros de CPF, é adequado utilizar números inteiros. Para tornar mnemonica a especificação defini uma abreviação para inteiros:
CPF == \num
3. Para representar as pessoas é utilizado o número do CPF. Para tornar mnemonica a especificação defini uma abreviação para CPF:
PERSON == CPF
4. O sistema deve armazenar as pessoas e classificá-las nos dois grupos. Os grupos 1 e 2 são distintos. O schema DATABASE foi usado para modelar o estado do sistema. Os atributos utilizados foram:
population - conjunto de todas pessoas cadastradas no sistema
offenders - conjunto de pessoas com antecendentes criminais
innocents - conjunto de pessoas sem ntecedentes criminais
5. Uma operação de registro de pessoas foi especificada. O schema REGISTRATION foi usado para modelar esta operação. Esta operação tem como entrada uma pessoa, denotada por foreign?. Quando uma pessoa é registrada ela é inserida nos conjuntos population e innocents. O conjunto offenders não sofre modificação nesta operação.
6. Uma operação de mudança de status foi especificada. Esta operação tem como entrada uma pessoa, denotada por p?. Se esta pessoa pertencer ao conjunto offenders, ela será removida do conjunto offenders e inserida no conjunto innocents. Se esta pessoa pertencer ao conjunto innocents, ela será removida do conjunto innocents e inserida no conjunto offenders.
7. Foi provado um teorema que afirma que toda pessoa satisfazendo as condições do estado do sistema, deve pertencer ao conjunto innocents ou então deve pertencer ao conjunto offenders.
A primeira versão da especificação deste sistema pode ser encontrada em:
http://www.dcc.ufba.br/~diego052/experimento/zevesblog/Sistema_Policial_v1.zip
Z/Eves no Windows (Mouse scroll)
A interface gráfica do Z/Eves para Windows possui bugs e costuma travar quando o scroll do mouse é utilizado. Se este problema ocorrer na sua instalação, desabilite o scroll do mouse através do painel de controle do Windows, no item "Mouse".
No Linux este problema não ocorre ;-)
The Z/EVES User’s Guide
Para compreender a interface gráfica e as funcionalidades providas pelo Z/Eves, você deve realizar a leitura do The Z/EVES 2.0 User’s Guide.
Este documento é distribuido com o software Z/Eves. Se você já baixou um pacote de instalação do Z/Eves, após instalá-lo você terá acesso a este documento.
O User's Guide ilustra o uso do Z/Eves através de especificações que usam Schemas. Schemas são abordados no capitulo 12 do Using Z. Por ora, não se preocupe com o entendimento da especificação exemplo do User's Guide, pois ela se tornará clara quando você avançar na leitura do Using Z. É suficiente neste primeiro momento que você note o que o Z/Eves pode lhe oferecer a principio: uma janela para interagir com a especificação (pag. 1-17), Type Checking e Domain Checking. (pag. 19-22).
Aconselho que a leitura do capitulo seis e posteriores do Using Z seja acompanhada do uso do Z/Eves. O que fizemos no MEFES foi: paralelo a leitura destes capitulos, escrevemos as especificações vistas no livro no Z/Eves. Esta é uma forma de habituar-se gradualmente ao ambiente do Z/Eves.
Onde encontrar o Python?
Uma versão do Python compativel com a versão 2.3.1 para Windows pode ser encontrada a partir do link:
http://www.dcc.ufba.br/~diego052/experimento/softwares/zeves/
Por que instalar o Python 2.3?
Você deve ter o Python instalado para poder usar a interface gráfica do Z/Eves. Caso não possua o Python, apenas poderá usar o Z/Eves em modo texto.
sexta-feira, 6 de junho de 2008
Download do Z/Eves 2.3 e 2.3.1
O Z/Eves 2.3.1 para windows pode ser baixado a partir do site
http://dl.dropbox.com/u/11299884/ZEves/Python-2.3.exe
(Python 2.3)
http://dl.dropbox.com/u/11299884/ZEves/Python-2.3.exe
(Python 2.3)
http://dl.dropbox.com/u/11299884/ZEves/z-eves-install-2.3.1.exe
(Z/Eves 2.3.1 para Windows)
(Z/Eves 2.3.1 para Windows)
http://dl.dropbox.com/u/11299884/ZEves/sm-windows.pdf
(Manual de instalação)
(Manual de instalação)
É necessário instalar o Python para utilizar a interface gráfica do Z/Eves. Neste site também é possível encontrar o manual de instalação (terceiro link).
Abaixo, um link para o Z/Eves 2.3 para Linux.
O arquivo abaixo é uma compilação do Z/Eves 2.3 + Python 1.5 + Tcl/Tk.
Procedimento para instalação e uso
1. Baixar e descompactar arquivo. Para descompactar, entre no diretório onde o arquivo foi baixado e digite no terminal do linux:
tar -jxvf Z.tar.bz2
2. Mover a pasta recém criada "Z" para o diretório /opt. Para fazer isto você precisará ter acesso de root:
mv Z /opt
3. Para executar o Z/EVES digite no terminal as linhas a seguir para fazer rodar a interface gráfica:
cd /opt/Z/Z-Eves/system
./z-eves-gui.sh
quinta-feira, 5 de junho de 2008
Onde encontrar o Z/Eves?
O site da ORA, a empresa que desenvolve o Z/Eves, não está mais online. Desta forma, não é possível encontrar o Z/Eves em um site oficial.
A versão do Z/Eves que utilizo no grupo de pesquisa é a 2.3, ela pode ser conseguida a partir do site http://www.exactas.org/. Neste site podem ser encontradas versões para linux e windows.
quarta-feira, 4 de junho de 2008
Onde começar?
Sugiro a leitura dos primeiros capítulos do livro Using Z: Specification, Refinement, and Proof. O livro é gratuito e pode ser baixado a partir do site: http://www.usingz.com. Segundo meu orientador, este é o melhor material já produzido para quem está começando a estudar métodos formais em Z.
É esperado que o leitor possua conhecimento em lógica matemática antes de lidar diretamente com especificações em Z. O UsingZ não pressupõe conhecimento algum em lógica matemática, os três primeiros capítulos são gastos com motivação e explicações sobre conectivos e quantificadores.
Se você fez um bom curso de lógica matemática o conteúdo destes capítulos deve lhe ser familiar.
Outro material que conheço é o Especificações em Z: uma introdução. O autor é o Arnaldo Vieira Moura, professor da UNICAMP. A página do autor é http://ze.ic.unicamp.br/
Um excelente material de referência sobre a notação Z é o livro Z Notation (Spivey), este material é mais adequado para quem já conhece Z e deseja revisar certas construções ou leis do toolkit matemático da notação Z.
É esperado que o leitor possua conhecimento em lógica matemática antes de lidar diretamente com especificações em Z. O UsingZ não pressupõe conhecimento algum em lógica matemática, os três primeiros capítulos são gastos com motivação e explicações sobre conectivos e quantificadores.
Se você fez um bom curso de lógica matemática o conteúdo destes capítulos deve lhe ser familiar.
Outro material que conheço é o Especificações em Z: uma introdução. O autor é o Arnaldo Vieira Moura, professor da UNICAMP. A página do autor é http://ze.ic.unicamp.br/
Um excelente material de referência sobre a notação Z é o livro Z Notation (Spivey), este material é mais adequado para quem já conhece Z e deseja revisar certas construções ou leis do toolkit matemático da notação Z.
Assinar:
Postagens (Atom)