Buenas,
No entiendo bien qué es lo que hay que hacer en este ejercicio.
¿Tenemos que probar la especificación? ¿O hay que escribir el algoritmo?
O capaz primero hay que escribir el algoritmo y después probar la especificación como en los ejercicios anteriores.
Saludos,
Joaquín
Hola Joaquín.
La idea es realizar la prueba siguiendo los pasos lógicos sugeridos por el algoritmo dado en pseudocódigo. Luego, se puede extraer un código correcto por construcción.
Definition nat_div_mod : forall a b,
~ (b = 0) -> { qr | spec_res_nat_div_mod a b qr }.
Proof.
intros. unfold spec_res_nat_div_mod. induction a.
...
Qed.
Extraction "natdivmod" nat_div_mod.
Saludos, Carlos
