De Wikipedia, la enciclopedia libre
Saltar a navegación Saltar a búsqueda
Dafny
ParadigmaImperativo , funcional
Diseñada porK. Rustan M. Leino
DesarrolladorInvestigación de Microsoft
Apareció por primera vez2009 ; Hace 12 años ( 2009 )
Lanzamiento estable
3.0.0 / 3 de febrero de 2021 ; hace 3 meses ( 03/02/2021 )
Disciplina de mecanografíaEstático, fuerte, seguro
LicenciaLicencia MIT
Extensiones de nombre de archivo.dfy
Sitio webinvestigación .microsoft .com / dafny

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] ).

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 [ editar ]

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 modifiescláusula. Dafny también proporciona una gama de tipos de colecciones inmutables que incluyen: secuencias (por ejemplo seq<int>), conjuntos (por ejemplo set<int>) y mapas ( map<int,int>). Además, se proporcionan matrices mutables (por ejemplo array<int>).

Características imperativas [ editar ]

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 ;  //  mientras ( i  <  arr .Longitud )  // Sangría como máximo arr.Length (necesario para mostrar i == arr.Length después del bucle)  invariante  ( i <= arr . Longitud );  // 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 el  invariante  máximo ( 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 requiresy ensures(respectivamente). Asimismo, la invariante de bucle y la variante de bucle se dan a través de las cláusulas invarianty decreases(respectivamente).

Invariantes de bucle [ editar ]

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]) >= 0mantenga en la asignación. Desde la condición previa, intuitivamente, se forall i :: 0 <= i < arr.Length ==> arr[i] >= 0mantiene en el bucle ya que arr[i] := arr[i];es un NOP . Sin embargo, esta asignación hace que Dafny la trate arrcomo 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 >= 0también se requiere ya que la variable iestá 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 [ editar ]

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 functiono method(como se muestra arriba) no son inusuales para herramientas de esta naturaleza, Dafny también permite la prueba de propiedades entre uno functiony 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í, NatSumLemmademuestra una propiedad útil entre sum() y isNatList()(es decir, eso isNatList(l) ==> (sum(l) >= 0)). El uso de a ghost methodpara 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 matchdeclaraciones y los casos no inductivos a menudo se descargan automáticamente. El verificador también debe tener acceso completo a los contenidos de un functiono predicatepara desenrollarlos según sea necesario. Esto tiene implicaciones cuando se usa junto con modificadores de acceso . Específicamente, ocultar el contenido de un functionuso de laprotected El modificador puede limitar las propiedades que se pueden establecer al respecto.

Referencias [ editar ]

  1. ^ 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 .
  2. ^ 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 .
  3. ^ 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 .
  4. ↑ 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 . 
  5. ^ 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 . 
  6. ^ 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 .  
  7. ^ "Página de inicio de Z3" . 2019-02-07.
  8. ↑ 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 .

Lectura adicional [ editar ]

  • 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 [ editar ]

  • 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