Diseño por contrato en C para usar en la demostración automatizada de teoremas

Question

Estoy trabajando en un par de proyectos de C y me gustaría utilizar la demostración automática de teoremas para validar el código. Idealmente, me gustaría utilizar el ATP para validar los contratos de funciones. ¿Hay alguna funcionalidad en C/gcc o software/packages/etc externos que permita la codificación de estilo de diseño por contrato?

Si no, entonces eso es solo un incentivo para comenzar por mi cuenta.

Mis referencias para esto sería algo así como SpeC# o # Sing de MSR, pero yo soy un tipo de código abierto y estoy en busca de soluciones de código abierto.

Answer 1

Obviamente, no está incorporado en el idioma, pero hay muchos complementos para que funcione. La mayoría de ellos son beta, pero puede considerar contribuir a ellos en lugar de comenzar el suyo.

El que está en RubyForge, Design by Contract for C, se ve muy prometedor. GNU Nana ha existido por mucho tiempo y probablemente se adapte bien a sus necesidades. Espero que estos sean útiles.

Editar: Salida this article at O'Reily en Diseño por contrato para C:

No satisfecho con assert() y entusiasmados Diseño por contrato, que se dispuso a crear mi propio diseño de aplicación del contrato de C. Después de mirar algunas de las soluciones disponibles para Java 1 decidí utilizar un subconjunto de objetos restricción lenguaje para expresar los contratos [4]. Usando Ruby y Racc, creé Design por Contract for C, un generador de código que convierte los contratos incrustados en C en código C para verificar los contratos .

Answer 2

de código abierto: cheque.

Prueba del teorema automatizado: comprobar.

Usted debe realmente como Frama-C y su lenguaje ACSL especificación. Es posible que ya haya oído hablar de su ancestro caduceo, pero en este momento se considera reemplazado por Frama-C/Jessie.

Answer 3

Si usted está interesado en la validación de código C utilizando demostradores de teoremas, usted debe comprobar la VCC project. De su página web:

VCC es un verificador mecánico para programas concurrentes C. VCC tiene un programa en C , anotado con las especificaciones de función, invariantes de bucle de datos, invariantes, y el código fantasma, y ​​trata de probar estas anotaciones correcta. Si tiene éxito, VCC promete que su programa realmente cumple con sus especificaciones.

VCC es muy maduro sistema de Microsoft Research, y se ha utilizado para verificar el hipervisor de Microsoft Hyper-V. VCC también es de código abierto.