Exemplo - Notação Z

Esta é uma pré-visualização de arquivo. Entre para ver o arquivo original

Joinville
UNIVERSIDADE DO ESTADO DE SANTA CATARINA – UDESC
CENTRO DE CIEˆNCIAS TECNOLO´GICAS – CCT
DEPARTAMENTO DE CIEˆNCIA DA COMPUTAC¸A˜O – DCC
Operac¸o˜es com carta˜o de cre´dito
Lucas Nadolny Vizentainer, Nadyan S. Pscheidt
Me´todos Formais - Linguagem Z
Modelagem de um sistema de carta˜o de cre´dito, incluindo suas operac¸o˜es como:
• Autenticac¸a˜o (falha/sucesso)
• Efetuar pagamento (falha/sucesso)
• Verificac¸a˜o de saldo (falha/sucesso)
• Pagamento com cre´dito (falha/sucesso)
• Pagamento limite (falha/sucesso)
Tipos globais da especificac¸a˜o :
[Carta˜oDeCre´dito]
Caracter : {a, b, c, ..., z}
Retorno == FalhanaAutenticac¸a˜o | SaldoInsuficiente | LimiteEstourado | OK
Carta˜oDeCre´dito
cliente : seq Caracter
senha : N
numeroCarta˜o : N
saldo : R
limiteUsado : R
limiteTotal : R
#senha = 6
limite ≥ 0
#numeroCarta˜o = 16
limiteUsado ≤ limiteTotal
saldo ≥ 0
limiteUsado ≥ 0
1
Para a autenticac¸a˜o ser efetuada com sucesso, o nu´mero de carta˜o precisa existir em Carta˜oDeCre´dito e
a senha fornecida precisa ser a mesma contida em Carta˜oDeCre´dito.
Caso positivo, a mensagem de OK sera´ mostrada.
Autenticac¸a˜o
ΞCarta˜oDeCre´dito
numeroCarta˜o? : N
senha? : N
msg ! : Retorno
numeroCarta˜o? ∈ Carta˜oDeCre´dito ∧ numeroCarta˜o?.senha = senha?
msg ! = OK
FalhaAutenticac¸a˜o
ΞAutenticac¸a˜o
ΞCarta˜oDeCre´dito
numeroCarta˜o? : N
senha? : N
msg ! : Retorno
(numeroCarta˜o? ∈ Carta˜oDeCre´dito ∧ numeroCarta˜o?.senha 6= senha?) ∨
(numeroCarta˜o? 6∈ Carta˜oDeCre´dito)
msg ! = FalhanaAutenticac¸a˜o
Para EfetuarPagamento ser executada com sucesso, o saldo do carta˜o precisa ser maior ou igual ao valor
do pagamento. Com isso, o novo saldo sera´ calculado subtraindo-se o valor pago.
Caso positivo, a mensagem de OK sera´ mostrada.
EfetuarPagamento
∆Carta˜oDeCre´dito
ΞAutenticac¸a˜o
numeroCarta˜o? : N
senha? : N
valor? : Rmsg ! : Retorno
ΞAutenticac¸a˜o
saldo ≥ valor?
saldo′ = saldo − valor?
msg ! = OK
FalhaEfetuarPagamento
ΞEfetuarPagamento
ΞCarta˜oDeCre´dito
numeroCarta˜o? : N
senha? : N
valor? : Rmsg ! : Retorno
ΞFalhaAutenticac¸a˜o ∨ saldo ≤ valor?
if saldo ≤ valor? then msg ! = SaldoInsuficiente
2
Para verificar o saldo, a autenticac¸a˜o deve ser executada com sucesso. Caso positivo, duas mensagens
sera˜o mostradas, a de saldo e o limite dispon´ıvel.
VerificarSaldo
ΞCarta˜oDeCre´dito
ΞAutenticac¸a˜o
limite : R
numeroCarta˜o? : N
senha? : N
msg1! : R
msg2! : R
ΞAutenticac¸a˜o
msg1! = saldo
msg2! = limiteTotal − limiteUsado
Caso a verificac¸a˜o falhe, a mensagem de FalhanaAutenticac¸a˜o sera´ mostrada:
FalhaVerificarSaldo
ΞVerificarSaldo
ΞCarta˜oDeCre´dito
saldo : R
numeroCarta˜o? : N
senha? : N
msg ! : Retorno
ΞFalhaAutenticac¸a˜o
msg ! = FalhanaAutenticac¸a˜o
3
Para o pagamento ser efetuado com sucesso, o valor a ser pago + limite usado deve ser menor que o limite
total. Sera´ tambem atualizado o valor do limiteUsado.
Caso positivo, a mensagem de OK sera´ mostrada.
EfetuarPagamentoCre´dito
∆Carta˜oDeCre´dito
ΞVerificac¸a˜o
numeroCarta˜o? : N
senha? : N
valor? : R
msg ! : Retorno
ΞAutenticac¸a˜o
limiteTotal ≥ valor? + limiteUsado
limiteUsado′ = limiteUsado + valor?
msg ! = OK
FalhaEfetuarPagamentoCre´dito
ΞCarta˜oDeCre´dito
ΞEfetuarPagamentoCre´dito
numeroCarta˜o? : N
senha? : N
valor? : R
msg ! : Retorno
ΞFalhaAutenticac¸a˜o ∨ (limiteTotal < limiteUsado + valor?)
if limiteTotal < (limiteUsado + valor?) then msg ! = LimiteEstourado
4
Para EfetuarPagamentoLimite ser executado com sucesso, o saldo deve ser maior ou igual ao valor a ser
pago. Sera´ atualizado o valor do limiteUsado.
Caso positivo, a mensagem de OK sera´ mostrada.
EfetuarPagamentoLimite
∆Carta˜oDeCre´dito
ΞAutenticac¸a˜o
numeroCarta˜o? : N
senha? : N
valor? : R
msg ! : Retorno
ΞAutenticac¸a˜o
saldo ≥ valor?
limiteUsado′ = limiteUsado − valor?
msg ! = OK
Caso o saldo seja inferior ao valor necessa´rio para o pagamento, a mensagem de SaldoInsuficiente sera´
mostrada:
FalhaEfetuarPagamentoLimite
ΞCarta˜oDeCre´dito
ΞEfetuarPagamentoLimite
numeroCarta˜o? : N
senha? : N
valor? : R
msg ! : Retorno
ΞFalhaAutenticac¸a˜o ∨ (saldo ≤ valor?)
if saldo ≤ valor? then msg ! = SaldoInsuficiente
5