¡Muy contento!

Después de algunos días construyendo un parser y definiendo una sintáxis abstracta, empecé a definir la semántica a través de traducciones a lógica.

Todavía no soporto ciclos, pero hace apenas 5 minutos pude demostrar la correctitud del siguiente programa, muy básico, pero algo al fin...

f(in a, out b)
:? a != 0
:! b > 10
{
____b <- 0
____c <- not a
____if a then {
________if c then {
________} else {
____________b <- b + 5
________}
________b <- b + 5
____} else {
________b <- b + 1
____}
____b <- b + 1
}