Are preconditions and postconditions needed in addition to invariants in member functions if doing design by contract?

Question

I understand that in the DbC method, preconditions and postconditions are attached to a function.

What I'm wondering is if that applies to member functions as well.

For instance, assuming I use invariants at the beginning at end of each public function, a member function will look like this:

edit: (cleaned up my example)

void Charcoal::LightOnFire() {
  invariant();
  in_LightOnFire();

  StartBurning();    
  m_Status = STATUS_BURNING;
  m_Color = 0xCCCCCC;

  return; // last return in body

  out_LightOnFire();
  invariant();
}

inline void Charcoal::in_LightOnFire() {
  #ifndef _RELEASE_
  assert (m_Status == STATUS_UNLIT);
  assert (m_OnTheGrill == true);
  assert (m_DousedInLighterFluid == true);
  #endif
}

inline void Charcoal::out_LightOnFire() {
  #ifndef _RELEASE_
  assert(m_Status == STATUS_BURNING);
  assert(m_Color == 0xCCCCCC);
  #endif
}

// class invariant
inline void Charcoal::invariant() {
  assert(m_Status == STATUS_UNLIT || m_Status == STATUS_BURNING || m_Status == STATUS_ASHY);
  assert(m_Color == 0x000000 || m_Color == 0xCCCCCC || m_Color == 0xEEEEEE);
}

Is it okay to use preconditions and postconditions with global/generic functions only and just use invariants inside classes?

This seems like overkill, but maybe its my example is bad.

edit:

Isn't the postcondition just checking a subset of the invariant?

In the above, I am following the instructions of http://www.digitalmars.com/ctg/contract.html that states, "The invariant is checked when a class constructor completes, at the start of the class destructor, before a public member is run, and after a public function finishes."

Thanks.

Answer 1

Well, the point of an invariant is that it describes something that's true of the object at all times. In this case, something is on the grill, or not (nothing in between). They normally describe a property of the entire state of the object.

Pre and post conditions describe things that are true just before a method executes, and just after, and will concern just the state that should have been touched by the method. This is different, presumably, from the state of the object. Pre and post conditions might be thought of as describing the footprint of a method - just what it needed, just what it touched.

So, to the specific question, the ideas do different things, so you may well want both. You certainly cannot just use invariants instead of pre and post conditions - in this instance, part of the object invariant is "Something is on the grill or not", but the precondition of lightOnFire needs to know that the item is on the grill. You can never infer this from the object invariant. It is true that from pre and postconditions and a known start state, you can (assuming that the objects structure is only mutable through methods, and the pre and post conditions describe all the environmental changes), infer an object invariant. However, this can be complex, and when you're stating things "in language", it's easier to just provide both.

Of course, doing in variants that state a boolean item is either true or false is a bit pointless - the type system ensures that.

Answer 2

Yes.

Class C's invariant is a common property of all of its instances (objects). The invariant evaluates to true if and only if the object is in a semantically valid state.

An elevator's invariant may contain information such as ASSERT(IsStopped() || Door.IsClosed()), because it is invalid for an elevator to be in a state different than stopped (say, going up) and with the door open.

In contrast, a member function such as MoveTo(int flat) may have CurrentFlat()==flat as a postcondition; because after a call to MoveTo(6) the current flat is 6. Similarly, it may have IsStopped() as a precondition, because (depending on the design) you can't invoke function MoveTo if the elevator is already moving. First, you have to query its state, make sure that it is stopped, and then call the function.

Of course I may be totally oversimplifying how an elevator works.

In any case, the preconditions and postconditions will make no sense, in general, as invariant conditions; an elevator doesn't need to be at floor 6 to be in a valid state.

A more concise example can be found here: Interception and Attributes: A Design-By-Contract Sample by Sasha Goldshtein.

Answer 3

Restricting the contracts in the classes to invariants is not optimal.

Preconditions and Postconditions are not just a subset of the invariants.

Invariants, Pre-conditions and Post-conditions have very different roles.

Invariants confirms the internal coherence of the object. They should be valid at the end of the constructor and before and after each method call.

Pre-conditions are checking that the status of the object and the arguments are suitable for the execution of the method. Preconditions are complementary to the invariants. They cover the check of the arguments (a stronger check that the type itself, i.e. not null, > 0,.. etc) but also could check for the object internal status (i.e. a call to file.write("hello") is a valid call only if file.is_rw and file.is_open are true).

Post-conditions are cheking that the method satisfied its obligation Post-conditions are also complementary to the invariants. Of course the status of the object has to be coherent after the method execution, but the Post-conditions are checking that the expected action was performed (i.e. list.add(i) should have as consequence that list.has(i) is true and list.count = old list.count + 1).