Especificación en Z de guardar_op

VELOCIDAD ::= nula | sin_cambio

COSECHA ::= detenida | no_cambia

MODO ::= prueba | normal

MENSAJE ::= si | no

[OPERACION]

ESPACIO == N

®tamaño: OPERACION f ESPACIO

®guardar_op: MODO x ESPACIO x OPERACION
® f OPERACION x MENSAJE x VELOCIDAD x COSECHA
Ç_______________
® Am: MODO; e: ESPACIO; o: OPERACION ¥
® guardar_op (m, e, o) =
® if m = prueba
® then if tamaño o ø e
® then (o, no, sin_cambio, no_cambia)
® else (o, si, nula, detenida)
® else (o, no, sin_cambio, no_cambia)

Recibe una operación a registrar y, dependiendo del modo en que funcione el sistema, chequea (o no) si el espacio disponible en disco es suficiente para almacenarla. Si es así guarda la operación, si no, si el modo es PRUEBA detiene la cosecha. La función sin especificar tamaño determina, dada una operación, el espacio que ésta requiere para ser guardada.

GDES

Cálculo DFC