Hola, me queda una duda de si en estas reglas es necesario pedir que el identificador del SO esté en el mapeo oss : os_indet -> os del estado, o alcanza con utilizarlo así nomás de la forma:
forall (osi : os_ident)...
Y ahí pedir las condiciones necesarias con ese identificador, sin pedir que el identificador esté en el mapeo oss : os_indet -> os del estado. (Siempre que no necesitemos acceder a la estructura os)
Saludos,
Jairo.
[Práctico 7] Reglas V y VI valid state (mapeo oss : os_indet -> os)
Número de respuestas: 1
En respuesta a Jairo Yamil Bonanata Silva
Re: [Práctico 7] Reglas V y VI valid state (mapeo oss : os_indet -> os)
de Carlos Luna -
Hola.
La segunda alternativa está bien (forall (osi : os_ident)...).
Saludos, Carlos