Design by Contract in C for use in Automated Theorem Proving

Question

I'm working on a couple of C projects and I'd like to use automated theorem proving to validate the code. Ideally I'd just like to use the ATP to validate the functions contracts. Is there any functionality in C/gcc or external software/packages/etc that would enable design-by-contract style coding?

If not then thats just incentive to get started on my own.

My references for this would be something like Spec# or Sing# from MSR, but I'm an open source guy and I'm looking for open source solutions.

Answer 1

Open-Source:check.

Automated Theorem Proving:check.

You should really like Frama-C and its ACSL specification language. You might have already heard about its Caduceus ancestor, but at this time it is considered superseded by Frama-C/Jessie.

Answer 2

Obviously it is not built into the language, but there are plenty of add-ons to get you going. Most of them are beta - but you might consider contributing to them rather than starting your own.

The one at RubyForge, Design by Contract for C, looks very promising. GNU Nana has been around for a long time and will probably suit your needs fine. Hope these are helpful.

Edit: Check out this article at O'Reily on Design By Contract for C:

Not satisfied with assert() and excited about Design by Contract, I set out to create my own Design by Contract implementation for C. After looking at some of the solutions available for Java 1 I decided to use a subset of the Object Constraint Language to express contracts [4]. Using Ruby and Racc, I created Design by Contract for C, a code generator that turns contracts embedded in C comments into C code to check the contracts.