UNIVERSIDADE da MADEIRA
Departamento de Matemática e Engenharias
FUNDAMENTOS LÓGICOS E ALGÉBRICOS DA PROGRAMAÇÃO
Licenciaturas em Engenharia Informática, Ensino de Informática e Matemática
2º Semestre 2005/2006
Folha de exercı́cios nº 6
Especificações Baseadas em Modelos. Linguagem Z
Esquemas de dados: Na linguagem de especificação Z, os esquemas de dados e operações
podem ser apresentados graficamente ou textualmente e são constituı́dos por um identificador,
S, por uma parte declarativa, D, e por uma parte predicativa, P .
Na parte declarativa são declaradas variáveis de estado, identificadores de outros esquemas
e parâmetros/saı́das de operações.
Os valores das variáveis determinam o estado da aplicação informática. As restrições aos
valores são determinadas na parte predicativa do esquema de dados por uma fórmula expressa
na lógica de predicados de primeira ordem. A fórmula da parte predicativa constitui o invariante
da aplicação informática. Qualquer que seja o estado da aplicação informática, a fórmula tem
de ser satisfeita.
1. Consideremos uma máquina de chocolates que vende chocolates de três tamanhos: pequeno, médio e grande. A máquina só aceita moedas de 50 e 20 cêntimos.
A especificação será constituı́da por uma máquina que tem um armazém e uma caixa.
No armazém existe uma certa quantidade de chocolates de cada tamanho. A caixa (de
pagamentos) contém um certo número de moedas de 50 e 20 cêntimos e conhece o preço de
cada um dos chocolates. Estes preços terão que ser ordenados de acordo com o tamanho
dos chocolates e devem ser uma combinação de moedas de 20 e 50.
Represente, na linguagem de especificação Z, um armazém e uma caixa nas condições
acima.
(a) Dê exemplo de um estado permitido na especificação (estado que satisfaz o invariante).
(b) Dê exemplo de dois estados não permitidos na especificação (estados que não satisfazem o invariante).
2. Especifique o esquema Máquina, a partir da importação dos esquemas Armazém e Caixa
definidos no exercı́cio anterior. Apresente este novo esquema na forma concisa e na forma
expandida.
1
Tipos livres: A linguagem de especificação Z permite a declaração de tipos livres. Os tipos
livres podem ser declarados na forma não-recursiva, simplesmente listando os elementos na forma
T ::= A | B | . . . | Z
que é uma abreviação de T == {A, B, . . . , Z}
Os tipos livres permitem a definição recursiva de estruturas de dados na forma
T ::= A | op ≪ B ≫
onde B é uma espécie que utiliza o tipo T .
3. Usando a linguagem de especificação Z:
(a) Escreva a declaração de que uma variável “Status” apenas pode tomar um dos valores
“OK” e “Erro”.
(b) Considere uma espécie de elementos E. A partir da lista vazia, nil, e do operador
cons : E × LIST ֌ LIST , defina recursivamente a estrutura de dados “LIST ” que
representa uma lista de elementos da espécie E.
Operações: Na linguagem de especificação Z, as operações são especificadas pela indicação das
propriedades observadas antes e após a sua execução.
A referência ao valor da variável após a operação é feita usando uma plica após o identificador.
Para um esquema de dados S, o esquema S ′ contém as referências aos valores das variáveis após
a execução de uma operação. O invariante do esquema S aplica-se, de igual forma, ao esquema
S ′.
4. Considerando que a máquina é inicializada sem moedas e sem chocolates, defina, na linguagem de especificação Z a operação “Inicialização”.
Esquema ∆ / Operações com alteração de estado: Dado um esquema de dados S, o
esquema ∆S é um esquema S ∧ S ′ . Os invariantes do esquema S são aplicáveis ao esquema S ′ .
A especificação de uma operação normal identifica os parâmetros necessários à execução da
operação, os valores de saı́da (resultados) e as propriedades satisfeitas antes (pré-condições) e
após (pós-condições) a operação. Na linguagem de especificação Z não existe uma separação
clara entre a pré-condição e a pós-condição: a conjunção das duas condições forma a parte
predicativa do esquema.
5. Indique o esquema da operação “NovoPreçoP” de alteração, sem falhas, do preço do chocolate pequeno.
6. Especifique a operação “CompraChocPOk” de compra, sem falhas, de um chocolate pequeno. Note que têm de ser considerados os parâmetros v50?, v20? que indicam as moedas
introduzidas pelo cliente, e as variáveis de resultado t50!, t20! que determinam o troco (o
qual apenas pode usar moedas já existentes na caixa antes da operação).
2
Esquema Ξ / Operações sem alteração de estado: Dado um esquema de dados S, o
esquema ΞS é um esquema sem parâmetros e sem resultados, sendo apenas usado na parte
predicativa o predicado de igualdade sobre as variáveis de estado.
As operações sem alteração de estado, tais como situações erróneas e de leitura, importam
o esquema Ξ.
7. Defina o esquema “ΞMáquinaIgual”, em que todas as variáveis de estado mantêm o mesmo
valor. Utilize esse esquema para especificar a operação “Saldo”, de leitura do saldo existente na máquina.
8. Especifique a operação “CompraChocPErr” de compra, não sucedida, de um chocolate
pequeno.
Esquemas Axiomáticos: Um esquema axiomático define constantes. Ao contrário das variáveis
de estado, o valor das constantes nunca pode ser alterado e os esquemas axiomáticos não possuem identificador. Os esquemas axiomáticos são globais, i.e., podem ser acedidos em todas as
partes predicativas de qualquer esquema definido depois do esquema axiomático. Os esquemas
axiomáticos podem também ser usados nos limites de gamas de valores.
9. Especifique um esquema axiomático que define uma constante “DIM ” de espécie N.
(a) Modifique o esquema Armazém definido no exercı́cio 1 de forma que este passe a
incluir a restrição de que o número máximo de chocolates de cada tipo existentes em
armazém é DIM .
(b) Defina a constante CALC de cálculo do valor de um número de moedas de 20 e de
50 cêntimos.
(c) Utilize a constante CALC para simplificar a especificação do esquema CompraChocP Ok
introduzido no exercı́cio 6.
3