Dafny

Dafny es un lenguaje compilado imperativo enfocado a C# y permite especificación formal a través de precondiciones, postcondiciones, invariantes de bucles y variantes de bucles. El lenguaje combina ideas principalmente de los paradigmas funcional e imperativo, e incluye soporte limitado para Programación Orientada a Objetos. Las características incluyen genéricos, asignación dinámica, tipos de datos inductivos y una variación de lógica de separación conocida como marcos implícitos dinámicamente​ para inferencia de efectos colaterales.​ Dafny fue creado por Rustan Leino en Microsoft Research tras su trabajo previo desarrollando ESC/Modula-3, ESC/Java, y Spec#. Dafny es empleado ampliamente en la enseñanza y aparece regularmente en competiciones de verificación de software (p. ej. VSTTE'08,​ VSCOMP'10,​ COST'11,​ y VerifyThis'12​).

Dafny fue diseñado para proporcionar una introducción simple a la especificación formal y la verificación y ha sido empleado ampliamente en la enseñanza. Dafny sigue la línea de muchas herramientas previas, incluyendo SPARK/Ada, ESC/Java, Spec#, Whiley, Why3​ y Frama-C. Estas herramientas dependen del uso de probado automático de teoremas para desempeñar obligaciones de prueba, a diferencia de, por ejemplo, aquellas basadas en tipos dependientes (p. ej. Idris, Agda) que requieren mayor intervención humana. Dafny se compila en el lenguaje intermediario Boogie, que usa el probador automático de teoremas Z3​​ para desempeñar obligaciones de prueba.

Tipos de datos

Dafny proporciona métodos para implementaciones que puedan tener efectos secundarios y funciones para uso en especificaciones puras que sean puras. Los métodos consisten en secuencias de sentencias que siguen un estilo imperativo conocido mientras que, en contraste, el cuerpo de una función es simplemente una expresión. Cualquier sentencia con efectos secundarios en un método (p. ej. asignar un elemento de un parámetro array) debe tenerse en cuenta señalando qué parámetros pueden ser alterados en la cláusula modifies. Dafny proporciona también un rango de tipos de colecciones inmutables incluyendo: secuencias (p. ej. seq<int>), conjuntos (p. ej. set<int>) y mapas (map<int,int>). Adicionalmente, se proporcionan arrays mutables (p. ej. array<int>).

Características imperativas

Dafny permite pruebas de programas imperativos basados en ideas de lógica de Hoare. Lo siguiente ilustra numerosas características de Dafny, incluyendo el uso de precondiciones, postcondiciones, invariantes de bucle y variantes de bucle.

method max(arr:array<int>) returns(max:int)
 // El array debe tener al menos un elemento
 requires arr!=null && arr.Length > 0;
 // El retorno no puede ser más pequeño que ningún elemento del array
 ensures (forall j :int :: (j >= 0 && j < arr.Length ==> max >= arr[j]));
 // El retorno debe coincidir con algún elemento del array
 ensures (exists j : int :: j>=0 && j < arr.Length && max==arr[j]);
{
  max:=arr[0];
  var i:int :=1;
  //
  while(i < arr.Length)
  // Alcanzar a lo sumo arr.Length (needed to show i==arr.Length after loop)
  invariant (i<=arr.Length);
  // Ningún elemento hasta el momento es mayor que max
  invariant (forall j:int :: j>=0 && j<i ==> max >= arr[j]);
  // Algún elemento coincide con max
  invariant (exists j:int :: j>=0 && j<i && max == arr[j]);
  // Terminar cuando i == arr.Length
  decreases (arr.Length-i); 
  {
    // Actualizar max si se ha encontrado un elemento mayor
    if(arr[i] > max){max := arr[i];}
    // Continuar a través del array
    i := i + 1;
  }
}

Este ejemplo obtiene el mayor elemento de un array. La precondición y postcondición del método se dan con las cláusulas requires y ensures (respectivamente). Así mismo, el  invariante y el variante del bucle se dan con las cláusulas invariant y decreases (respectivamente).

Invariantes de bucle

El tratamiento de invariantes de bucles en Dafny difiere de la lógica de Hoare tradicional.  Las variables alteradas en un bucle son tratadas de manera que (la mayor parte de) la información conocida sobre ellas previa al bucle es descartada. La información requerida para probar propiedades de estas variables debe estar expresada explícitamente en el invariante del bucle. En contraposición, se conserva toda la información conocida de antemano de las variables no alteradas en el bucle. He aquí una muestra: Esta verificación falla porque Dafny no puede establecer que (suma + arr[i]) >= 0  se mantiene en la asignación. De la precondición, intuitivamente, forall i :: 0 <= i < arr.Length ==> arr[i] >= 0 se mantiene en el bucle dado quearr[i] := arr[i]; es una NOP. Sin embargo, esta asignación prove que Dafny trate arr como una variable alterable y prescinda de información conocida sobre ella previa al bucle. Para verificar este programa en Dafny podemos: eliminar la asignación redundante arr[i] := arr[i];; o bien, añadir el invariante de bucle invariant forall i :: 0 <= i < arr.Length ==> arr[i] >= 0

Dafny adicionalmente emplea un limitado análisis estático para inferir invariantes de bucle simples cuando sea posible. En el ejemplo anterior, podría parecer que el invariante de bucle invariant i >= 0 es necesario dado que i es alterada en el bucle. Si bien la lógica interna requiere dicho invariante, Dafny lo infiere automáticamente y, por lo tanto, puede ser omitido a nivel de código.

Características de prueba

Dafny incluye características que apoyan su uso más allá de la verificación asistida.Mientras que las pruebas de propiedades sencillas dentro de function o method (como se muestra arriba) no son inusuales en herramientas de este tipo, Dafny también permite realizar pruebas entre una función y otra. Como es común para un asistente de verificación, tales pruebas son a menudo inductivas de manera natural. Dafny es quizás inusual al emplear invocación de métodos como mecanismo para aplicar hipótesis inductivas. He aquí una muestra:

datatype List = Nil | Link(dato:int,siguiente:List)

function suma(l:List): int {
  match l
    case Nil => 0
    case Link(d,n) => d + suma(n)
}

predicate esListaNat(l:List) {
  match l
    case Nil => true
    case Link(d,n) => d >= 0 && esListaNat(n)
}

ghost method sumaNatLema(l:List, n:int)
requires esListaNat(l) && n == suma(l)
ensures n >= 0 
{
  match l
    case Nil =>
      // Realizado automáticamente
    case Link(dato,siguiente) => {
      // Aplicar hipótesis de inducción
      NatSumLemma(siguiente,suma(siguiente));
      // Comprobar lo que Dafny sabe
      assert dato >= 0;
    }
}

Aquí, sumaNatLema prueba una propiedad útil entre suma() y esListaNat() (i.e. que esListaNat(l) ==> (suma(l) >= 0)). El uso de un ghost method para codificar lemas y teoremas es estándar en Dafny con la recursión empleada para inducción (habitualmente, inducción estructural). El análisis de casos es llevado a cabo empleando sentencias match y los casos no inductivos son a menudo realizados automáticamente. El verificador debe tener también acceso completo a los contenidos de una  function o predicate para desarrollarlos cuando sea necesario. Esto tiene implicaciones cuando se emplea conjuntamente con modificadores de acceso. Específicamente, ocultar los contenidos de una function utilizando el modificador protected puede limitar lo que se puede establecer acerca de las propiedades.

Referencias

• Datos: Q48989398