Design by Contract syntax also comes with some very useful keywords such as old; in Eiffel the return value always has a name, called Result (this, by the way, encourages structured programming where control flow is expressed with if-then-else, making control flow visually clear via scoping), so there it is easy to refer to it when forming a post-condition; e.g.
positive: result > 0
One simple function I've found extremely blissful for contract programming is implies, defined as
implies a b = not a or b
As an example, transitivity expressed with implication/entailment:
(a > b and b > c) implies (a > c)
It's a bit of a shame we can use neither the natural words for logical operators, nor their symbolic representatives.
I may sound like a broken record, always praising Eiffel but there's also much to be loved about C#. Iterators, lamda expressions and extension methods for example. It doesn't hurt to look around though. Contracts are a way to specify, constrain and verify the state machines we are surrounded with.