¿Se necesitan precondiciones y postcondiciones además de invariantes en las funciones de los miembros si se realiza el diseño por contrato?

Question

Entiendo que en el método DbC, las condiciones previas y posteriores se adjuntan a una función.

Lo que me pregunto es si eso también se aplica a las funciones de los miembros.

Por ejemplo, suponiendo que use invariantes al principio al final de cada función pública, una función miembro se verá así:

editar: (limpié mi ejemplo)

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);
}

¿Está bien usar condiciones previas y posteriores con funciones globales / genéricas solamente y solo usar invariantes dentro de las clases?

Esto parece una exageración, pero quizás mi ejemplo es malo.

editar:

¿No es la condición posterior solo verificar un subconjunto de la invariante?

En lo anterior, estoy siguiendo las instrucciones de http://www.digitalmars.com /ctg/contract.html que establece, "El invariante se verifica cuando un constructor de clase se completa, al comienzo del destructor de clase, antes de que se ejecute un miembro público y después de que finalice una función pública." / p>

Gracias.

Answer 1

Sí.

La clase C invariante es una propiedad común de todas sus instancias (objetos). El invariante se evalúa como verdadero si y solo si el objeto está en un estado semánticamente válido.

El invariante de un ascensor puede contener información como ASSERT (IsStopped () || Door.IsClosed ()) , porque no es válido para un ascensor estar en un estado diferente al detenido (por ejemplo, subiendo) y con la puerta abierta.

En contraste, una función miembro como MoveTo (int flat) puede tener CurrentFlat () == flat como postcondición ; porque después de una llamada a MoveTo (6), el piso actual es 6. De manera similar, puede tener IsStopped () como una condición previa , porque (según el diseño) puede invoque la función MoveTo si el elevador ya está en movimiento. Primero, debe consultar su estado, asegurarse de que esté detenido y luego llamar a la función.

Por supuesto, puedo simplificar demasiado el funcionamiento de un ascensor.

En cualquier caso, las precondiciones y postcondiciones no tendrán sentido, en general, como condiciones invariables; un elevador no necesita estar en el piso 6 para estar en un estado válido.

Un ejemplo más conciso se puede encontrar aquí: Intercepción y atributos: una muestra de diseño por contrato de Sasha Goldshtein .

Answer 2

Restringir los contratos en las clases a invariantes no es óptimo.

Las condiciones previas y posteriores no son solo un subconjunto de los invariantes.

Las invariantes, precondiciones y postcondiciones tienen roles muy diferentes.

Las invariantes confirman la coherencia interna del objeto. Deben ser válidos al final del constructor y antes y después de cada llamada al método.

Las condiciones previas verifican que el estado del objeto y los argumentos sean adecuados para la ejecución del método. Las condiciones previas son complementarias a las invariantes. Cubren la comprobación de los argumentos (una comprobación más fuerte de que el tipo en sí mismo, es decir, no es nulo, > 0, etc.), pero también podría comprobar el estado interno del objeto (es decir, una llamada a file.write ( " ; hola " ) es una llamada válida solo si file.is_rw y file.is_open son verdaderos).

Las condiciones posteriores indican que el método cumplió con su obligación Las condiciones posteriores también son complementarias de los invariantes. Por supuesto, el estado del objeto debe ser coherente después de la ejecución del método, pero las condiciones posteriores verifican que se realizó la acción esperada (es decir, list.add (i) debería tener como consecuencia que list.has (i) es verdadero y list.count = old list.count + 1).

Answer 3

Bueno, el punto de una invariante es que describe algo que es verdadero del objeto en todo momento . En este caso, algo está a la parrilla o no (nada en el medio). Normalmente describen una propiedad del estado completo del objeto.

Las condiciones previas y posteriores describen cosas que son ciertas justo antes de que se ejecute un método, y justo después, y se referirán a solo el estado que el método debería haber tocado . Esto es diferente, presumiblemente, del estado del objeto. Se podría pensar que las condiciones previas y posteriores describen la huella de un método, justo lo que necesitaba, justo lo que tocaba.

Entonces, para la pregunta específica, las ideas hacen cosas diferentes, por lo que es posible que desee ambas. Ciertamente, no puede usar invariantes en lugar de condiciones previas y posteriores; en este caso, parte del objeto invariante es "Algo está en la parrilla o no", pero la condición previa de lightOnFire necesita saber que el artículo está en la parrilla. Nunca se puede inferir esto del objeto invariante. Es cierto que a partir de las condiciones previas y posteriores y de un estado de inicio conocido, puede (suponiendo que la estructura de los objetos solo es mutable a través de métodos, y las condiciones previas y posteriores describen todos los cambios ambientales), inferir un objeto invariante. Sin embargo, esto puede ser complejo, y cuando estás diciendo cosas '' en lenguaje '', es más fácil proporcionar ambas.

Por supuesto, hacer variantes que dicen que un elemento booleano es verdadero o falso no tiene sentido, el sistema de tipos lo garantiza.