Buenas, quería saber si los siguientes mapas deberían ser parciales:
- El codominio de hypervisor_map
- El mapa vadd -> madd de una Page Table
- oss_map
Hola.
Si, son mappings parciales. Pueden usar para esto el tipo option (totalizando la función); por ejemplo:
Definition partial a b := a -> option b.
Notation "a ⇸ b" := (partial a b) (at level 51, right associativity).
La memoria también sería una mapping parcial y para que vean la forma de trabajar con el tipo option copio abajo el ejemplo del update de la memoria:
Definition system_memory := madd ⇸ page.
Definition update mem addr page : system_memory :=
fun addr' => if madd_eq addr' addr
then Some page
else mem addr'.
Esta es una forma de trabajar, pero no la única.
Saludos, Carlos