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 escritura sensible al flujo, también conocida como "escritura de flujo".
Paradigma | Imperativo , funcional |
---|---|
Diseñada por | David J. Pearce |
Apareció por primera vez | Junio de 2010 |
Lanzamiento estable | 0.5.0 / 7 de junio de 2020 |
Disciplina de mecanografía | Fuerte , seguro , estructural , sensible al flujo |
Licencia | BSD |
Sitio web | whiley |
Influenciado por | |
Java , C , Python , Rust |
El proyecto Whiley comenzó en 2009 en respuesta al "Gran desafío de verificación del compilador" presentado por Tony Hoare en 2003. [2] El primer lanzamiento público de Whiley fue en junio de 2010. [3]
Desarrollado principalmente por David Pearce, Whiley es un proyecto de código abierto con contribuciones de una pequeña comunidad. El sistema se ha utilizado para proyectos de investigación de estudiantes y en la enseñanza de clases de pregrado. [4] Fue financiado entre 2012 y 2014 por el Fondo Marsden de la Real Sociedad de Nueva Zelanda. [5]
El compilador Whiley genera código para la máquina virtual Java y puede interactuar con Java y otros lenguajes basados en JVM.
Descripción general
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 fue fuertemente promovida a principios de la década de 2000 a través del Gran desafío de verificación del compilador de Hoare . El propósito de este desafío era impulsar nuevos esfuerzos para desarrollar un compilador de verificación , que se describe a grandes rasgos a continuación: [6]
Un compilador de verificación utiliza razonamiento matemático y lógico para verificar la exactitud de los programas que compila.
- Tony Hoare
El propósito 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 para desarrollar tales 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 Java Modeling Language agregan anotaciones para especificar condiciones previas y posteriores a Java . Asimismo, Spec # y Frama-C agregan 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 contraste, el lenguaje Whiley fue diseñado desde cero en un esfuerzo por evitar errores comunes y hacer que la verificación sea más manejable. [9]
Características
La sintaxis de Whiley sigue la apariencia general de los lenguajes imperativos u orientados a objetos. La sintaxis de sangría se elige sobre el uso de llaves para delinear bloques de instrucciones, dado un gran parecido con Python . Sin embargo, el aspecto imperativo de Whiley es algo engañoso ya que el núcleo del lenguaje es funcional y puro .
Mientras que distingue a function
(que es puro ) de a method
(que puede tener efectos secundarios ). Esta distinción es necesaria ya que permite utilizar funciones en especificaciones. Un conjunto familiar de tipos de datos primitivos está disponible, incluyendo bool
, int
, las matrices (por ejemplo int[]
) y los registros (por ejemplo {int x, int y}
). Sin embargo, a diferencia de la mayoría de los lenguajes de programación, el tipo de datos entero int
,, es ilimitado 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 módulo aritmético 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 lo son en lenguajes como Java o C # , sino que son valores inmutables .
Whiley adopta un enfoque inusual para la verificación de tipos que se conoce como "Escritura de flujo". Las variables pueden tener diferentes tipos estáticos en diferentes puntos de una función o método. La tipificación de flujo es similar a la tipificación de ocurrencias que se encuentra en Racket . [10] Para facilitar la tipificación 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 de la tipificación 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, suponga una variable x
de tipo T
y una prueba de tipo en tiempo de ejecución x is S
. En la rama verdadera, el tipo de se x
convierte T & S
en, mientras que en la rama falsa, se convierte en T & !S
.
Whiley utiliza un sistema de tipo estructural en lugar de nominal . Modula-3 , Go y Ceylon son ejemplos de otros lenguajes que admiten la escritura estructural de alguna forma.
Whiley admite vidas de referencia similares a las que se encuentran en Rust . Se pueden dar tiempos de vida al asignar nuevos objetos para indicar cuándo se pueden desasignar de forma segura. Las referencias a tales objetos deben incluir un identificador de por vida para evitar referencias colgantes . Cada método tiene una vida útil implícita a la que se hace referencia this
. Una variable de tipo &this:T
representa una referencia a un objeto de tipo T
que está desasignado con el método adjunto. La subtipificación entre vidas está determinada por la relación de vidas supervivientes . Por lo tanto, &l1:T
es un subtipo de &l2:T
si la vida l1
sobrevive estáticamente a la vida l2
. Se dice que una vida cuyo alcance encierra a otra la sobrevive. Los tiempos de vida en Whiley difieren de Rust en que actualmente no incluyen un concepto de propiedad .
Mientras que no tiene soporte incorporado para la concurrencia ni un modelo de memoria formal para determinar cómo se debe interpretar la lectura / escritura en el estado mutable compartido.
Ejemplo
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 tipificación de flujo. La función está destinada a devolver el primer índice de un entero item
en una matriz de enteros items
. Si no existe tal índice, null
se devuelve.
// Definir el tipo de números naturales type nat is ( int x ) donde x > = 0 función pública indexOf ( int [] elementos , int elemento ) -> ( int | índice nulo ) // Si se devuelve int, el elemento en esta posición coincide con el elemento asegura que el índice sea int ==> elementos [ índice ] == elemento // Si int devuelto, el elemento en esta posición es la primera coincidencia asegura que el índice sea int ==> no { i in 0 .. index | items [ i ] == item } // Si se devuelve nulo, ningún elemento en los elementos coincide con el elemento asegura que el índice sea nulo ==> no { i en 0 .. | artículos | | items [ i ] == item } : // nat i = 0 // while i < | artículos | // Ningún elemento visto hasta ahora coincide con el elemento donde no hay { j en 0 .. i | items [ j ] == item } : // si items [ i ] == item : return i i = i + 1 // devuelve nulo
En lo anterior, el tipo de retorno declarado de la función se le da el tipo de unión int|null
que indica que ya sea un int
valor se devuelve o null
se devuelve. La poscondición de la función se compone de tres ensures
cláusulas, cada una de las cuales describe diferentes propiedades que deben contener lo devuelto index
. Tipificación de flujo se emplea en estas cláusulas a través del operador de la prueba de tipo de tiempo de ejecución, is
. Por ejemplo, en la primera ensures
cláusula, la variable index
se vuelve a escribir de int|null
a justo int
en el lado derecho del operador de implicación (es decir ==>
).
El ejemplo anterior también ilustra el uso de un invariante de bucle inductivo . Se debe mostrar que el invariante de bucle se mantiene en la entrada al bucle, para cualquier iteración dada del bucle y cuando el bucle sale. En este caso, el ciclo invariante establece lo que se sabe sobre los elementos del items
examinado hasta ahora, es decir, que ninguno de ellos coincide con el dado item
. El invariante de bucle no afecta el significado del programa y, en cierto sentido, podría considerarse innecesario. Sin embargo, se requiere el invariante de bucle para ayudar al verificador automatizado que usa el compilador Whiley a probar que esta función cumple con su especificación.
El ejemplo anterior también define el tipo nat
con un invariante de tipo apropiado . Este tipo se utiliza para declarar variable i
e indicar que nunca puede tener un valor negativo. En este caso, la declaración evita la necesidad de un ciclo adicional invariante de la forma where i >= 0
que de otro modo sería necesario.
Historia
Whiley comenzó en 2009 con el primer lanzamiento público, v0.2.27
siguiendo en junio de 2010 y v0.3.0
en 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 de v0.3.33
primera clase , pero se eliminaron a favor de representar cadenas como matrices restringidas . Del mismo modo, versiones anteriores al conjunto de primera clase admitido (p . Ej. ), Diccionario (p . Ej. ) Y lista redimensionable ), pero se descartaron en favor de matrices simples (p . Ej .). 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 más manejable el desarrollo del compilador.string
char
int[]
v0.3.35
{int}
{int=>bool}
[int]
int[]
real
v0.3.38
Otro hito importante en la evolución de Whiley se produjo en la versión v0.3.40
con la inclusión de vidas de referencia, desarrolladas por Sebastian Schweizer como parte de su tesis de maestría en la Universidad de Kaiserslautern .
Referencias
- ^ "Página de inicio de Whiley" .
- ^ Hoare, Tony (2003). "El compilador de verificación: un gran desafío para la investigación informática". Revista de la ACM . 50 : 63–69. doi : 10.1145 / 602382.602403 . S2CID 441648 .
- ^ "¡Se lanzó Whiley v0.2.27!" .
- ^ "whiley.org/people" .
- ^ "Fondo Marsden" .
- ^ Hoare, Tony (2003). "El compilador de verificación: un gran desafío para la investigación informática". Revista de la ACM . 50 : 63–69. doi : 10.1145 / 602382.602403 . S2CID 441648 .
- ^ "Why3 --- Donde los programas se encuentran con los probadores" .
- ^ Barnett, Mike; Fähndrich, Manuel; Leino, K. Rustan M .; Müller, Peter; Schulte, Wolfram; Venter, Herman (2011). "Especificación y verificación: la experiencia de Spec #". Comunicaciones de la ACM . 54 (6): 81. doi : 10.1145 / 1953122.1953145 . S2CID 29809 .
- ^ Pearce, David J .; Groves, Lindsay (2015). "Diseño de un compilador de verificación: lecciones aprendidas del desarrollo de Whiley" . Ciencia de la Programación de Computadores . 113 : 191–220. doi : 10.1016 / j.scico.2015.09.006 .
- ^ "Escritura de ocurrencia" .
- ^ Pearce, David (2013). "Mecanografía de flujo completo y sonoro con uniones, intersecciones y negaciones" (PDF) .