Whiley es un lenguaje de programación experimental que combina características de los paradigmas funcional e imperativo , y admite la especificación formal a través de precondiciones de función , poscondiciones e invariantes de bucle . [1] El lenguaje utiliza tipado sensible al flujo también conocido como "tipado de flujo".
El proyecto Whiley comenzó en 2009 como respuesta al "Gran desafío del compilador verificador" propuesto por Tony Hoare en 2003. [2] El primer lanzamiento público de Whiley fue en junio de 2010. [3]
Whiley es un proyecto de código abierto desarrollado principalmente por David Pearce y que cuenta con la colaboración de una pequeña comunidad. El sistema se ha utilizado en proyectos de investigación de estudiantes y en la enseñanza de clases de grado. [4] Entre 2012 y 2014 recibió el apoyo del Fondo Marsden de la Royal Society of New Zealand. [5]
El compilador Whiley genera código para la máquina virtual Java y puede interoperar con Java y otros lenguajes basados en JVM.
El objetivo de Whiley es proporcionar un lenguaje de programación realista en el que la verificación se utilice de forma rutinaria y sin pensar. La idea de una herramienta de este tipo tiene una larga historia, pero se promovió con fuerza a principios de la década de 2000 a través del Gran Desafío del Compilador Verificador de Hoare . El propósito de este desafío era estimular nuevos esfuerzos para desarrollar un compilador verificador , que se describe a grandes rasgos de la siguiente manera: [6]
Un compilador verificador utiliza razonamiento matemático y lógico para comprobar la corrección de los programas que compila.
—Tony Hoare
El objetivo principal de una herramienta de este tipo es mejorar la calidad del software al garantizar que un programa cumpla con una especificación formal . Whiley sigue muchos intentos de desarrollar dichas herramientas, incluidos esfuerzos notables como SPARK/Ada , ESC/Java , Spec#, Dafny , Why3, [7] y Frama-C .
La mayoría de los intentos anteriores de desarrollar un compilador de verificación se centraron en ampliar los lenguajes de programación existentes con construcciones para escribir especificaciones. Por ejemplo, ESC/Java y el lenguaje de modelado Java añaden anotaciones para especificar condiciones previas y posteriores a Java . Del mismo modo, Spec# y Frama-C añaden construcciones similares a los lenguajes de programación C# y C. Sin embargo, se sabe que estos lenguajes contienen numerosas características que plantean problemas difíciles o insuperables para la verificación. [8] En cambio, el lenguaje Whiley se diseñó desde cero en un esfuerzo por evitar los errores comunes y hacer que la verificación fuera más manejable. [9]
La sintaxis de Whiley sigue la apariencia general de los lenguajes imperativos u orientados a objetos. Se prefiere la sintaxis de sangría en lugar del uso de llaves para delimitar los bloques de instrucciones, dada su gran similitud con Python . Sin embargo, la apariencia imperativa de Whiley es algo engañosa, ya que el núcleo del lenguaje es funcional y puro .
Whiley distingue a function(que es puro ) de a method(que puede tener efectos secundarios ). Esta distinción es necesaria ya que permite que las funciones se utilicen en especificaciones. Hay disponible un conjunto familiar de tipos de datos primitivos que incluyen bool, int, matrices (p. ej. int[]) y registros (p. ej. {int x, int y}). Sin embargo, a diferencia de la mayoría de los lenguajes de programación, el tipo de datos entero, int, no tiene límites y no corresponde a una representación de ancho fijo como el complemento a dos de 32 bits . Por lo tanto, un entero sin restricciones en Whiley puede tomar cualquier valor entero posible, sujeto a las restricciones de memoria del entorno del host. Esta elección simplifica la verificación, ya que el razonamiento sobre la aritmética modular es un problema conocido y difícil. Los objetos compuestos (p. ej. matrices o registros) no son referencias a valores en el montón como lo son en lenguajes como Java o C# sino que, en cambio, son valores inmutables .
Whiley adopta un enfoque inusual para la verificación de tipos, conocido como " Tipo de flujo ". Las variables pueden tener diferentes tipos estáticos en diferentes puntos de una función o método. El tipo de flujo es similar al tipo de ocurrencia que se encuentra en Racket . [10] Para ayudar al tipo de flujo, Whiley admite tipos de unión , intersección y negación. [11] Los tipos de unión son comparables a los tipos de suma que se encuentran en lenguajes funcionales como Haskell pero, en Whiley, no son disjuntos. Los tipos de intersección y negación se utilizan en el contexto del tipo de flujo para determinar el tipo de una variable en las ramas verdadera y falsa de una prueba de tipo en tiempo de ejecución. Por ejemplo, supongamos una variable xde tipo Ty un tipo de tiempo de ejecución test x is S. En la rama verdadera, el tipo de xse convierte T & Sen while, en la rama falsa, se convierte en T & !S.
Whiley utiliza un sistema de tipos estructural en lugar de nominal . Modula-3 , Go y Ceylon son ejemplos de otros lenguajes que admiten el tipado estructural de alguna forma.
Whiley admite tiempos de vida de referencia similares a los que se encuentran en Rust . Se pueden proporcionar tiempos de vida al asignar nuevos objetos para indicar cuándo se pueden desasignar de forma segura. Las referencias a dichos objetos deben incluir un identificador de tiempo de vida para evitar referencias colgantes . Cada método tiene un tiempo de vida implícito al que se hace referencia mediante this. Una variable de tipo &this:Trepresenta una referencia a un objeto de tipo Tque se desasigna con el método que lo encierra. La subtipificación entre tiempos de vida está determinada por la relación outlives . Por lo tanto, &l1:Tes un subtipo de &l2:Tif lifetime l1outlives statically lifetime l2. Se dice que un tiempo de vida cuyo alcance encierra otro lo sobrevive. Los tiempos de vida en Whiley difieren de Rust en que actualmente no incluyen un concepto de propiedad .
Whiley no tiene soporte integrado para concurrencia ni un modelo de memoria formal para determinar cómo debe interpretarse la lectura/escritura en un estado mutable compartido.
El siguiente ejemplo ilustra muchas de las características interesantes de Whiley, incluido el uso de poscondiciones, invariantes de bucle, invariantes de tipo, tipos de unión y tipado de flujo. La función tiene como objetivo devolver el primer índice de un entero itemen una matriz de enteros items. Si no existe dicho índice, nullse devuelve .
.svg/1280px-Free_and_open-source_software_logo_(2009).svg.png){kind=logo}
// Define el tipo de números naturales type nat es ( int x ) donde x >= 0public function indexOf ( int [] items , int item ) -> ( int | null index ) // Si se devuelve int, el elemento en esta posición coincide con el elemento asegura que el índice es int ==> items [ index ] == item // Si se devuelve int, el elemento en esta posición es la primera coincidencia asegura que el índice es int ==> no { i in 0 .. index | items [ i ] == item } // Si se devuelve null, ningún elemento en items coincide con el elemento asegura que el índice es null ==> no { i in 0 .. | items | | items [ i ] == item } : // nat i = 0 // while i < | items | // Ningún elemento visto hasta ahora coincide con el elemento donde no { j in 0 .. i | items [ j ] == item } : // if items [ i ] == item : return i i = i + 1 // return nullEn lo anterior, al tipo de retorno declarado de la función se le asigna el tipo de unión int|nullque indica que seint devuelve un valor o se devuelve. La condición posteriornull de la función se compone de tres cláusulas, cada una de las cuales describe diferentes propiedades que deben cumplirse del valor devuelto . La tipificación de flujo se emplea en estas cláusulas a través del operador de prueba de tipo en tiempo de ejecución, . Por ejemplo, en la primera cláusula, la variable se vuelve a tipificar de a justo en el lado derecho del operador de implicación (es decir, ).ensuresindexisensuresindexint|nullint==>
El ejemplo anterior también ilustra el uso de un invariante de bucle inductivo . Se debe demostrar que el invariante de bucle se mantiene al ingresar al bucle, para cualquier iteración dada del bucle y cuando el bucle sale. En este caso, el invariante de bucle establece lo que se sabe sobre los elementos del itemsexaminado hasta el momento, es decir, que ninguno de ellos coincide con el item. El invariante de bucle no afecta el significado del programa y, en cierto sentido, podría considerarse innecesario. Sin embargo, el invariante de bucle es necesario para ayudar al verificador automático que se usa en el compilador Whiley a demostrar que esta función cumple con su especificación.
El ejemplo anterior también define el tipo natcon un invariante de tipo apropiado . Este tipo se utiliza para declarar una variable ie indicar que nunca puede contener un valor negativo. En este caso, la declaración evita la necesidad de un invariante de bucle adicional de la forma where i >= 0que de otro modo sería necesario.
Whiley comenzó en 2009 con el primer lanzamiento público, v0.2.27seguido en junio de 2010 y v0.3.0en septiembre de ese año. El lenguaje ha evolucionado lentamente con numerosos cambios sintácticos realizados hasta la fecha. Las versiones anteriores admitían tipos de datos y v0.3.33de primera clase , pero estos se eliminaron a favor de la representación de cadenas como matrices restringidas. Del mismo modo, las versiones anteriores a admitían conjuntos de primera clase (por ejemplo, ), diccionarios (por ejemplo, ) y listas redimensionables , pero estos se eliminaron a favor de matrices simples (por ejemplo, ). Quizás lo más controvertido fue la eliminación del tipo de datos en la versión . Muchos de estos cambios fueron motivados por el deseo de simplificar el lenguaje y hacer que el desarrollo del compilador fuera más manejable.stringcharint[]v0.3.35{int}{int=>bool}[int]int[]realv0.3.38
Otro hito importante en la evolución de Whiley llegó en la versión v0.3.40con la inclusión de tiempos de vida de referencia, desarrollada por Sebastian Schweizer como parte de su tesis de maestría en la Universidad de Kaiserslautern .