Siguiendo el paper, el tipo os (usado como codominio del map os_map) es un record en donde un campo es option Hyper_call.
No me queda claro qué cómo definir el tipo Hyper_call. Por el contexto la semántica es que debería de ser una suma (un 'enumerado'), pero no se con qué contenido.
Hola.
Para el caso de estudio del práctico 7 alcanzaría con poner:
Parameter Hyper_call: Set.
No es necesario que formalicen las diferentes hypercalls, que podrían definirse en Coq, por ejemplo, de la siguiente manera:
Inductive Hyper_call: Set :=
| Hyperv_call_new : vadd -> padd -> Hyperv_call
| Hyperv_call_del : vadd -> Hyperv_call
| Hyperv_call_lswitch : padd -> Hyperv_call
| Hyperv_call_unpin : padd -> Hyperv_call
| Hyperv_call_pin : padd -> ptype -> Hyperv_call.
Saludos, Carlos
Hola,
¿Es correcto utilizar el parámetro que viene en la plantilla?
Parameter Hyperv_call: Set.
Yo entendí que los Hyper_call eran estos, que no había que definir otro parámetro.
Saludos,
Jairo.
Sí! yo lo vi después de hacer la pregunta!
Es correcto.
saludos, Carlos