Whiley (lenguaje de programación)

Whiley es un lenguaje de programación experimental que combina características de los paradigmas de programación funcional e imperativa , y admite la especificación formal a través de precondiciones de función , postcondiciones e invariantes de bucle . ^{[ 1 ]} El lenguaje utiliza tipado sensible al flujo, también denominado tipado de flujo .

El proyecto Whiley comenzó en 2009 en respuesta al "Gran Desafío de Verificación de Compiladores" propuesto por Tony Hoare en 2003. ^{[ 2 ]} La primera versión pública de Whiley fue en junio de 2010. ^{[ 3 ]}

Whiley, desarrollado principalmente por David Pearce, es un proyecto de código abierto con contribuciones de una pequeña comunidad. El sistema se ha utilizado para proyectos de investigación estudiantiles y en la enseñanza de clases de pregrado. ^{[ 4 ]} Fue financiado entre 2012 y 2014 por el Fondo Marsden de la Royal Society of New Zealand. ^{[ 5 ]}

El compilador Whiley genera código para la máquina virtual de Java (JVM) y puede interoperar con Java y otros lenguajes basados ​​en la JVM.

El objetivo de Whiley es proporcionar un lenguaje de programación realista donde la verificación se utilice de forma rutinaria y sin esfuerzo. La idea de una herramienta de este tipo tiene una larga historia, pero se impulsó 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 , descrito aproximadamente 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.

El propósito principal de dicha herramienta es mejorar la calidad del software asegurando que un programa cumpla con una especificación formal . Whiley sigue muchos intentos de desarrollar tales herramientas, incluyendo esfuerzos notables como SPARK/Ada , ESC/Java , Spec#, Dafny , Why3, ^{[ 7 ]} y Frama-C .

La mayoría de los intentos previos de desarrollar un compilador de verificación se centraron en extender los lenguajes de programación existentes con construcciones para escribir especificaciones. Por ejemplo, ESC/Java y el Java Modeling Language añaden anotaciones para especificar precondiciones y postcondiciones a Java . Del mismo modo, Spec# y Frama-C añaden construcciones similares a los lenguajes C# y C. Sin embargo, estos lenguajes contienen muchas características que plantean problemas difíciles o insuperables para la verificación. ^{[ 8 ]} En contraste, el lenguaje Whiley se diseñó desde cero con el fin de evitar errores comunes y hacer que la verificación sea más manejable. ^{[ 9 ]}

La sintaxis de Whiley sigue la apariencia general de los lenguajes de programación imperativos u orientados a objetos . Se utiliza la sintaxis de indentación (la regla de sangría ) en lugar de llaves para delimitar los bloques de instrucciones , lo que le confiere un gran parecido a Python . Sin embargo, la apariencia imperativa de Whiley puede resultar algo engañosa, ya que el núcleo del lenguaje es funcional y puro .

Whiley distingue un function(que es puro ) de un method(que puede tener efectos secundarios ). Esta distinción es necesaria ya que permite usar funciones en las especificaciones. Se dispone de un conjunto familiar de tipos de datos primitivos, incluidos bool, int, matrices (por ejemplo, int[]) y registros (por ejemplo, {int x, int y}). Sin embargo, a diferencia de la mayoría de los lenguajes de programación, el tipo de dato entero, int, no está acotado 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 razonar sobre aritmética modular es un problema conocido y difícil. Los objetos compuestos (por ejemplo, matrices o registros) no son referencias a valores en el montón como en lenguajes como Java o C# , sino que son valores inmutables .

Whiley adopta un enfoque inusual para la verificación de tipos denominado tipado de flujo . Las variables pueden tener diferentes tipos estáticos en diferentes puntos de una función o método. El tipado de flujo es similar al tipado de ocurrencia que se encuentra en Typed Racket . ^{[ 10 ]} Para facilitar el tipado 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 tipado 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 una prueba de tipo en tiempo de ejecución x is S. En la rama verdadera, el tipo de xse convierte en T & Smientras que, 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 tipado estructural de alguna forma.

Whiley admite tiempos de vida de referencia similares a los que se encuentran en Rust . Los tiempos de vida se pueden especificar al asignar nuevos objetos para indicar cuándo se pueden liberar 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 libera con el método que la contiene. El subtipo entre tiempos de vida se determina mediante la relación outlives&l1:T . Por lo tanto, es un subtipo de &l2:Tsi el tiempo de vida l1supera estáticamente al tiempo de vida l2. Se dice que un tiempo de vida cuyo ámbito contiene a otro lo supera. Los tiempos de vida en Whiley difieren de Rust en que actualmente no incluyen un concepto de propiedad .

Whiley no tiene soporte integrado para la concurrencia ni un modelo de memoria formal para determinar cómo se debe interpretar la lectura/escritura en un estado mutable compartido.

El siguiente ejemplo ilustra muchas de las características interesantes de Whiley, incluyendo el uso de postcondiciones, invariantes de bucle, invariantes de tipo, tipos de unión y tipado de flujo. La función está diseñada para devolver el primer índice de un entero itemen un array de enteros items. Si no existe tal índice, nullse devuelve.

// Define el tipo de números naturales type nat is ( int x ) where x >= 0public function indexOf ( int [] items , int item ) -> ( int | null index ) // Si se devuelve int, el elemento en esta posición coincide con item. Se asegura de que index sea int ==> items [ index ] == item // Si se devuelve int, el elemento en esta posición es la primera coincidencia. Se asegura de que index sea int ==> no { i in 0 .. index | items [ i ] == item } // Si se devuelve null, ningún elemento en items coincide con item. Se asegura de que index sea null ==> no { i in 0 .. | items | | items [ i ] == item } : // nat i = 0 // while i < | items | // No se ha visto ningún elemento hasta ahora que coincida con item donde no { j in 0 .. i | items [ j ] == item } : // if items [ i ] == item : return i i = i + 1 // return null

En lo anterior, el tipo de retorno declarado de la función recibe el tipo de unión int|nullque indica que seint devuelve un valor o se devuelve. La postcondiciónnull de la función consta de tres cláusulas, cada una de las cuales describe diferentes propiedades que debe tener el valor devuelto . En estas cláusulas se emplea la tipificación de flujo 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 . Debe demostrarse que el invariante de bucle se cumple al entrar en el bucle, para cualquier iteración dada del bucle y cuando el bucle sale. En este caso, el invariante de bucle indica lo que se sabe sobre los elementos itemsexaminados hasta el momento, a saber, que ninguno de ellos coincide con el valor dado item. El invariante de bucle no afecta el significado del programa y, en cierto sentido, puede considerarse innecesario. Sin embargo, el invariante de bucle es necesario para ayudar al verificador automático que utiliza 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 usa 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 muchos cambios de sintaxis realizados hasta la fecha. Las versiones anteriores v0.3.33admitían tipos de datos de primera clase stringy char, pero estos se eliminaron en favor de representar cadenas como int[]matrices restringidas. Del mismo modo, las versiones anteriores v0.3.35admitían conjuntos de primera clase (por ejemplo, {int}), diccionarios (por ejemplo, {int=>bool}) y listas redimensionables [int]), pero estos se eliminaron en favor de matrices simples (por ejemplo, int[]). Quizás lo más controvertido fue la eliminación del realtipo de datos en la versión v0.3.38. Muchos de estos cambios fueron motivados por el deseo de simplificar el lenguaje y hacer que el desarrollo del compilador fuera más manejable.

Otro hito importante en la evolución de Whiley llegó con la versión v0.3.40que incluía 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 .

• Sitio web oficial
• Mientras tanto en GitHub