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.

Ungraceful

Answer 1

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.

Reconcile

Answer 2

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.

Latchstring

Answer 3

If you are interested in validating C code using theorem provers, you should check the VCC project. From their webpage:

VCC is a mechanical verifier for concurrent C programs. VCC takes a C program, annotated with function specifications, data invariants, loop invariants, and ghost code, and tries to prove these annotations correct. If it succeeds, VCC promises that your program actually meets its specifications.

VCC is very mature system from Microsoft Research, and has been used to verify the hypervisor of Microsoft Hyper-V. VCC is also open source.

Greathouse