Whiley (lenguaje de programación)

Whiley es un lenguaje compilado multiparadigma de propósito general desarrollado por David Pearce.​ El lenguaje combina características de los paradigmas Funcionales e Imperativos, maneja tipos estáticos y soporta el uso de especificaciones formales a través de precondiciones y postcondiciones de funciones e invariantes de lazos. El lenguajes es también notable por el uso de tipado sensitivo al flujo.

El proyecto Whiley empezó en 2009 en respuesta al "Gran reto del compilador verificante" lanzado por Tony Hoare en 2003.​ La primera versión pública de Whiley estuvo disponible en junio de 2010.​

Whiley es principalmente desarrollado por David Pearce, pero es un proyecto de software libre que ha atraído contribuciones de una pequeña comunidad. Este lenguaje ha sido utilizado en proyectos académicos y también en la enseñanza universitaria.​ El proyecto fue financiado entre 2012 y 2014 por el Fondo Marsen de la Real Sociedad de Nueva Zelanda.​

El compilador de Whiley actualmente genera código para la Máquina Virtual de Java por lo que puede interoperar con Java y otros lenguajes basados en esa arquitectura.

Ejemplo

El ejemplo siguiente ilustra muchas de las características interesantes en Whiley, incluyendo el uso de postcondiciones, invariantes de bucle, invariantes de tipo, tipos unión y el tipado sensitivo al flujo. Se pretende que la función retorne el primer índice de un item entero en un arreglo de elementos enteros. Si no existe tal índice, entonces retorna null.

// Definición del tipo de los naturales
type nat is (int x) where x >= 0

public function indexOf(int[] items, int item) -> (int|null index)
// Cuando el resultado es int, el elemento en la posición index es igual a item
ensures index is int ==> items[index] == item
// Cuando el resultado es int, el element en la posición index es el primero igual a tiem
ensures index is int ==> no { i in 0 .. index | items[i] == item }
// Cuando el resultado es null, no hay elementos en items iguales a item
ensures index is null ==> no { i in 0 .. |items| | items[i] == item }:
    // La variable i no puede ser negativa
    nat i = 0
    
    while i < |items|
    // Ningún elemento anterior es igual a item
    where no { j in 0 .. i | items[j] == item }:
        
        if items[i] == item:
            return i
        i = i + 1
    
    return null

La función anterior se declara que el tipo de retorno la unión int|null lo cual indica que el valor resultante es un entero o un valor nulo. La postcondición de la función tiene tres cláusulas ensure, cada cual de las cuales describe propiedades diferentes que deben cumplirse en el valor de retorno. Se emplea tipado sensitivo al flujo en estas cláusulas a través del operador de verificación de tipos dinámico es. Por ejemplo, en la primera cláusula ensure el tipo de la variable index se afina de int|null a solamente int en el lado derecho del operador de implicación ( ==>).

El ejemplo anterior ilustra también el uso de un invariante de lazo inductivo. Debe verificarse que el invariante se cumple al principio del lazo, en cada iteración y al final del lazo. En este caso, el invariante de lazo establece los que se sabe sobre los elementos del arreglo que ya han sido examinados — concretamente, que ninguno de ellos es igual al elemento buscado. El invariante de lazo no afecta el significado del programa y, en algún sentido, podría ser considerado como innecesario. Aun así, el invariante de lazo es requerido para ayudar la verificación automatizada utilizada en el compilador de Whiley para probar que esta función cumple con su especificación.

El ejemplo anterior define también el tipo nat con un invariante de tipo apropiado. Este tipo se utiliza para declarar la variable i e indica que esta no puede contener valores negativos. En este caso, la declaración evita la necesidad de un invariante de lazo adicional de la forma where i >= 0 que de otra forma sería necesario.

Influencias

Whiley es pionero en el uso de tipado sensitivo al flujo, un concepto que más tarde fue acogido por otros lenguajes de programación como Ceylon, TypeScript y Facebook Flow.

Referencias

• Datos: Q23653623