Using Design by Contract in C
Subject:   No side effects (contract vs. assert)
Date:   2004-11-12 00:06:04
From:   cmills
Response to: No side effects (contract vs. assert)

Now I'm confused, given that the author stresses that code should behave the same with or without DBC active; the implementation given calls abort() just as assert() would...

I guess a better way to think about it is that the code should not be affected by the contract checking unless a contract is broken (in which case the program can ideally terminate and spit out some useful info about the problem).

The kind of side effects you need to be warry of are:
(1) changing the value of variables
(2) calling functions that change the state of your program

DBC for C doesn't allow assignment, which pretty much takes care of (1). But (2) is still a problem. Take for example:
post: Stack_pop(s) == elem
void Stack_push(Stack_T s, void *elem)

This statement pops the last value off of the stack s in order to check the condition. That is a side effect.
Here is a better way:
post: Stack_peek(s) == elem

post: s->length == s->length @ pre + 1
post: s->array[s->length - 1] == elem

Big words (DBC), business as usual...

Don't get put off by catchy nomenclature :) Try it out, see if it meets your needs.