Lenguaje de especificación ANSI / ISO C - ANSI/ISO C Specification Language

El lenguaje de especificación ANSI / ISO C ( ACSL ) es un lenguaje de especificación para programas C , que utiliza pre y poscondiciones e invariantes de estilo Hoare , que sigue el paradigma de diseño por contrato . Las especificaciones se escriben como comentarios de anotaciones en C para el programa en C, que por lo tanto se pueden compilar con cualquier compilador de C.

La herramienta de verificación actual para ACSL es Frama-C . También implementa un lenguaje hermano, ANSI / ISO C ++ Specification Language ( ACSL ++ ), definido para C ++ .

Visión general

En 1983, el American National Standards Institute (ANSI) encargó a un comité, X3J11, que estandarizara el lenguaje C. El primer estándar para C fue publicado por ANSI. Aunque este documento fue adoptado posteriormente por la Organización Internacional de Normalización (ISO) y ANSI ha adoptado las revisiones posteriores publicadas por ISO, el nombre ANSI C sigue utilizándose.

ACSL es un lenguaje de especificación de interfaz de comportamiento (BISL). Su objetivo es especificar las propiedades de comportamiento del código fuente C. La principal inspiración para este idioma viene del lenguaje de especificación de la herramienta para la verificación del caduceo deductiva de propiedades de comportamiento de los programas en C . El lenguaje de especificación de Caduceus está inspirado en JML, que apunta a objetivos similares para el código fuente de Java.

Una diferencia con JML es que ACSL tiene como objetivo la verificación estática y la verificación deductiva, mientras que JML tiene como objetivo la verificación de afirmaciones en tiempo de ejecución y la verificación estática utilizando, por ejemplo, la herramienta ESC / Java .

Sintaxis

Considere el siguiente ejemplo para el prototipo de una función denominada incrstar:

/*@ requires \valid(p);
  @ assigns *p;
  @ ensures *p == \old(*p) + 1;
  @*/
void incrstar (int *p);

El contrato viene dado por el comentario que comienza con /*@. Su significado es el siguiente:

• la primera línea es una condición previa: establece que la función incrstardebe llamarse con un puntero pque apunte a una ubicación de memoria asignada de forma segura.
• La segunda línea es una cláusula de marco, que indica que la función incrstarno modifica ninguna ubicación de memoria, excepto la apuntada por p.
• Finalmente, la ensurescláusula es una condición posterior, que especifica que el valor *pse incrementa en uno.

Una implementación válida de la función anterior sería:

void incrstar (int *p) {
    (*p)++;
}

Soporte de herramientas

La mayoría de las funciones de ACSL son compatibles con Frama-C .

El analizador estático TrustInSoft es un derivado comercial de Frama-C. Verifica el comportamiento del programa y (con reglas integradas basadas en la especificación del lenguaje) detecta casos de comportamiento indefinido .

Referencias

• Ejemplo de uso de ACSL Condiciones previas suficientes para la verificación de afirmación modular en VMCAI 2008, páginas 188-202.
• ACSL by Example , una colección bien documentada de especificaciones de ACSL de algoritmos simples, es desarrollada y mantenida por VerificationGroup en Fraunhofer FOKUS
• Un tutorial sobre Frama-C con WP y ACSL para principiantes que también proporciona algunas ideas sobre la teoría detrás de las herramientas ( disponible también en francés ).
• Un informe sobre el uso de ACSL y Frama-C para formular y verificar requisitos de bajo nivel en el contexto de un proyecto compatible con DO-178C
• Informe que menciona el uso de ACSL en la enseñanza [1] , Петренко Ольга Леонидовна y Хорошилов Алексей Владимирович.
• En Technikum Wien, ACSL y Frama-C se imparten en un curso sobre diseño y verificación .

enlaces externos

• La especificación completa de ACSL está disponible en la página de descarga de Frama-C .
• TSnippet de TrustInSoft permite realizar pruebas en el navegador de fragmentos de código C mediante ACSL.