 |
| Autor: Anónimo | Fuente:Wikipedia | Licencia: CC BY-SA 3.0 |
Para los que están aprendiendo a realizar especificaciones completas de sistemas informáticos (o partes críticas de los mismos) valiéndose de lenguajes formales como Z, sabrán que es un tema que hay que coger con mucho tacto y dedicación. Y es que tanta simbología y matemática pueden dejarte en babia y atorarte cada dos por tres, pero esto cambia practicando mucho y, como no, inspirándose con ejemplos.
Como ya ha finalizado el primer cuatrimestre, voy a hacer pública mi solución de la práctica final de Métodos Formales, la cual no es la única solución ni la mejor, pero seguro que os servirá como ejemplo.
Si no deseas escribir la especificación en papel, visita http://czt.sourceforge.net/.
Enunciado
En el videoclub se alquilan copias de películas identificadas por una clave única, las cuales incluyen también el nombre de la película. Pueden existir varias copias de una misma película, por tanto todas ellas compartirían el título.
Los socios, se identificarán de forma única con una clave y además el sistema registrará el nombre de los mismos (puede haber dos socios que se llamen igual).
Deben definirse, al menos las siguientes operaciones:
- Introducción de una nueva película.
- Introducción de un socio nuevo.
- Retirada de una película por un socio.
- Devolución de la película.
- Aviso diario de los socios que deben entregar la película ese día.
- Eliminación de un socio.
- Eliminación de una película.
Solución
Declaración de tipos básicos. El IdentificadorPelícula podría ser un número y el IdentificadorSocio el DNI.
Como es requisito de la práctica un alto nivel de abstracción los he denominado así:
─ [IdentificadorPelícula, IdentificadorSocio, Título, Nombre, Fecha] └
Tipos de errores que puede haber mediante definición de tipos libres:
─
Report ::= ok | Identificador_película_duplicado | Identificador_socio_duplicado |
Socio_inexistente | Película_inexistente | Película_ya_alquilada | Película_no_alquilada |
Socio_con_películas_sin_devolver
└
El esquema del videoclub incluye las películas, los socios y las películas alquiladas de forma que se ven como tres funciones totales (todos los elementos tienen imagen).
Se presupone que un mismo socio puede alquilar varias películas.
┌ Videoclub
películas: IdentificadorPelícula → Título
socios: IdentificadorSocio → Nombre
películasAlquiladas: IdentificadorPelícula → (IdentificadorSocio × Fecha)
|
dom (películasAlquiladas) ⊆ dom (películas)
∀s: IdentificadorSocio | s ∈ {r:IdentificadorSocio; f:Fecha | (r,f) ∈ ran
(películasAlquiladas) ⦁ r} ⦁ s ∈ dom (socios)
└
Esquema del videoclub decorado:
┌ Videoclub′
películas′: IdentificadorPelícula → Título
socios′: IdentificadorSocio → Nombre
películasAlquiladas′: IdentificadorPelícula → (IdentificadorSocio × Fecha)
|
dom (películasAlquiladas′) ⊆ dom (películas′)
∀s: IdentificadorSocio | s ∈ {r:IdentificadorSocio; f:Fecha | (r,f) ∈ ran
(películasAlquiladas′) ⦁ r} ⦁ s ∈ dom (socios′)
└
Inicialización del videoclub:
┌ VideoclubInit
Videoclub′
|
películas′ = ∅
socios′ = ∅
películasAlquiladas′ = ∅
└
Operación que permite introducir una nueva película en el videoclub:
┌ IntroducirNuevaPelícula
ΔVideoclub
título?: Título
identificador?: IdentificadorPelícula
reporte!: Report
|
identificador? ∉ dom (películas)
películas′ = películas ∪ {identificador? ↦ título?}
socios′ = socios
películasAlquiladas′ = películasAlquiladas
reporte! = ok
└
┌ IdentificadorPelículaDuplicado
ΞVideoclub
identificador?: IdentificadorPelícula
reporte!: Report
|
identificador? ∈ dom (películas)
reporte! = Identificador_película_duplicado
└
IntroducirNuevaPelículaCompleto ≙ IntroducirNuevaPelícula ∨ IdentificadorPelículaDuplicado
Operación para registrar un nuevo socio:
┌ IntroducirNuevoSocio
ΔVideoclub
nombre?: Nombre
identificador?: IdentificadorSocio
reporte!: Report
|
identificador? ∉ dom (socios)
películas′ = películas
socios′ = socios ∪ {identificador? ↦ nombre?}
películasAlquiladas′ = películasAlquiladas
reporte! = ok
└
┌ IdentificadorSocioDuplicado
ΞVideoclub
identificador?: IdentificadorSocio
reporte!: Report
|
identificador? ∈ dom (socios)
reporte! = Identificador_socio_duplicado
└
IntroducirNuevaSocioCompleto ≙ IntroducirNuevaSocio ∨ IdentificadorSocioDuplicado
Operación que especifica el comportamiento del sistema cuando un socio alquila una película (el socio debe estar registrado y la copia de la película con determinado id no puede estar ya alquilada). La fecha que se registra en la función películasAlquiladas es la de entrega.
┌ SocioRetiraPelícula
ΔVideoclub
idSocio?: IdentificadorSocio
idPelícula?: IdentificadorPelícula
fechaDeEntrega?: Fecha
reporte!: Report
|
idSocio? ∈ dom (socios)
idPelícula? ∈ dom (películas) ∧ idPelícula? ∉ dom (películasAlquiladas)
películas′ = películas
socios′ = socios
películasAlquiladas′ = películasAlquiladas ∪ {idPelícula? ↦ (idSocio?,
fechaDeEntrega?)}
reporte! = ok
└
┌SocioInexistente
ΞVideoclub
identificador?: IdentificadorSocio
reporte!: Report
|
identificador? ∉ dom (socios)
reporte! = Socio_inexistente
└
┌PelículaInexistente
ΞVideoclub
identificador?: IdentificadorPelícula
reporte!: Report
|
identificador? ∉ dom (películas)
reporte! = Película_inexistente
└
┌PelículaYaAlquilada
ΞVideoclub
identificador?: IdentificadorPelícula
reporte!: Report
|
identificador? ∈ dom (películasAlquiladas)
reporte! = Identificador_película_duplicado
└
SocioRetiraPelículaCompleto ≙ SocioRetiraPelícula ∨ SocioInexistente ∨ PelículaInexistente ∨ PelículaYaAlquilada
Operación que tiene lugar cuando un socio devuelve una película al videoclub:
┌ DevoluciónPelícula
ΔVideoclub
idPelícula?: IdentificadorPelícula
reporte!: Report
|
idPelícula? ∈ dom (películasAlquiladas)
películas′ = películas
socios′ = socios
películasAlquiladas′ ={idPelícula?} ⩤ películasAlquiladas
reporte! = ok
└
┌PelículaNoAlquilada
ΞVideoclub
identificador?: IdentificadorPelícula
reporte!: Report
|
identificador? ∉ dom (películasAlquiladas)
reporte! = Película_no_alquilada
└
DevoluciónPelículaCompleto ≙ DevoluciónPelícula ∨ PelículaNoAlquilada
Operación que avisa de los socios con copias a devolver un día determinado:
┌ AvisoDiarioDevoluciones
ΞVideoclub
fechaDeHoy?: Fecha
sociosQueEntreganHoy!: ℙ {s:IdentificadorSocio ⦁ s}
reporte!: Report
|
sociosQueEntreganHoy! = {s:IdentificadorSocio | (s, fechaDeHoy?) ∈ ran
(películasAlquiladas)}
reporte! = ok
└
Operación para dar de baja un socio (sólo si ha devuelto todas sus películas alquiladas):
┌ EliminarSocio
ΔVideoclub
idSocio?: IdentificadorSocio
reporte!: Report
|
idSocio? ∈ dom (socios)
¬(∃f:Fecha ⦁ (idSocio?,f) ∈ ran (películasAlquiladas))
películas′ = películas
socios′ = {idSocio?} ⩤ socios
películasAlquiladas′ = películasAlquiladas
reporte! = ok
└
┌ SocioConPelículasSinDevolver
ΞVideoclub
idSocio?: IdentificadorSocio
reporte!: Report
|
∃f:Fecha ⦁ (idSocio?,f) ∈ ran (películasAlquiladas)
reporte! = Socio_con_películas_sin_devolver
└
EliminarSocioCompleto ≙ EliminarSocio ∨ SocioInexistente ∨SocioConPelículasSinDevolver
Esquema de la operación que permite dar de baja una copia del videoclub (para ello la copia no puede estar alquilada):
┌ EliminarPelícula
ΔVideoclub
idPelícula?: IdentificadorPelícula
reporte!: Report
|
idPelícula? ∈ dom (películas) ∧ idPelícula? ∉ dom (películasAlquiladas)
películas′ = {idPelícula?} ⩤ películas
socios′ = socios
películasAlquiladas′ = películasAlquiladas
reporte! = ok
└
EliminarPelículaCompleto ≙ EliminarPelícula ∨ PelículaYaAlquilada ∨ PelículaInexistente
