Funciones que deben aparecer fuera de las anotaciones
Estoy siguiendo el tutorial en línea de Dafny (https://dafny-lang.github.io/dafny/OnlineTutorial/guide). Justo después del Ejercicio, se menciona que las funciones solo pueden aparecer en anotaciones. Por lo tanto, no se puede escribir:
var v := abs(3);
El tutorial también menciona que a veces es conveniente usar una función en código real, por lo que se puede definir un método de función, que se puede llamar desde el código real.
Entonces, en el Ejercicio 5, esto es lo que he escrito:
function max(a: int, b: int): int
{
if a < b then b else a
}
method Testing() {
var a := 3;
var b := 4;
var c := max(a,b); //parece que Dafny acepta este programa a diferencia de lo que se dijo en el tutorial
assert a <= c && b <= c;
}
Esperaba un error en la línea
var c := max(a,b);
Sin embargo, no recibí ningún error.
Por otro lado, en el Ejercicio 6, cuando tengo el siguiente código:
function abs(x: int): int
{
if x < 0 then -x else x
}
method Abs(x: int) returns (y: int)
ensures y == abs(x);
{
y := abs(x);
}
Tengo el error en la línea:
y := abs(x);
que indica que “las llamadas a funciones solo están permitidas en contextos de especificación (considere declarar la función como ‘function method’)”.
Después de cambiar la línea function abs(x: int): int a function method abs(x: int): int, el error desaparece.
¿Puedo verificar por qué funciona en el Ejercicio 5 pero no en el Ejercicio 6?
De todos modos, también puedo verificar qué significa cuando usan el término “código real” en la frase “usar una función en el código real”.
Gracias.
davy.ai
Como se menciona en el tutorial en línea de Dafny, las funciones solo pueden aparecer en anotaciones. Sin embargo, en el Ejercicio 5, el usuario definió una función llamada “max” y pudo llamarla desde código real sin errores. Esto se debe a que Dafny permite el uso de métodos de funciones, que son métodos que solo contienen pre- y postcondiciones y se comportan como funciones puras. Por lo tanto, cuando el usuario definió la función “max” como un método de función, pudo ser utilizada en código real sin errores.
Sin embargo, en el Ejercicio 6, el usuario definió una función llamada “abs” e intentó llamarla desde código real sin declararla como un método de función. Esto resultó en un error que indicaba que las llamadas a funciones solo están permitidas en contextos de especificación. Esto se debe a que Dafny no permite el uso de funciones en código real a menos que se declaren como métodos de función.
En cuanto al término “código real”, se utiliza para referirse al código de implementación real en un programa, en contraste con las pre- y postcondiciones utilizadas en las anotaciones de Dafny.