search

alexgadea / fun

Derivador de programas a partir de especificaciones.
GNU General Public License v3.0
1 stars 0 forks source link

Nueva clase de declaración #18

Open alexgadea opened 8 years ago

alexgadea commented 8 years ago

Se me ocurre que podría estar bueno tener nuevas declaraciones del estilo de Ejemplo y Contra-Ejemplo (así como tenemos thm, spec, prop, etc.) con el fin de poder asignar valor a las variables y confirmar el valor de verdad que pensamos que la proposición tiene para tales asignaciones.

Como ejemplo de utilidad, permitiría resolver ejercicios del estilo: Decidí si cada una de las siguientes fórmulas proposicionales son válidas o no. En todos los casos justificá con una demostración o un contraejemplo, según corresponda

Propuesta rápida de sintaxis ("basada en los parsers que tenemos"): let c-example cex1 = p ≡ q begin assign p = True q = False end assign

miguelpagano commented 8 years ago

¿Qué chequeo se hace para estas nuevas declaraciones? Lo primero que se me ocurre es para los contra-ejemplos se chequea que con la asignación dada la expresión evalúa a False. ¿Esa es la idea?

alexgadea commented 8 years ago

Sí sí, tal cual :)

En el contexto del ejercicio, tal vez la contra de tener esto es que uno puede llegar a "resolver" el problema empezando a probar distintas asignaciones sin pensar (siempre que la cantidad de variables lo permita :yum:).