[Práctico 7] Ejercicio 6

[Práctico 7] Ejercicio 6

de Julian Tricanico Gadea -
Número de respuestas: 6

Buenas,

Estoy tratando de probar one_step_preserves_prop_iii. Lo estoy haciendo por inducción en la acción a.

Estoy en el caso del write y lo que me está costando en particular es probar que se cumple    trusted_os ctxt s    a partir de    trusted_os ctxt s' .

Yo por cierto one-step execution lo definí como

Definition one_step s a s' := valid_state s /\ Pre s a /\ Post s a s'
pero en la plantilla recomiendan usar Inductive en lugar de Definition que me hace dudar un poco. Pero es lo que interpreto directamente de:

valid_state(s)    Pre s a    Post s a s'
----------------------------------------
                 a ⇒ s ↪ s'

Voy bien encaminado? Alguna idea para lo de trusted_os ctxt ?

Saludos!

En respuesta a Julian Tricanico Gadea

Re: [Práctico 7] Ejercicio 6

de Carlos Luna -

Hola

Tenés que probar cosas para s' partir de cosas en s y no al revés.

Vas bien encaminado según tu pregunta.

La preservación de la prop iii para write debería salir esencialmente de las cosas que se mantienen de s a s' (igualdades).

Saludos, Carlos

En respuesta a Carlos Luna

Re: [Práctico 7] Ejercicio 6

de Julian Tricanico Gadea -
> Tenés que probar cosas para s' a partir de cosas en s y no al revés.
Claro, el tema es que como yo lo escribí,
    trusted_os ctxt s
está en las hipótesis de valid_state_iii s, que es un implica, entonces "se dan vuelta"; pero la tésis que es aos_exec_mode s' = svc, estoy de acuerdo que es sobre s', y asumo de hipótesis aos_exec_mode s = svc.


> Vas bien encaminado según tu pregunta.
Bien, demás, gracias.
Saludos!
En respuesta a Julian Tricanico Gadea

Re: [Práctico 7] Ejercicio 6

de Bruno Lartigau Antonini -
Buenas, en mi caso llegué a un punto como el que Julián describió y no he podido avanzar.

Primero me gustaría confirmar si mi valid_state_iii es correcto:

Definition valid_state_iii (s : State) : Prop :=
(aos_activity s = waiting \/ (trusted_os ctxt s)) -> aos_exec_mode s = svc.

De ser correcto, cualquier ayuda para resolver el caso de trusted_os ctxt s es bienvenida.

Saludos!
En respuesta a Bruno Lartigau Antonini

Re: [Práctico 7] Ejercicio 6

de Carlos Luna -

Hola.

Con la formalización de abajo la prueba se puede hacer sin problemas:

Definition valid_state_iii (s : State) : Prop :=

    ((trusted_os ctxt s /\ aos_activity s = running) (* trusted os running *)

     \/ aos_activity s = waiting) (* hypervisor running *)

    -> aos_exec_mode s = svc.

Tener presente que en cada acción lo que no cambia hay que explicitarlo en su postcondición. Esto es, entre el estado previo y posterior a la ejecución de una acción la mayoría de las cosas se deben mantener (ser explícitamente iguales).

Saludos, Carlos

En respuesta a Bruno Lartigau Antonini

Re: [Práctico 7] Ejercicio 6

de Julian Tricanico Gadea -
Nosotros usamos exactamente la definición que dijo Carlos, y tal vez en retrospectiva un poco trivial, pero recomiendo para la prueba notar que trusted_os depende de active_os.