Conception par contrat en C pour l'utilisation dans le théorème automatisé Proving

Question

Je travaille sur un couple de projets C et je voudrais utiliser le théorème automatisé prouvant pour valider le code. Idéalement, j'aimerais simplement utiliser l'ATP pour valider les contrats de fonctions. Y a-t-il des fonctionnalités dans C/gcc ou des logiciels/packages/etc externes qui permettent le codage de style par contrat?

Si ce n'est pas le cas, c'est juste une incitation à démarrer moi-même. Mes références pour cela seraient quelque chose comme SpeC# ou Sing # de MSR, mais je suis un gars open source et je suis à la recherche de solutions open source.

Answer 1

De toute évidence, il n'est pas intégré dans la langue, mais il existe de nombreux modules complémentaires pour vous aider à démarrer. La plupart d'entre eux sont bêta - mais vous pourriez envisager de contribuer à eux plutôt que de commencer le vôtre.

Celui de RubyForge, Design by Contract for C, semble très prometteur. GNU Nana a été autour depuis longtemps et répondra probablement à vos besoins. Espérons que ce sont utiles.

Edit: Consultez this article at O'Reily sur la conception par contrat C:

Non satisfait assert() et enthousiasmés par la conception par contrat, je mis à créer ma propre conception par mise en œuvre du contrat pour C. Après en regardant certaines des solutions disponibles pour Java 1 j'ai décidé de utiliser un sous-ensemble de la contrainte d'objet Langue pour exprimer des contrats [4]. En utilisant Ruby et Racc, j'ai créé le modèle par contrat pour C, un générateur de code qui transforme les contrats incorporés dans les commentaires C en code C pour vérifier les contrats .

Answer 2

Open-Source: vérifier.

Calcul automatique du théorème: vérifier.

Vous devriez vraiment aimer Frama-C et son langage de spécification ACSL. Vous avez peut-être déjà entendu parler de son ancêtre Caduceus, mais à ce moment-là, il est considéré comme dépassé par Frama-C/Jessie.

Answer 3

Si vous souhaitez valider le code C à l'aide de prouveurs de théorèmes, vous devez vérifier le VCC project. De leur page Web:

VCC est un vérificateur mécanique pour les programmes C concurrents. VCC prend un programme C , annoté avec des spécifications de fonction, invariants de données, boucle invariants, et le code fantôme, et essaie de prouver ces annotations correct. Si cela réussit, VCC promet que votre programme répond réellement aux spécifications de son .

est CCV système très mature de Microsoft Research, et a été utilisé pour vérifier l'hyperviseur de Microsoft Hyper-V. VCC est également open source.