El atractivo del lenguaje Ada ── Cuando los tipos expresan el diseño, el lenguaje que sostiene software que funciona durante décadas
· Actualizado el: · Go Komura · Ada, ProgrammingLanguage, StrongTyping, SPARK, GNAT, Alire, HighIntegrity, Embedded, AltaFiabilidad
1. Lo primero que hay que entender
¿Ha oído hablar alguna vez del lenguaje llamado Ada?
Es posible que muchas personas lo asocien con ideas como «un lenguaje antiguo», «un lenguaje militar» o «algo que solo se mencionó de pasada en clase».
Sin embargo, Ada sigue siendo un lenguaje vigente hoy en día.
En el mundo del software cuya interrupción pone en riesgo vidas humanas —control de vuelo de aeronaves, sistemas de señalización ferroviaria, cohetes, control del tráfico aéreo, satélites artificiales, equipos médicos—, Ada lleva décadas utilizándose sin interrupción.
A la hora de entender Ada, conviene tener presente lo siguiente.
Ada es un lenguaje que dedica todo su esfuerzo a "eliminar los errores antes de ejecutar el programa"
Los tipos no son simples contenedores de datos, sino herramientas para expresar la intención del diseño
La separación entre especificación e implementación, los contratos y la concurrencia están integrados en el lenguaje
No se convirtió en un lenguaje popular, pero su filosofía de diseño ha pasado a los lenguajes modernos
En este artículo repasamos el atractivo de Ada: su historia, su sintaxis, el tipado fuerte, las restricciones de rango, los paquetes, el diseño por contrato, las tareas, SPARK, el entorno de desarrollo y también sus puntos débiles.
El objetivo es que quienes habitualmente programan en C#, C++ o Java se lleven la sensación de «expresar el diseño mediante tipos».
Como el artículo es largo, con 21 capítulos en total, primero dejamos un mapa de orientación.
Estructura de este artículo:
Cap. 1-3 Qué es Ada, su historia y dónde se utiliza
Cap. 4-5 Primer paso (Hello, World) y una sintaxis que prioriza la legibilidad
Cap. 6-11 Sistema de tipos: tipado fuerte, restricciones de rango, arreglos, paquetes, registros, genéricos
Cap. 12-13 Manejo de excepciones y diseño por contrato (Pre/Post)
Cap. 14-15 Concurrencia: tareas y objetos protegidos
Cap. 16-17 Verificación formal con SPARK e interoperabilidad con C/C++
Cap. 18 Entorno de desarrollo (GNAT y Alire)
Cap. 19-21 Puntos débiles y precauciones, el valor desde la óptica del software de larga vida, resumen
Está escrito de forma que tenga sentido leerlo también por partes: quien quiera ponerlo en marcha cuanto antes puede ir directo a los capítulos 4 y 18, y quien solo quiera captar la filosofía de diseño, a los capítulos 1, 6, 7 y 13.
Además, los fragmentos de código que aparecen en este artículo están publicados en GitHub como una colección de referencia, organizada por archivos según el capítulo.
ada-language-appeal - komurasoft-blog-samples (GitHub)
2. Qué es Ada ── el origen de su nombre y su historia
Ada es un lenguaje de programación de propósito general que nació a finales de la década de 1970 por iniciativa del Departamento de Defensa de Estados Unidos (DoD).
En aquella época, el Departamento de Defensa se enfrentaba al problema de que cada proyecto usaba un lenguaje distinto, lo que disparaba el coste de mantenimiento del software.
Por ello, se organizó un concurso internacional de diseño para seleccionar un lenguaje estándar que también pudiera usarse en sistemas embebidos y de tiempo real.
La propuesta elegida fue la del equipo liderado por Jean Ichbiah.
El nombre del lenguaje, Ada, proviene de Ada Lovelace (Augusta Ada King, condesa de Lovelace), considerada la primera programadora de la historia.
A grandes rasgos, la historia de Ada puede resumirse así.
1980 se establece la primera especificación como MIL-STD-1815
1983 Ada 83 (estándar ANSI)
1987 se convierte en estándar ISO
1995 Ada 95 (introducción de la orientación a objetos y los objetos protegidos)
2005 Ada 2005 (interfaces y ampliación de la biblioteca de contenedores)
2012 Ada 2012 (el diseño por contrato se incorpora como característica del lenguaje)
2022 Ada 2022 (el estándar más reciente)
Ada 95 es uno de los primeros lenguajes orientados a objetos en obtener estandarización ISO.
Y en Ada 2012, el diseño por contrato (Design by Contract) —precondiciones, poscondiciones e invariantes de tipo— se incorporó a la especificación del lenguaje.
Ada no es «un lenguaje antiguo», sino un lenguaje que se ha seguido revisando durante más de 40 años.
3. Dónde se utiliza Ada
Los ámbitos representativos donde Ada se sigue utilizando son los sistemas que exigen alta integridad (High Integrity).
Control de vuelo y aviónica de aeronaves comerciales
Sistemas de control del tráfico aéreo
Sistemas de señalización y seguridad ferroviaria
Cohetes y satélites artificiales
Sistemas de defensa
Equipos médicos
Algunos sistemas troncales financieros e industriales
Estos ámbitos comparten una serie de características.
Un error se traduce directamente en pérdida de vidas humanas o en pérdidas económicas enormes
La certificación y las auditorías exigen "evidencia de corrección"
Una vez desplegado, el sistema sigue usándose durante décadas
El coste de corregirlo más adelante es extremadamente alto
Es un mundo donde no vale la idea de «ya lo arreglaremos después de publicarlo».
El diseño del lenguaje Ada existe precisamente para responder a esta exigencia.
Todo el lenguaje está atravesado por una misma filosofía: eliminar en tiempo de compilación los errores detectables en tiempo de compilación, mediante comprobaciones en tiempo de ejecución los que solo pueden detectarse en tiempo de ejecución y, yendo más allá, mediante demostración matemática los que se pueden demostrar.
Esta filosofía merece la pena estudiarla incluso para quienes desarrollan aplicaciones empresariales web o de escritorio.
4. Primero, Hello, World
Veamos código en Ada.
with Ada.Text_IO;
procedure Hello is
begin
Ada.Text_IO.Put_Line ("Hello, Ada!");
end Hello;
Este código se puede guardar y ejecutar de inmediato. El compilador representativo de Ada es GNAT (el compilador de Ada gratuito incluido en GCC; las opciones de compilación de los ejemplos de código de este artículo también corresponden a GNAT), y compilarlo y ejecutarlo se resume en dos líneas.
gnatmake hello.adb -> genera el ejecutable hello (hello.exe en Windows)
./hello -> Hello, Ada!
La convención es que el nombre de archivo sea «el nombre de la unidad en minúsculas + .adb» (para procedure Hello, sería hello.adb). En el capítulo 18 se explica cómo obtener GNAT y un procedimiento aún más cómodo mediante el gestor de paquetes Alire. Si prefiere montar primero el entorno y ponerse a trabajar, puede saltar directamente al capítulo 18.
Lo primero que probablemente llame la atención es lo siguiente.
with importa unidades de biblioteca
El cuerpo del programa es un procedimiento (procedure)
begin / end delimita un bloque
Después de end se repite el nombre
Las sentencias terminan en punto y coma
Repetir el nombre al final, como en end Hello;, es un rasgo característico de Ada.
Aunque los bloques se aniden en profundidad, se ve de un vistazo a qué corresponde cada end.
Además, el compilador comprueba la correspondencia de nombres, por lo que cerrar mal un bloque produce un error de compilación.
Puede parecer un detalle menor, pero refleja bien la filosofía de Ada: «el lenguaje respalda los puntos donde las personas suelen leer mal».
5. Una sintaxis centrada en la legibilidad
La sintaxis de Ada está diseñada priorizando la legibilidad por encima de la facilidad de escritura.
Parte de la premisa de que el software se lee muchísimas más veces de las que se escribe.
Por ejemplo, los bucles y las condicionales se escriben así.
for I in 1 .. 5 loop
Ada.Text_IO.Put_Line (Integer'Image (I * I));
end loop;
if Temperature > 80.0 then
Start_Cooling;
elsif Temperature < 20.0 then
Start_Heating;
else
Keep_Current_State;
end if;
La sentencia case tiene un rasgo característico de Ada.
case Today is
when Mon .. Fri =>
Put_Line ("Weekday");
when Sat | Sun =>
Put_Line ("Weekend");
end case;
Los puntos clave son los siguientes.
case produce un error de compilación si no cubre todos los valores posibles
No existe el fall-through implícito propio de los lenguajes de la familia C
Las condiciones pueden agruparse con rangos (Mon .. Fri) o listas de opciones (Sat | Sun)
Al añadir un valor a un tipo enumerado, cualquier sentencia case que no lo cubra pasa a producir un error de compilación.
Una vez que se experimenta que «el compilador enumera todos los puntos afectados por un cambio de especificación», resulta difícil prescindir de ello.
Además, los argumentos admiten asociación por nombre.
Draw_Rectangle (Left => 10, Top => 20, Width => 100, Height => 50);
Esto evita confundir el orden de los argumentos y hace que el propio código de la llamada actúe como documentación.
La asignación se escribe := y la comparación =, de modo que la confusión típica de if (a = b) en los lenguajes de la familia C no puede darse a nivel sintáctico.
6. Tipado fuerte ── convertir la confusión de unidades en un error de compilación
El mayor atractivo de Ada es su tipado fuerte.
La expresión «tipado fuerte» se usa en muchos lenguajes, pero en Ada tiene un nivel de profundidad adicional.
En Ada, dos tipos declarados con nombres distintos son tipos diferentes aunque su estructura sea idéntica.
type Meters is new Float;
type Seconds is new Float;
Distance : Meters := 100.0;
Time : Seconds := 9.58;
Ambos son, en el fondo, números en coma flotante, pero no se pueden mezclar.
Distance := Time; -- error de compilación
Distance := Distance + Time; -- error de compilación
Solo cuando la conversión es intencionada se escribe de forma explícita.
Speed : constant Float := Float (Distance) / Float (Time);
¿Por qué llegar a este nivel de rigor?
No son pocos los accidentes reales de software cuya causa fue una «confusión de unidades».
Un ejemplo célebre es la pérdida en 1999 de la sonda marciana Mars Climate Orbiter, causada por la mezcla del sistema imperial y el sistema métrico.
La respuesta de Ada es sencilla.
Hacer que metros y pies sean tipos distintos
Que mezclarlos produzca un error de compilación
Obligar a escribir la conversión de forma explícita
En lugar de «tener cuidado», «detectarlo en la revisión» o «atraparlo con pruebas», hacer directamente que la compilación no pase.
Esta es la postura básica de Ada.
7. Restricciones de rango ── impedir valores inválidos a nivel del tipo de datos
En Ada, un tipo puede tener asociado un rango de valores.
subtype Percentage is Integer range 0 .. 100;
Progress : Percentage := 50;
Si se intenta asignar a una variable de tipo Percentage un valor fuera de rango, se produce en tiempo de ejecución la excepción Constraint_Error.
Progress := 120; -- Constraint_Error en tiempo de ejecución
Las violaciones que se pueden determinar en tiempo de compilación se detectan en tiempo de compilación.
Premisas implícitas como «este valor debería estar entre 0 y 100» o «este valor debería ser mayor o igual que 1» pueden expresarse mediante el tipo, en lugar de mediante comentarios.
De hecho, la biblioteca estándar de Ada ya define de antemano tipos con restricción de uso frecuente.
Natural = Integer range 0 .. Integer'Last
Positive = Integer range 1 .. Integer'Last
Además, desde Ada 2012 es posible adjuntar cualquier condición como predicado.
subtype Even is Integer
with Dynamic_Predicate => Even mod 2 = 0;
El lenguaje también incorpora tipos orientados al control de hardware, como los tipos de punto fijo.
type Temperature is delta 0.1 range -50.0 .. 150.0;
En muchos lenguajes, la comprobación de valores inválidos tiende a quedar así.
Validación mediante una sentencia if al principio de la función
Las comprobaciones olvidadas dependen de la revisión de código
No queda claro qué funciones reciben valores ya comprobados
En Ada se puede afirmar que «por el simple hecho de ser un valor de este tipo, el rango ya está garantizado».
Al trasladar la responsabilidad de la validación al tipo de dato, la lógica de la función puede concentrarse en su tarea propiamente dicha.
8. Arreglos e índices ── comprobación de límites e índices con tipos enumerados
En los arreglos de Ada se puede elegir libremente el tipo del índice.
type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
type Hours_Array is array (Day) of Natural;
Work_Hours : Hours_Array := (Mon .. Fri => 8, others => 0);
Es un arreglo indexado por el tipo enumerado Day.
Se puede acceder con Work_Hours (Wed), sin necesidad de recordar qué significa cada índice numérico.
Los bucles también pueden escribirse conforme al tipo del índice.
for D in Work_Hours'Range loop
Put_Line (Day'Image (D) & ":" & Natural'Image (Work_Hours (D)));
end loop;
Con atributos como 'Range, 'First, 'Last y 'Length se puede obtener en cualquier momento la información de los límites del arreglo.
Como los límites no se codifican de forma fija, un cambio en el tamaño del arreglo no repercute en el bucle.
Y lo importante es que el acceso al arreglo siempre se comprueba frente a sus límites.
Buffer : String (1 .. 10);
Index : Integer := 11;
Buffer (Index) := 'x'; -- Constraint_Error en tiempo de ejecución
El desbordamiento de búfer en C/C++ sigue siendo, desde hace años, una de las principales causas de vulnerabilidades de seguridad.
En Ada, un acceso fuera de rango no es un comportamiento indefinido, sino una excepción bien definida.
En lugar de corromper la memoria en silencio y provocar un fallo misterioso en otro lugar, el programa se detiene de inmediato, con estrépito, justo en el punto donde surge el problema.
Si se piensa en el coste de investigar fallos en sistemas de uso prolongado, esta diferencia es enorme.
9. Paquetes ── separación entre especificación e implementación
El mecanismo de modularización de Ada es el paquete.
Un paquete se divide en dos archivos: la especificación (spec) y el cuerpo (body).
counters.ads especificación: la interfaz que se expone al exterior
counters.adb cuerpo: los detalles de la implementación
La especificación se escribe así.
package Counters is
type Counter is private;
procedure Increment (C : in out Counter);
function Value (C : Counter) return Natural;
private
type Counter is record
Count : Natural := 0;
end record;
end Counters;
El cuerpo se escribe así.
package body Counters is
procedure Increment (C : in out Counter) is
begin
C.Count := C.Count + 1;
end Increment;
function Value (C : Counter) return Natural is
begin
return C.Count;
end Value;
end Counters;
Conviene fijarse en lo siguiente.
Al declarar el type como private, el código que lo usa no puede tocar su estructura interna
Leyendo solo la especificación (.ads) se entiende todo el modo de uso
Aunque se modifique el cuerpo (.adb), si la especificación no cambia, la recompilación del lado que lo usa es mínima
Se parece a los archivos de cabecera de C/C++, pero la coherencia se comprueba como parte de la especificación del lenguaje, no mediante una expansión textual como #include.
Cualquier discrepancia entre la especificación y el cuerpo es un error de compilación.
Además, en los parámetros siempre se especifica un modo: in, out o in out.
procedure Increment (C : in out Counter);
Con solo mirar la firma se sabe si «este parámetro se lee, se escribe o se lee y se escribe».
Es posible leer la dirección del flujo de datos sin necesidad de conocer punteros ni referencias.
10. Registros y discriminantes
El equivalente en Ada de las estructuras (struct) es el registro (record).
type Point is record
X : Float := 0.0;
Y : Float := 0.0;
end record;
P : Point := (X => 1.0, Y => 2.0);
Los campos pueden tener valores por defecto, y la inicialización mediante un agregado (aggregate) puede hacerse por nombre.
Una característica propia de Ada es el discriminante (discriminant).
type Buffer (Size : Positive) is record
Data : String (1 .. Size);
Length : Natural := 0;
end record;
Small : Buffer (Size => 16);
Large : Buffer (Size => 4096);
El discriminante es un parámetro que determina la «forma» del registro.
Buffer (16) y Buffer (4096) son del mismo tipo, pero el tamaño del arreglo interno queda fijado en la declaración y no cambia después.
Es como si el lenguaje gestionara de forma segura, mediante el propio tipo, lo que en C sería «una estructura con un miembro de longitud variable más un campo de tamaño».
Desde el principio no existe la puerta de entrada a un tipo de error habitual en C: la inconsistencia entre el tamaño declarado y el real.
11. Genéricos
Ada contaba con genéricos (generic) desde su primer estándar, en 1983.
Es mucho anterior a las plantillas de C++ (años noventa) o a los genéricos de Java (2004).
generic
type Element is private;
procedure Swap (Left, Right : in out Element);
procedure Swap (Left, Right : in out Element) is
Temp : constant Element := Left;
begin
Left := Right;
Right := Temp;
end Swap;
Quien lo usa lo instancia con un tipo concreto.
procedure Swap_Integers is new Swap (Element => Integer);
procedure Swap_Floats is new Swap (Element => Float);
Una característica de los genéricos de Ada es que exponen explícitamente las operaciones que requieren.
generic
type Element is private;
with function "<" (Left, Right : Element) return Boolean is <>;
function Max (Left, Right : Element) return Element;
En la especificación se declara que «esta función genérica requiere que el tipo Element tenga un operador de comparación».
El problema que las plantillas de C++ arrastraron durante años —que el error solo se descubre al instanciar— no se produce en Ada desde el principio.
Ada ya tenía respuesta, hace 40 años, al problema que los concepts de C++20 o los límites de traits de Rust intentaron resolver.
12. Manejo de excepciones
Ada dispone de manejo de excepciones.
with Ada.Text_IO;
with Ada.Exceptions;
procedure Read_Config is
begin
Load_File ("config.txt");
exception
when Ada.Text_IO.Name_Error =>
Ada.Text_IO.Put_Line ("No se encontró el archivo de configuración");
when E : others =>
Ada.Text_IO.Put_Line (Ada.Exceptions.Exception_Information (E));
raise;
end Read_Config;
Al final del bloque se escribe la parte exception, con un manejador para cada tipo de excepción.
Entre las excepciones definidas por el lenguaje, las más representativas son las siguientes.
Constraint_Error violación de restricción de rango, de los límites de un arreglo, división entre cero, etc.
Program_Error violación de una regla del lenguaje (por ejemplo, alcanzar un punto al que no se debería llegar)
Storage_Error falta de memoria
Tasking_Error fallo en la comunicación entre tareas
Lo destacable es que las violaciones de restricciones de rango y de comprobación de límites están todas integradas en este mismo mecanismo de excepciones.
Si se incumple «la restricción escrita en el tipo», el resultado es Constraint_Error.
Es decir, la restricción de rango vista en el capítulo 7 funciona como una aserción de tiempo de ejecución generada automáticamente.
No hace falta esparcir por el código comprobaciones manuales con sentencias if.
13. Diseño por contrato ── expresar precondiciones y poscondiciones como característica del lenguaje
El punto estrella de Ada 2012 es el soporte del lenguaje para el diseño por contrato (Design by Contract).
Se pueden escribir directamente en un subprograma una precondición (Pre) y una poscondición (Post).
package Stacks is
type Stack is private;
function Is_Full (S : Stack) return Boolean;
function Is_Empty (S : Stack) return Boolean;
function Count (S : Stack) return Natural;
procedure Push (S : in out Stack; Item : Integer)
with Pre => not Is_Full (S),
Post => Count (S) = Count (S)'Old + 1;
procedure Pop (S : in out Stack; Item : out Integer)
with Pre => not Is_Empty (S),
Post => Count (S) = Count (S)'Old - 1;
private
-- Detalles de la implementación
end Stacks;
Pre es «la promesa que debe cumplir quien llama», y Post es «la promesa que garantiza la implementación».
Con el atributo 'Old se puede referenciar el valor previo a la llamada.
Este contrato puede activarse como comprobación en tiempo de ejecución mediante una opción de compilación (en GNAT, -gnata).
Si se incumple el contrato, se produce la excepción Assertion_Error, y queda claro quién rompió la promesa.
Violación de Pre -> error del lado que llama
Violación de Post -> error del lado de la implementación
¿En qué se diferencia esto de escribir en un comentario de documentación «esta función no debe llamarse con una pila vacía»?
Un comentario puede desviarse de la implementación sin que nadie lo note
El compilador comprueba la sintaxis y los tipos del contrato
El contrato se puede verificar automáticamente en tiempo de ejecución
El contrato sirve de entrada para la demostración estática con SPARK (capítulo 16)
La especificación existe dentro del código de una forma verificable.
Este es el mundo de Ada a partir de 2012.
Con el invariante de tipo (Type_Invariant) también se puede expresar la restricción de que «los valores de este tipo siempre cumplen esta propiedad».
14. Tareas ── la concurrencia integrada en el lenguaje
Otro gran atractivo de Ada es que la concurrencia forma parte de la especificación del lenguaje.
Mientras que C/C++ dependen de las API del sistema operativo o de bibliotecas (pthread, std::thread) para los hilos, Ada ya tenía las tareas integradas en el lenguaje en 1983.
with Ada.Text_IO;
procedure Task_Demo is
task Worker;
task body Worker is
begin
for I in 1 .. 3 loop
Ada.Text_IO.Put_Line ("worker:" & Integer'Image (I));
delay 0.5;
end loop;
end Worker;
begin
for I in 1 .. 3 loop
Ada.Text_IO.Put_Line ("main :" & Integer'Image (I));
delay 0.5;
end loop;
end Task_Demo;
Al declarar una task, la ejecución concurrente comienza al mismo tiempo que el bloque que la contiene.
Y lo importante es que el bloque no termina hasta que todas las tareas internas han finalizado.
Estructuralmente no puede darse el tipo de error consistente en «olvidar el join de un hilo y que ocurra algo extraño al terminar el proceso».
Para la sincronización entre tareas existe una característica del lenguaje llamada rendezvous (cita).
task Logger is
entry Write (Message : String);
end Logger;
task body Logger is
begin
loop
select
accept Write (Message : String) do
Ada.Text_IO.Put_Line (Message);
end Write;
or
terminate;
end select;
end loop;
end Logger;
Quien lo usa puede escribirlo con la misma forma que una llamada a procedimiento: Logger.Write ("hello");.
Así se puede escribir comunicación entre tareas mediante paso de mensajes, sin necesidad de conocer los bloqueos.
Para los sistemas de tiempo real, incluso está estandarizado el perfil Ravenscar, que fija la política de planificación y el control de prioridades, y que además restringe las funciones de tareas para facilitar su verificación.
15. Objetos protegidos ── expresar la exclusión mutua como un tipo
Para el control de exclusión mutua sobre datos compartidos se utiliza el objeto protegido (protected object), introducido en Ada 95.
protected Shared_Counter is
procedure Increment;
function Value return Natural;
private
Count : Natural := 0;
end Shared_Counter;
protected body Shared_Counter is
procedure Increment is
begin
Count := Count + 1;
end Increment;
function Value return Natural is
begin
return Count;
end Value;
end Shared_Counter;
Los datos de un objeto protegido solo pueden accederse a través de las operaciones definidas.
Y la exclusión mutua queda garantizada por el propio lenguaje.
procedure permite lectura y escritura, se ejecuta de forma exclusiva
function solo lectura, permite la ejecución simultánea de varias tareas
entry puede hacer esperar a quien llama hasta que se cumpla una condición (barrera)
En muchos lenguajes, el control de exclusión mutua tiende a depender de la disciplina del programador, con reglas como las siguientes.
Al tocar este dato, hay que tomar este mutex
No olvidar liberar el bloqueo
Respetar el orden de los bloqueos
En los objetos protegidos de Ada, sencillamente no se puede escribir «código que olvide tomar el bloqueo».
Porque el dato y el control de exclusión que lo protege se declaran como un único tipo.
Usando la condición de barrera de entry, también se puede escribir sincronización condicional —como «esperar hasta que entren datos en la cola»— sin gestionar manualmente banderas o variables de condición.
16. SPARK ── el camino hacia la verificación formal
En el mundo de Ada existe un aliado poderoso llamado SPARK.
SPARK es un subconjunto (sublenguaje) de Ada, diseñado para poder demostrar matemáticamente las propiedades de un programa.
procedure Increment (X : in out Integer)
with SPARK_Mode,
Pre => X < Integer'Last,
Post => X = X'Old + 1;
La herramienta de SPARK (GNATprove) demuestra, sin ejecutar el código, cuestiones como las siguientes.
Que no se produce desbordamiento
Que no se viola ninguna restricción de rango
Que no ocurre una división entre cero
Que no se lee ninguna variable sin inicializar
La coherencia entre Pre y Post
La diferencia con las pruebas es determinante.
Prueba confirma que el programa funciona correctamente para las entradas elegidas
Demostración muestra que la propiedad se cumple para todas las entradas posibles
El contrato (Pre/Post) visto en el capítulo 13 se convierte, tal cual, en objeto de demostración en SPARK.
Un contrato escrito como comprobación en tiempo de ejecución puede elevarse después a la categoría de «demostrado».
SPARK ha acumulado un historial sólido en el mundo aeroespacial y de defensa, pero en los últimos años su uso se ha extendido también en la industria, con casos como el de NVIDIA, que lo ha adoptado para la seguridad de firmware.
El ecosistema de Ada/SPARK sigue desmintiendo, en silencio, el lugar común de que «los métodos formales son demasiado académicos para usarse en la práctica».
17. Interoperabilidad con C y C++
Ada no es un lenguaje aislado.
La interoperabilidad con C está estandarizada en el anexo B de la especificación del lenguaje (Annex B ── «Interface to Other Languages» del manual de referencia de Ada, el ARM, el anexo que define la interfaz con otros lenguajes como C o Fortran).
Por ejemplo, para llamar desde Ada a Sleep de la API de Windows, se escribe así.
with Interfaces.C;
procedure Sleep_Demo is
procedure Sleep (Milliseconds : Interfaces.C.unsigned)
with Import,
Convention => Stdcall,
External_Name => "Sleep";
begin
Sleep (1000);
end Sleep_Demo;
Los puntos clave son los siguientes.
Import importa una implementación externa
Convention especifica la convención de llamada (C, Stdcall, etc.)
External_Name especifica el nombre del símbolo en el enlazado
Interfaces.C proporciona tipos correspondientes a los tipos de C (int, unsigned, char*, etc.)
También es posible en sentido contrario.
Usando Export, un procedimiento escrito en Ada puede exponerse como una función llamable desde C.
Es decir, se pueden dar usos progresivos como los siguientes.
Utilizar desde Ada una biblioteca de C ya existente
Escribir en Ada/SPARK solo el núcleo del sistema y dejar el resto en C/C++
Convertir código Ada en una DLL y llamarlo desde otros lenguajes
No es un lenguaje que obligue a «reescribirlo todo o nada»: permite convivir con los activos existentes e ir elevando la fiabilidad empezando por las partes más importantes.
18. Entorno de desarrollo ── GNAT y Alire (también funciona en Windows)
Puede que piense que «para probar Ada hacen falta herramientas caras».
Hoy en día se puede montar un entorno de desarrollo serio y completamente gratuito.
GNAT el compilador de Ada incluido en GCC (gratuito)
Alire el gestor de paquetes y herramienta de compilación de Ada
GNAT Studio el IDE creado por AdaCore
VS Code con la extensión Ada Language Server se obtiene autocompletado y salto a la definición
En particular, la aparición de Alire (cuyo comando es alr) ha hecho que iniciarse en Ada sea muchísimo más sencillo.
Es una experiencia muy cercana a la de cargo en Rust.
alr init --bin hello_ada
cd hello_ada
alr build
alr run
Con alr init se crea el proyecto, con alr build se compila y con alr run se ejecuta.
Como Alire también descarga la cadena de herramientas (el propio GNAT), ni siquiera es necesario instalar el compilador manualmente.
Funciona tanto en Windows como en Linux o macOS.
Si desarrolla en Windows, el camino más corto es el siguiente.
1. Descargar el instalador para Windows desde el sitio oficial de Alire
2. Crear la plantilla con alr init --bin
3. Instalar en VS Code la extensión de Ada (creada por AdaCore)
4. Compilar y ejecutar con alr build
También se pueden añadir bibliotecas con alr with nombre_de_la_biblioteca.
Ha terminado la época en la que uno se rendía al intentar montar el entorno.
19. Puntos débiles y precauciones de Ada
Hasta aquí hemos presentado sus atractivos, pero Ada también tiene puntos débiles.
Los repasamos con honestidad.
Ecosistema reducido
Pocas opciones de frameworks web, GUI, SDK en la nube, etc.
El número de paquetes de Alire es órdenes de magnitud menor que en los lenguajes dominantes
Escasez de profesionales e información
La información en japonés es especialmente escasa
Adoptarlo en un equipo exige prever un coste de formación
La sintaxis puede resultar verbosa
La declaración de tipos y la separación entre especificación y cuerpo pesan en scripts pequeños
No es apto para el uso de "hacerlo funcionar de cualquier manera"
Mercado laboral limitado
Concentrado en sectores como la aeroespacial, la defensa o el ferrocarril
Además, la historia nos enseña que no se trata simplemente de que «usar Ada garantice la seguridad».
La explosión del primer vuelo del cohete Ariane 5 en 1996 tuvo como una de sus causas un software escrito en Ada.
Al reutilizar en el Ariane 5, cuyas características de vuelo eran distintas, un código escrito para el Ariane 4, un valor mayor de lo previsto provocó durante una conversión un Constraint_Error que no se gestionó adecuadamente, y el sistema se detuvo.
Los detalles concretos son estos. Dentro de la unidad de referencia inercial (SRI) había un proceso que convertía de número en coma flotante de 64 bits a entero con signo de 16 bits el valor BH (Horizontal Bias, un valor interno relacionado con la velocidad horizontal) calculado para la alineación previa al despegue. Como la trayectoria de vuelo del Ariane 5 genera una velocidad horizontal unas 5 veces mayor que la del Ariane 4, el valor de BH superó el rango representable en 16 bits y la conversión falló (en el informe de investigación se denomina «error de operando»; en términos de la comprobación de rango de Ada, se trata de una conversión fuera de rango). Y, además, esta conversión no estaba protegida. Como el ordenador del SRI tenía como objetivo una «carga máxima del 80 %», de las 7 variables con riesgo solo se protegieron 4, y en las 3 restantes se prescindió de la protección al considerar que «están físicamente limitadas o cuentan con margen suficiente». En el caso de BH, ese criterio dejó de ser válido en el Ariane 5.
Lo que muestra este accidente es lo siguiente.
La comprobación en tiempo de ejecución del lenguaje detectó el problema (no falló en silencio)
Sin embargo, no se verificó que las premisas de operación habían cambiado
El diseño posterior a la excepción (a prueba de fallos) era insuficiente
Ni el sistema de tipos ni los contratos sustituyen al proceso de revisar las premisas.
El lenguaje es una parte de la ingeniería de seguridad, no toda ella.
Creo que esta es la advertencia más honesta a la hora de aprender Ada.
20. El software de larga vida y Ada ── desde la óptica del mantenimiento
En este sitio tratamos con frecuencia el mantenimiento y la prolongación de la vida útil de activos existentes en Windows.
Desde esa perspectiva, Ada tiene otro atractivo distinto.
No es raro encontrar sistemas escritos en Ada que llevan funcionando durante décadas.
Y el propio diseño del lenguaje Ada da por supuesto el mantenimiento a largo plazo.
Separación entre especificación (.ads) e implementación (.adb)
-> quien dé mantenimiento dentro de 20 años puede entender la interfaz leyendo solo la especificación
Tipos fuertes y restricciones de rango
-> las premisas implícitas quedan en el código, sin depender de la tradición oral ni de los comentarios
Contrato (Pre/Post)
-> "la promesa de esta función" queda registrada de forma verificable
Comprobación de exhaustividad de case
-> el compilador enumera los puntos afectados por un cambio de especificación
Prioridad de la compatibilidad hacia atrás incluso en las revisiones del estándar
-> gran parte del código de Ada 83 sigue compilando en los compiladores actuales
Todo esto puede importarse tal cual como directrices de diseño también al hacer mantenimiento a largo plazo en C# o C++.
Definir tipos con significado propio (tipos que representan un ID, tipos con unidad) en lugar de int
Diseñar tipos que no permitan construir valores inválidos (validación en el constructor)
Separar de forma consciente la interfaz pública de la implementación
Expresar las precondiciones y poscondiciones mediante aserciones o pruebas
Escribir de forma exhaustiva los switch sobre tipos enumerados y tratar las advertencias como errores
Aunque no tenga ocasión de usar Ada en el trabajo, aprender su filosofía de diseño tiene un valor considerable.
Como material para aprender la sensación de «expresar el diseño mediante tipos», Ada sigue siendo de primera categoría.
21. Resumen
Hemos repasado el atractivo de Ada.
Recapitulemos los puntos clave.
Ada es un lenguaje vigente que se usa desde hace más de 40 años en sistemas de alta fiabilidad
Su nombre proviene de Ada Lovelace y su estándar más reciente es Ada 2022
Aunque la estructura sea la misma, tipos con nombres distintos son tipos distintos: confundir unidades es un error de compilación
Las restricciones de rango impiden valores inválidos a nivel del tipo
Los arreglos tienen comprobación de límites, por lo que el desbordamiento de búfer no es comportamiento indefinido
Los paquetes separan la especificación de la implementación, y el modo de los argumentos deja explícito el flujo de datos
Los genéricos declaran en la especificación las operaciones que requieren, por lo que los errores de uso son claros
El contrato (Pre/Post) de Ada 2012 permite dejar la especificación en el código de forma verificable
Las tareas y los objetos protegidos permiten escribir concurrencia de forma segura como característica del lenguaje
Con SPARK se puede elevar un contrato de comprobación en tiempo de ejecución a demostración matemática
Con GNAT y Alire se puede probar de inmediato y de forma gratuita, incluso en Windows
Sus puntos débiles son un ecosistema pequeño y la escasez de profesionales
Los mecanismos de seguridad del lenguaje no sustituyen al proceso de revisar las premisas
Ada, en el sentido de moda, es un lenguaje que no llegó a ser dominante.
Sin embargo, Ada ya contaba, desde hace décadas, con muchas de las características que los lenguajes modernos presentan como «novedades»: seguridad frente a null, comprobación de exhaustividad, contratos y un rigor cercano a la propiedad (ownership).
La esencia de Ada puede resumirse en una sola frase.
Los errores no son algo que se busca, sino algo que los tipos y los contratos hacen imposible de escribir.
Le invito a crear un proyecto con Alire un fin de semana y escribir un pequeño programa, dejándose regañar por el compilador.
Cuando se dé cuenta de que cada uno de esos errores de compilación es «un error atrapado antes de convertirse en un fallo en producción», el atractivo de Ada terminará de encajar.
Referencias
- Colección de referencia con los fragmentos de código de este artículo, organizados por capítulo - komurasoft-blog-samples (GitHub)
- Ada Programming Language - AdaCore
- Learn Ada - AdaCore (learn.adacore.com)
- Introduction to Ada - learn.adacore.com
- Ada Reference Manual (Ada 2022)
- Alire - Ada Library Repository
- GNAT User’s Guide - GCC
- SPARK - AdaCore
- Introduction to SPARK - learn.adacore.com
- Ada Conformity Assessment Authority
- Ariane 501 Inquiry Board Report (ESA)
Artículos relacionados
Artículos recientes con las mismas etiquetas para profundizar en temas cercanos.
Programación genérica en Ada ── escribir contratos con tipos y lograr la reutilización sin costo en tiempo de ejecución
Explica de forma sistemática los genéricos de Ada: subprogramas, paquetes, parámetros formales y categorías de tipo, con pautas de diseño...
Programación de sistemas de tiempo real con Ada — Control práctico de prioridad, periodo y tiempo de ejecución
Aprenda el Annex D de Ada (sistemas de tiempo real) con 8 ejemplos prácticos de código: prioridad de tareas, Ceiling_Locking, ejecución p...
Concurrencia segura en Ada — Guía práctica de tareas y objetos protegidos
Introducción a las tareas y objetos protegidos de Ada: rendezvous, aceptación selectiva, exclusión mutua, llamadas con tiempo de espera y...
Introducción a la verificación formal con SPARK ── De los contratos de Ada a la demostración matemática
Un artículo introductorio y práctico sobre la verificación formal con SPARK, el subconjunto de Ada. Repasa cómo pasar de los contratos (P...
Cómo funcionan el portapapeles y arrastrar y soltar — Gestionar correctamente la transferencia de datos OLE en aplicaciones empresariales
Una tabla de Excel se deforma al pegarla y deja de poder pegarse si cierra el origen: es el portapapeles colocando el mismo contenido en ...
Temas relacionados
Estas páginas sitúan el tema en un contexto más amplio de servicios y decisiones.
Temas técnicos de Windows
Portal sobre desarrollo de Windows, investigación de fallos y aprovechamiento de activos existentes.
Preguntas frecuentes
Preguntas habituales en las consultas sobre el tema del artículo.
- ¿El lenguaje Ada todavía se utiliza hoy en día?
- Sí, se sigue utilizando. Se emplea desde hace décadas en sistemas de alta fiabilidad donde un fallo pone en riesgo vidas humanas o provoca pérdidas económicas enormes: control de vuelo de aviones comerciales, control del tráfico aéreo, sistemas de señalización y seguridad ferroviaria, cohetes y satélites, sistemas de defensa y equipos médicos. Ada es un lenguaje que se ha revisado durante más de 40 años: comenzó con Ada 83 en 1983 y, pasando por Ada 95, Ada 2005 y Ada 2012, su estándar más reciente es Ada 2022.
- ¿En qué se diferencia el tipado fuerte de Ada del de otros lenguajes?
- En Ada, dos tipos declarados con nombres distintos se tratan como tipos diferentes aunque su estructura sea exactamente la misma. Por ejemplo, si se crean los tipos Meters y Seconds a partir de Float, mezclarlos provoca un error de compilación y cualquier conversión debe escribirse de forma explícita. Además, con subtype es posible dotar a un tipo de una restricción de rango de valores (por ejemplo, de 0 a 100), y su incumplimiento genera en tiempo de ejecución la excepción Constraint_Error. Es un diseño que evita errores como la confusión de unidades no mediante la precaución, sino haciendo que, directamente, la compilación no pase.
- ¿Cómo puedo probar el lenguaje Ada de forma gratuita?
- Con GNAT (el compilador de Ada gratuito incluido en GCC) y Alire (el gestor de paquetes y herramienta de compilación de Ada, cuyo comando es alr) se obtiene un entorno de desarrollo completo y gratuito tanto en Windows como en Linux o macOS. Basta con descargar el instalador desde el sitio oficial de Alire, crear la plantilla con alr init --bin, compilar con alr build y ejecutar con alr run: una experiencia muy cercana a la de cargo en Rust. Como el propio Alire descarga la cadena de herramientas, ni siquiera es necesario instalar el compilador manualmente. Para VS Code existe la extensión de Ada creada por AdaCore.
- ¿Cuáles son los puntos débiles del lenguaje Ada?
- Entre ellos se encuentran un ecosistema reducido, con menos opciones de frameworks web, GUI o SDK en la nube que los lenguajes dominantes; escasez de profesionales e información (especialmente en japonés), lo que obliga a prever un coste de formación; una sintaxis de declaración de tipos y de separación entre especificación y cuerpo que puede resultar pesada para scripts pequeños; y un mercado laboral concentrado en sectores como la aeroespacial, la defensa o el ferrocarril. Además, como muestra el accidente del Ariane 5 en 1996, conviene tener presente que los mecanismos de seguridad del lenguaje no sustituyen al proceso de revisar las premisas de diseño.
Perfil del autor
Página de presentación del autor del artículo.
Go Komura
Representante de KomuraSoft LLC
Especializado en desarrollo de software para Windows, consultoría técnica e investigación de fallos, sobre todo en proyectos con sistemas existentes y errores difíciles de reproducir.