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 ala 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 illustra 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)
 // Array must have at least one element
 requires arr!=null && arr.Length > 0;
 // Return cannot be smaller than any element in array
 ensures (forall j :int :: (j >= 0 && j < arr.Length ==> max >= arr[j]));
 // Return must match some element in array
 ensures (exists j : int :: j>=0 && j < arr.Length && max==arr[j]);
{
  max:=arr[0];
  var i:int :=1;
  //
  while(i < arr.Length)
  // Indent at most arr.Length (needed to show i==arr.Length after loop)
  invariant (i<=arr.Length);
  // No element seen so far larger than max
  invariant (forall j:int :: j>=0 && j<i ==> max >= arr[j]);
  // Some element seen so far matches max
  invariant (exists j:int :: j>=0 && j<i && max == arr[j]);
  // Terminate when i == arr.Length
  decreases (arr.Length-i); 
  {
    // Update max if larger element encountered
    if(arr[i] > max){max := arr[i];}
    // Continue through 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 tante, 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(data:int,next:List)

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

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

ghost method NatSumLemma(l:List, n:int)
requires isNatList(l) && n == sum(l)
ensures n >= 0 
{
  match l
    case Nil =>
      // Discharged Automatically
    case Link(data,next) => {
      // Apply Inductive Hypothesis
      NatSumLemma(next,sum(next));
      // Check what known by Dafny
      assert data >= 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 acabo 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.