[Practico 7] Pre/Post condiciones con mapas parciales

Re: [Practico 7] Pre/Post condiciones con mapas parciales

de Carlos Luna -
Número de respuestas: 0

Hola Tomás.

Podés escribir por ejemplo: 

... exists (ma : madd) (p : page), va_mapped_to_ma s va ma /\ memory s ma = Some p /\ is_RW (page_content p) ...

Saludos, Caros