Esquemas e suas operações

Forma geral:
Ident.
Declarações
Predicado

ou
Ident. =^ [Declarações | Predicado]
Esquemas são estruturas que agrupam
variáveis e predicados que restringem
seus valores. Seu nome possui escopo
global, mas as declarações e
predicados possuem escopo local
Exemplos de esquemas
given sets
[Pessoa, Fone]
Agenda =^ [ag: Pessoa  Fone; con: IP Pessoa | con = dom ag]
ou, alternativamente,
Agenda
ag: Pessoa  Fone
con: IP Pessoa
con = dom ag
Renomeação em esquemas

Forma geral:
– nomeEsquema [nomeNovo / nomeAtual]

Exemplo: Aniversarios =^ Agenda[aniv/ag]
Resulta em
Aniversarios
aniv: Pessoa  Fone
con: IP Pessoa
con = dom aniv
Inclusão de Esquemas

Forma geral:
Ident.
nomeEsquema
Declarações
Predicado

Exemplo:
ContaAg
Agenda
qtd: IN
qtd = # con
ContaAg
ag: Pessoa  Fone
con: IP Pessoa
qtd: IN
con = dom ag
qtd = # con
Decoração de esquemas


Forma geral: nomeEsquema’
Exemplo:
ContaAg’
ag’: Pessoa  Fone
con’: IP Pessoa
qtd’: IN
con’ = dom ag’
qtd’ = # con’
Convenções sobre esquemas



Forma geral:  nomeEsquema
Usado em operações para denotar
mudança de estado
Exemplo:
 Agenda
Agenda
Agenda’
 Agenda
ag, ag’: Pessoa  Fone
con, con’:IP Pessoa
con = dom ag
con’ = dom ag’
Convenções sobre esquemas



Forma geral:  nomeEsquema
Usado em operações para denotar que
não há mudança de estado
Exemplo:
 Agenda
 Agenda
ag=ag’
con=con’
 Agenda
ag, ag’: Pessoa  Fone
con, con’: IP Pessoa
con = dom ag
con’ = dom ag’
ag = ag’
con = con’
Usando  e  em operações
Inclui0
 Agenda
p?: Pessoa
f?: Fone
ag’ = ag  {p?  f?}
con’ = con  {p?}
Consulta0
 Agenda
p?: Pessoa
f!: Fone
p?  con
f! = ag(p?)
Variáveis de entrada (?)
Variável de saída (!)
Conjunção e disjunção de
esquemas
Seja Resultado ::= opOK | pessoaInexistente
ERRO
Sucesso
 Agenda
m!: Resultado
p?: Pessoa
m! = opOK
m!: Resultado
p?  con
m! = pessoaInexistente
^ (Consulta  Sucesso)  ERRO
Consulta =
0
Outras operações

nomeEsquema1  nomeEsquema2
– Junta declarações
– Implicação dos predicados

nomeEsquema1  nomeEsquema2
– Junta declarações
– Equivalência dos predicados
Operação ocultamento (“hiding”)


Corresponde a quantificar
existencialmente variáveis em questão
Exemplo: QualquerFone = Consulta0\(p?)
QualquerFone
 Agenda
f!: Fone
 p?:Pessoa 
p?  con
f! = ag(p?)
Composição seqüencial

Sejam O1 e O2 dois esquemas como
operações

O1;O2 representa a composição
seqüencial entre O1 e O2
Significando que o estado final de O1 irá
coincidir com o estado inicial de O2

entrada(?){
S
O1
S’ = S
O2
Estado intermediário
S’
}saída (!)
Composição seqüencial
Sejam O1 e O2 os seguintes esquemas:
O1
O2
x, x’: T
x, x’: T
P(x, x’)
Q(x, x’)
A composição seqüencial de O1 e O2, O1 ; O2, é definida por:
^ (O [x /x’]  O [x /x]) \ (x )
O1 ; O2 =
1 0
2 0
0
ou
O1 ; O2
x, x’: T
 x0:T  P(x, x0)  Q(x0, x’)


Exercício: se p?  dom ag então Inclui0 ; Exclui0 Agenda,
onde
Exclui0 =^ [ Agenda; p?:Pessoa |
p?  con  ag’ = {p?} ag  con’ = con\{p?}]
Operação piping



Semelhante à composição seqüencial,
exceto por considerar as comunicações
ao invés do estado
Portanto, P>>Q significa que as saídas
de P corresponderão as entradas de Q
O predicado referente ao estado será
simplesmente a conjunção dos
predicados de P e de Q
Tipos em Z

Há quatro formas de introduzir tipos em
Z:
– Given sets: [ ... ]
– Produto cartesiano: ...  ...
– Conjunto das partes: IP ...
– Esquemas:
nomeTipo
...
...
Tipos em Z


Os naturais ( IN), inteiros (Z) e reais ( IR)
são usualmente assumidos como prédefinidos
Conjuntos arbitrários são permitidos em
declarações, mas nem sempre são tipos
– O tipo é derivado (inferência) das subexpressões que compõem o conjunto
arbitrário, através de um processo de
normalização
Processo de normalização
Seja Pares == { n: IN | 2 * n }
y: Pares
R: X  Y
f: X  Y
s: seq X
y: IN
y  Pares
R: IP(X  Y)
f: IP(X  Y)
fXY
s: IP(X  Y)
s  seq X
Esquema como tipo


Semelhante aos registros de PASCAL
Componentes são acessados através
da operação de projeção (.)
Agenda
ag: Pessoa  Fone
con: IP Pessoa
con = dom ag
a, b: Agenda
a . ag = b . ag
Projeção
Mapeamentos (“bindings”)


Um esquema como tipo pode ser visto
como um binding de variável para valor
Por exemplo: seja a: Agenda, tal que
 ag

{(josé,32213423)}, con
{josé} 
Então, aplicando o operador de projeção
sobre a, referente a ag, nos dá
– a . ag = {(josé, 32213423)}
O operador 


Aplica-se a nomes de esquemas,
retornando seu binding característico
Por exemplo: seja a: Agenda, tal como
antes então
–  a =  ag


{(josé,32213423)}, con
{josé} 
Seu uso comum é  Agenda’= Agenda,
que implica ag’=ag  con’=con
Um esquema é dito normalizado quando
suas declarações estão normalizadas