Des conditions préalables et postconditions sont-elles nécessaires en plus des invariants dans les fonctions membres si la conception est réalisée par contrat?

Question

Je comprends que dans la méthode DbC, les conditions préalables et postconditions sont attachées à une fonction.

Ce que je me demande, c'est si cela s'applique également aux fonctions membres.

Par exemple, en utilisant des invariants au début, à la fin de chaque fonction publique, une fonction membre ressemblera à ceci:

modifier: (nettoyé mon exemple)

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

Puis-je utiliser uniquement les préconditions et les post-conditions avec des fonctions globales / génériques et simplement utiliser des invariants à l'intérieur de classes?

Cela semble exagéré, mais peut-être que mon exemple est mauvais.

modifier:

La postcondition ne vérifie-t-elle pas seulement un sous-ensemble de l'invariant?

Dans ce qui précède, je suis les instructions de http://www.digitalmars.com /ctg/contract.html : "L’invariant est vérifié lorsqu'un constructeur de classe termine, au début du destructeur de classe, avant l’exécution d’un membre public et après la fin d’une fonction publique."

Merci.

Answer 1

Oui.

L ' invariant de la classe C est une propriété commune à toutes ses instances (objets). L'invariant est évalué à true si et seulement si l'objet est dans un état sémantiquement valide.

L'invariant d'un ascenseur peut contenir des informations telles que ASSERT (IsStopped () || Door.IsClosed ()) , car il est incorrect qu'un ascenseur soit dans un état différent de celui arrêté (par exemple, monter) et avec la porte ouverte.

En revanche, une fonction membre telle que MoveTo (int flat) peut avoir CurrentFlat () == flat en tant que postcondition ; Parce que, après un appel à MoveTo (6), l’appartement actuel est 6. De la même façon, il peut avoir IsStopped () comme condition préalable , car (en fonction de la conception), vous pouvez: N'invoquez pas la fonction MoveTo si l'ascenseur est déjà en mouvement. Tout d'abord, vous devez interroger son état, assurez-vous qu'il est arrêté, puis appeler la fonction.

Bien sûr, je simplifie peut-être totalement le fonctionnement d'un ascenseur.

En tout état de cause, les conditions préalables et postconditions n’auront aucun sens, en général, en tant que conditions invariantes; un ascenseur n'a pas besoin d'être au 6ème étage pour être dans un état valide.

Vous trouverez un exemple plus concis ici: Interception et attributs: exemple de conception par contrat de Sasha Goldshtein .

Answer 2

Limiter les contrats des classes aux invariants n’est pas optimal.

Les préconditions et les postconditions ne sont pas simplement un sous-ensemble des invariants.

Les invariants, les pré-conditions et les post-conditions ont des rôles très différents.

Les invariants confirment la cohérence interne de l'objet. ils doivent être valides à la fin du constructeur et avant et après chaque appel de méthode.

Les conditions préalables vérifient que le statut de l'objet et les arguments conviennent à l'exécution de la méthode. Les conditions préalables sont complémentaires aux invariants. Ils couvrent la vérification des arguments (vérification plus forte que le type lui-même, c'est-à-dire non nul, > 0, etc.), mais peuvent également vérifier le statut interne de l'objet (c'est-à-dire un appel à file.write ( " ; hello " ) est un appel valide uniquement si file.is_rw et file.is_open ont la valeur true).

Les conditions postérieures indiquent que la méthode a satisfait à son obligation Les conditions postérieures sont également complémentaires des invariants. Bien sûr, le statut de l'objet doit être cohérent après l'exécution de la méthode, mais les post-conditions vérifient que l'action attendue a été effectuée (c'est-à-dire que list.add (i) doit avoir pour conséquence que list.has (i) est vrai. et list.count = old list.count + 1).

Answer 3

Eh bien, l'intérêt d'un invariant est qu'il décrit quelque chose qui est vrai de l'objet à tout moment . Dans ce cas, quelque chose est sur le gril ou non (rien entre les deux). Ils décrivent normalement une propriété de l’ensemble de l’état de l’objet.

Les conditions avant et après décrivent les choses qui sont vraies juste avant l'exécution d'une méthode et juste après, et concernent uniquement l'état qui aurait dû être touché par la méthode . Ceci est probablement différent de l'état de l'objet. Les conditions préalables et postérieures peuvent être considérées comme décrivant l'empreinte d'une méthode - exactement ce dont elle avait besoin, exactement ce qui la touchait.

Donc, pour la question spécifique, les idées ont des effets différents, vous voudrez donc peut-être les deux. Vous ne pouvez certainement pas simplement utiliser des invariants à la place de conditions préalables et postérieures - dans ce cas, une partie de l'invariant d'objet est "Quelque chose est sur le gril ou non", mais la condition préalable de lightOnFire doit savoir que l'élément est sur le gril. Vous ne pouvez jamais déduire cela de l'invariant d'objet. Il est vrai que, à partir des conditions préalables et postérieures et d'un état de démarrage connu, vous pouvez (en supposant que la structure de l'objet ne peut être modifiée que par des méthodes et que les conditions préalables et ultérieures décrivent tous les changements environnementaux), induire un invariant d'objet. Toutefois, cela peut être complexe et lorsque vous énoncez des mots "en langage", il est plus facile de fournir les deux.

Bien sûr, le fait de spécifier dans les variantes qu’un élément booléen est vrai ou faux n’a aucun sens - le système de types le garantit.