Un Truco de HAT: Verificación Automática de Invariantes de Representación Usando Autómatas Finitos Simbólicos

Los programas funcionales típicamente interactúan con bibliotecas con estado que ocultan el estado detrás de abstracciones tipadas. Una clase de aplicaciones particularmente importante son las implementaciones de estructuras de datos que dependen de tales bibliotecas para proporcionar un nivel de eficiencia y escalabilidad que puede ser difícil de lograr de otra manera. Sin embargo, dado que las especificaciones de los métodos proporcionados por estas bibliotecas son necesariamente generales y rara vez especializadas para las necesidades de un cliente específico, cualquier invariante necesario a nivel de aplicación debe expresarse a menudo en términos de restricciones adicionales sobre el estado (a menudo) opaco mantenido por la biblioteca. En este documento, consideramos la especificación y verificación de tales invariantes de representación utilizando autómatas finitos simbólicos (SFA). Demostramos que los SFA se pueden utilizar para capturar de manera sucinta y precisa historias de interacciones temporales y dependientes de datos entre clientes funcionales y bibliotecas con estado. Para facilitar el razonamiento modular y composicional, integramos SFA en un sistema de tipos de refinamiento para calificar cálculos con estado resultantes de tales interacciones. La instanciación particular que consideramos, Tipos de Autómatas de Hoare (HATs), nos permite especificar y verificar automáticamente los invariantes de representación de un tipo de datos, incluso cuando su implementación depende de métodos de bibliotecas con estado que operan sobre un estado oculto. También desarrollamos un nuevo algoritmo de verificación de tipos bidireccional que implementa una verificación de inclusión de subtipos eficiente sobre HATs, lo que permite su traducción a una forma adecuada para la verificación automatizada basada en SMT. Presentamos resultados experimentales extensos sobre una implementación de este algoritmo que demuestra la viabilidad de verificar tipos en implementaciones de estructuras de datos OCaml especificadas por HAT complejas y sofisticadas.