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

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).