Formulario de Lógica de Hoare — Q1
Objetivo
Hoja tamaño carta horizontal que condensa la notación de las Notas 4–6 del profesor, las reglas de inferencia y el procedimiento mínimo para resolver ejercicios de asignación, composición, condicionales y ciclos.
La hoja incluye la convención del curso (Q_E^V\equiv Q[E/V]), la aserción vacía ({\ }=\top), las condiciones de verificación de un ciclo y las variantes usadas para demostrar terminación. La idea operativa es: ejecutar hacia delante, verificar hacia atrás.