Dafny es un lenguaje compilado imperativo que se dirige a C # y admite la especificación formal a través de precondiciones , poscondiciones , invariantes de bucle y variantes de bucle . El lenguaje combina ideas principalmente de los paradigmas funcional e imperativo e incluye un soporte limitado para la programación orientada a objetos . Las características incluyen clases genéricas , asignación dinámica , tipos de datos inductivos y una variación de la lógica de separación conocida como tramas dinámicas implícitas[1] por razonar sobre los efectos secundarios. [2] Dafny fue creado por Rustan Leino en Microsoft Research después de su trabajo anterior en el desarrollo de ESC / Modula-3, ESC / Java y Spec # . Dafny se usa ampliamente en la enseñanza y se presenta regularmente en concursos de verificación de software (por ejemplo, VSTTE'08, [3] VSCOMP'10, [4] COST'11, [5] y VerifyThis'12 [6] ).
Paradigma | Imperativo , funcional |
---|---|
Diseñada por | K. Rustan M. Leino |
Desarrollador | Investigación de Microsoft |
Apareció por primera vez | 2009 |
Lanzamiento estable | 3.0.0 / 3 de febrero de 2021 |
Disciplina de mecanografía | Estático, fuerte, seguro |
Licencia | Licencia MIT |
Extensiones de nombre de archivo | .dfy |
Sitio web | investigación |
Dafny fue diseñado para proporcionar una introducción simple a la especificación y verificación formales y se ha utilizado ampliamente en la enseñanza. Dafny se basa en el lenguaje intermedio Boogie que utiliza el demostrador de teoremas automatizado Z3 para cumplir con las obligaciones de prueba. [7] [8]
Tipos de datos
Dafny proporciona métodos de implementación que pueden tener efectos secundarios y funciones para usar en especificaciones que son puras . Los métodos consisten en secuencias de enunciados que siguen un estilo imperativo familiar, mientras que, por el contrario, el cuerpo de una función es simplemente una expresión. Cualquier declaración que tenga efectos secundarios en un método (por ejemplo, la asignación de un elemento de un parámetro de matriz) debe tenerse en cuenta señalando qué parámetros se pueden modificar en la modifies
cláusula. Dafny también proporciona una gama de tipos de colecciones inmutables que incluyen: secuencias (p seq
. Ej. ), Conjuntos (p set
. Ej. ) Y mapas ( map
). Además, se proporcionan matrices mutables (por ejemplo array
).
Características imperativas
Dafny apoya pruebas de programas imperativos basados en las ideas de la lógica de Hoare . A continuación se ilustran muchas de estas características en Dafny, incluido el uso de precondiciones, poscondiciones, invariantes de bucle y variantes de bucle.
método max ( arr : arreglo < int > ) devuelve ( max : int ) // El arreglo debe tener al menos un elemento requiere arr ! = null && arr . Longitud > 0 ; // El retorno no puede ser más pequeño de lo que asegura cualquier elemento en la matriz ( forall j : int :: ( j > = 0 && j < arr . Length ==> max > = arr [ j ] )); // El retorno debe coincidir con algún elemento de la matriz asegura ( existe j : int :: j > = 0 && j < arr . Length && max == arr [ j ] ); { max : = arr [ 0 ] ; var i : int : = 1 ; // while ( i < longitud de arr . ) // Sangría como máximo arr.Length (necesario para mostrar i == arr.Length después del bucle) invariante ( i <= longitud de arr . ); // Ningún elemento visto hasta ahora más grande que max invariante ( forall j : int :: j > = 0 && j < i ==> max > = arr [ j ] ); // Algún elemento visto hasta ahora coincide con max invariant ( existe j : int :: j > = 0 && j < i && max == arr [ j ] ); // Termina cuando i == arr.Length disminuye ( arr . Length - i ); { // Actualizar max si se encuentra un elemento más grande if ( arr [ i ] > max ) { max : = arr [ i ] ;} // Continuar a través de la matriz i : = i + 1 ; } }
Este ejemplo calcula el elemento máximo de una matriz. La precondición y la poscondición del método se dan con las cláusulas requires
y ensures
(respectivamente). Asimismo, la invariante de bucle y la variante de bucle se dan a través de las cláusulas invariant
y decreases
(respectivamente).
Invariantes de bucle
El tratamiento de los invariantes de bucle en Dafny difiere de la lógica tradicional de Hoare . Las variables mutadas en un bucle se tratan de tal manera que se descarta (la mayor parte) de la información conocida sobre ellas antes del bucle. La información requerida para probar las propiedades de tales variables debe expresarse explícitamente en el ciclo invariante. Por el contrario, las variables no mutadas en el bucle retienen toda la información conocida sobre ellas de antemano. Lo siguiente proporciona ilustra:
método sumAndZero ( ns : array < int > ) devuelve ( sum : nat ) requiere ns ! = null requiere forrall i :: 0 <= i < ns . Longitud ==> ns [ i ] > = 0 modifica ns { var i : int : = 0 ; var arr : matriz < int > : = ns ; // porque no se pueden asignar parámetros sum : = 0 ; // while ( i < longitud de arr . ) { suma : = suma + arr [ i ] ; arr [ i ] : = arr [ i ] ; yo : = yo + 1 ; } }
Esto falla en la verificación porque Dafny no puede establecer que se (sum + arr[i]) >= 0
mantenga en la asignación. Desde la condición previa, intuitivamente, se forall i :: 0 <= i < arr.Length ==> arr[i] >= 0
mantiene en el bucle ya que arr[i] := arr[i];
es un NOP . Sin embargo, esta asignación hace que Dafny la trate arr
como una variable mutable y elimine información conocida sobre ella desde antes del ciclo. Para verificar este programa en Dafny podemos: eliminar la asignación redundante arr[i] := arr[i];
; o, agregue el ciclo invarianteinvariant forall i :: 0 <= i < arr.Length ==> arr[i] >= 0
Dafny además emplea un análisis estático limitado para inferir invariantes de bucle simple cuando sea posible. En el ejemplo anterior, parecería que el invariante de bucle invariant i >= 0
también se requiere ya que la variable i
está mutada dentro del bucle. Si bien la lógica subyacente requiere tal invariante, Dafny automáticamente infiere esto y, por lo tanto, se puede omitir en el nivel de fuente.
Funciones de prueba
Dafny incluye funciones que respaldan aún más su uso como asistente de pruebas . Si bien las pruebas de propiedades simples dentro de un function
o method
(como se muestra arriba) no son inusuales para herramientas de esta naturaleza, Dafny también permite la prueba de propiedades entre uno function
y otro. Como es común para un asistente de pruebas , tales pruebas son a menudo de naturaleza inductiva . Dafny es quizás inusual al emplear la invocación de métodos como mecanismo para aplicar la hipótesis inductiva. Lo siguiente ilustra:
Lista de tipos de datos = Nulo | Enlace ( datos : int , siguiente : Lista )función suma ( l : Lista ): int { coincide con l caso Nil => 0 caso Enlace ( d , n ) => d + suma ( n ) }predicado isNatList ( l : List ) { match l case Nil => true case Link ( d , n ) => d > = 0 && isNatList ( n ) }El método fantasma NatSumLemma ( l : List , n : int ) requiere isNatList ( l ) && n == sum ( l ) asegura n > = 0 { coincide con l case Nil => // Descargado automáticamente case Link ( data , next ) => { // Aplicar hipótesis inductiva NatSumLemma ( siguiente , suma ( siguiente )); // Verifica lo que sabe Dafny aseverar datos > = 0 ; } }
Aquí, NatSumLemma
demuestra una propiedad útil entre sum()
y isNatList()
(es decir, eso isNatList(l) ==> (sum(l) >= 0)
). El uso de a ghost method
para codificar lemas y teoremas es estándar en Dafny con la recursividad empleada para la inducción (típicamente, inducción estructural ). El análisis de casos se realiza mediante match
declaraciones y los casos no inductivos a menudo se descargan automáticamente. El verificador también debe tener acceso completo a los contenidos de un function
o predicate
para desenrollarlos según sea necesario. Esto tiene implicaciones cuando se usa junto con modificadores de acceso . Específicamente, ocultando el contenido de un function
utilizando el protected
modificador puede limitar qué propiedades se pueden establecer sobre él.
Referencias
- ^ Smans, enero; Jacobs, Bart; Piessens, Frank (2009). Marcos dinámicos implícitos: combinación de marcos dinámicos y lógica de separación (PDF) . Actas de la Conferencia sobre la Conferencia Europea de Programación Orientada a Objetos. págs. 148-172. doi : 10.1007 / 978-3-642-03013-0_8 .
- ^ Leino, Rustan (2010). Dafny: un verificador automático de programas para la corrección funcional . Actas de la Jornada de Lógica para Programación, Inteligencia Artificial y Razonamiento. págs. 348–370. doi : 10.1007 / 978-3-642-17511-4_20 .
- ^ Leino, Rustan; Monahan, Romero (2010). Dafny cumple el desafío de los puntos de referencia de verificación (PDF) . Conferencia internacional sobre software verificado: teorías, herramientas y experimentos. págs. 112-116. doi : 10.1007 / 978-3-642-15057-9_8 .
- ^ Klebanov, Vladimir; et al. (2011). El primer concurso de software verificado: Informe de experiencia . Actas de la Conferencia sobre métodos formales. págs. 154-168. CiteSeerX 10.1.1.221.6890 . doi : 10.1007 / 978-3-642-21437-0_14 .
- ^ Bormer, Thorsten; et al. (2011). Concurso de verificación COST IC0701 2011 . Actas de la conferencia sobre verificación formal de software orientado a objetos. págs. 3-21. CiteSeerX 10.1.1.396.6170 . doi : 10.1007 / 978-3-642-31762-0_2 .
- ^ Huisman, Marieke; Klebanov, Vladimir; Monahan, Romero (2015). "VerifyThis 2012: un concurso de verificación de programas" (PDF) . Revista de herramientas de software para la transferencia de tecnología . 17 (6): 647–657. doi : 10.1007 / s10009-015-0396-8 . S2CID 14301377 .
- ^ "Página de inicio Z3" . 2019-02-07.
- ^ de Moura, Leonardo; Bjørner, Nikolaj (2008). Z3: un solucionador SMT eficiente . Actas de la Jornada sobre Herramientas y Algoritmos para la Construcción y Análisis. págs. 337–340. doi : 10.1007 / 978-3-540-78800-3_24 .
Otras lecturas
- Meyer, Bertrand; Nordio, Martin, eds. (2012). Herramientas para la verificación práctica de software: Escuela de verano internacional, LASER 2011, Isla de Elba, Italia, Conferencias tutoriales revisadas . Springer . ISBN 978-3642357459.
enlaces externos
- Dafny: un verificador de programas y lenguaje para la corrección funcional - Microsoft Research
- GitHub - dafny-lang / dafny: Dafny es un lenguaje de programación consciente de la verificación