Cette classe est-elle un sous type légitime ?

Bonsoir à tous,

Je suis fasse à un cas un peu limite ou on me demande de justifier si la classe Compteur2 est bien un sous-type légitime de Compteur0 au sens du principe de substitution de Liskov, sachant que¹

class Compteur0 {
    Compteur0() { ... }

    // post-condition: this_post > this
    public void incr() { ... }
}

class Compteur2 extends Compteur0 {
    Compteur2() {...}

    // pre-condition: val > 0
    // post-condition: this_post = this + val
    public void incr(int val) { ... }
}

En fait, la question est très simple: est ce que, vu que incr(int val) est une fonction qui n’a rien à voir avec incr() (c’est pas une re-définition), le LSP ne s’applique pas (auquel cas tout ce passe bien), ou est ce que le LSP s’applique malgré tout (auquel cas il y a renforcement de la pré-condition, donc violation du LSP).

Si il y a des motivés de la preuve de programme qui passent par ici, merci d’avance

M’en doutais un peu. Évidement, il n’y a aucun risque, puisque la méthode void incr() est hérité telle quelle (donc pré et post conditions inchangées) et que void incr(int val) est spécifique à Compteur2.

Merci, c’était pour être sur. En fait, "ma" (enfin, celle de mon cours) définition du LSP est la suivante:

Si $S$S est un sous-type de $T$T, les objets de type $S$S doivent pouvoir être utilisé dans tout contexte qui requiert des objets de type $T$T.

Et jusque là, pas de problème.

Néanmoins, il ajoute que:

… Et je voulais bien être sur que ladite "règle des signatures" s’appliquait uniquement aux méthodes qui ont été redéfinies (override): il est logique que oui, mais comme le LSP est assez restrictif, on ne sait jamais.

EDIT: j’avais complètement zappé qu’il existait un tuto sur la preuve de programme sur ZdS

Mieux vaut passer par la bêta et aller chercher la version anglaise, elle est beaucoup, beaucoup, beaucoup plus à jour.

Pour ceux que ça amuse, on m’a soumis une question plus pénible récemment sur le sujet. En gros : est ce que les propriétés temporelles devraient entrer dans le cadre du principe de substitution. Par exemple si j’ai un type de base :

class Foo {
public:
  /*@
    requires this->val >= 0
    ensures this->val > \old(this->val) ;
  */
  void incr();

  /*@
    ensures this->val < \old(this->val) ;
  */
  void decr();
};

On a une propriété temporelle implicite qui est que si la valeur de l’objet passe en dessous de 0, elle ne peut plus jamais passer au dessus de 0. Supposons que maintenant, je crée une nouvelle classe qui en dérive et que j’ajoute une méthode:

class Bar : public Foo {
public:
  /*@
    ensures this->val == \old(this->val) * x ;
  */
  void mul(int x) ;
}

En utilisant la fonction mul, je ne change aucunement les contrats de incr et decr et pourtant, je peux casser la propriété temporelle si je trouve un chemin qui me permet de passer par mul par le jeu des surcharges ce qui casserait le LSP ? Ou pas ? Est ce qu’il est possible de trouver un tel chemin ?

J’ai potassé un peu sur le problème mais je n’ai pas la réponse donc si ça intéresse quelqu’un

@Ksass`Peuk : ton énigme est intéressante, j’ai réfléchi un peu.

J’ai l’impression que la différence-clé est que dans le premier exemple, on ne peut pas sortir de l’état "val < 0", alors que dans le deuxième, on crée un nouveau chemin possible qui permet de revenir à l’état "val >= 0". En gros, les séquence d’états valides seront différentes.

Ensuite fouillant Wikipedia, on voit que ce problème est intégré dans le LSP. Je cite la page du LSP :

History constraint (the "history rule"). Objects are regarded as being modifiable only through their methods (encapsulation). Because subtypes may introduce methods that are not present in the supertype, the introduction of these methods may allow state changes in the subtype that are not permissible in the supertype. The history constraint prohibits this. It was the novel element introduced by Liskov and Wing.

En bref, si on permet dans un sous-type des évolutions de l’état (à définir) impossible avec le sur-type, on viole le principe. Malheureusement, je n’ai pas pu lire l’article pour en savoir plus.

Quoi qu’il en soit, ça montre que les propriétés temporelles ne sont pas du tout triviales et que les preuves dessus sont utiles pour éviter de créer des états bizarres non maîtrisés (comme dans l’exemple du compteur).

Intéressant que ce soit intégré à la règle du LSP, je n’en avais pas le souvenir et pourtant je l’ai potassée une paire de fois.

Bah c’est d’autant plus non-trivial que la preuve ne nous aidera pas forcément. En l’occurrence, ici la propriété temporelle est dérivée des contrats et une fois que l’on sait ce que l’on doit chercher (une preuve que si l’on devient négatif alors on n’est plus jamais positif), c’est trivial de trouver l’explication, en revanche, on n’a a priori pas d’information de ce que l’on doit chercher.

Ici l’exemple est trivial, mais sur des exemples plus complexes, on doit quelque part trouver une preuve que "pour toute propriété temporelle dérivable de mes contrats, ma nouvelle classe ne casse pas la propriété". Et ces propriétés temporelles ne sont pas forcément explicites. Après par contre, on peut raisonnablement penser que si l’on a un programme utilisateur qui dépend d’une telle propriété, sa preuve aura nécessité d’expliciter la propriété, mais ça rend le respect du LSP sensiblement contextuel ce qui n’est jamais bon pour la modularité.

J’ai tendance à voir la formulation usuelle du LSP comme une formulation microscopique permettant d’assurer que

Tout protocole valable sur un objet d’un type doit rester valable sur un objet d’un sous-type

Où protocole est à prendre comme synonyme de suite de messages envoyé à l’objet; et rester valable comme le respect des préconditions induit le respect des mêmes post-conditions.

Et en ce sens la fonction mul ne change rien à priori : aucun protocole impliquant uniquement les messages valables sur le type de départ (donc incr et decr) ne peut impliquer le message mul — sinon ce protocol n’est plus valable pour un objet du type de départ.

C’est en ce sens que je dis que le LSP devient contextuel. Parce que tu ne peux pas présumer depuis la classe de base, ou la classe dérivée en cours de développement, du protocole qui va être appliqué dessus, tu es obligé de connaître ce protocole.

Sauf si :

Personnellement, c’est la propriété que j’attendrais. Seulement pour ça, on a besoin d’une preuve que pour tout programme sur le type de départ, aucun chemin ne peut permettre d’appeler mul même s’il y a remplacement d’autres objets (en respect du LSP), et autre manipulation du genre. Et autant si je ne vois pas de contre-exemple trivial, je ne vois pas non plus comment construire une preuve que si on respecte tout le temps le LSP alors un tel chemin ne peut pas exister.

EDIT: après, pour être facilement blindé, on peut faire un truc très simple : forcer la règle "tout attribut est privé". De cette manière, mul ne peut pas accéder directement à la valeur interne de sa classe parente et il n’y a plus de question à se poser : elle ne peut plus remplir son contrat. Dans un tel cas, je pense que la preuve est à peu près triviale.

Je tends à rejoindre Freedom. Le LSP va se respecter sur ces protocoles, si un protocole exprimé sur le type parent permet de casser l’objet, l’enfant ni est pour rien (enfin… ce n’est pas un problème de LSP pour moi s’il n’y a aucune violation supplémentaire qui soit locale ou globale — mais que la violation était déjà bien là au niveau parent)

Et si c’est un protocole exclusif au type enfant qui met la pagaille…. (*), je ne tends pas à voir ça comme un problème de LSP, mais un mélange d’OCP non respecté et de mauvaise encapsulation. Probablement un mauvais design in fine. Mais que je ne range pas dans la case LSP, car on ne substitue rien sur un chemin exclusif hors sentiers de l’OCP.

(*) mul n’existait pas au niveau parent, et aucun chemin n’y conduisait.

Ok, je vais présenter un petit "contre-exemple" où à mon sens, le fautif n’est pas si facile à trouver (note: je considère que l’on est dans le cas où le champ est protected, sinon c’est effectivement trivial). En conservant les classes précédentes. On peut imaginer deux autres classes utilisatrices suivantes :

class Other {
public:
  Other();
  void up_1(){ m_foo.dec(); }
  virtual void up_2();
  virtual Foo& get(){ return m_foo ; }
private:
  Foo m_foo ;
};

class Derived : public Other {
public:
  void up_2(){ m_bar.mul(-2); }
  Foo& get() { return m_bar ; }
private:
  Bar m_bar ;
};

Et on pourrait avoir un code appelant où il se passe ça :

Other o ;

while(o.get().is_positive()){
  o.up_1();
}
//ici l'objet obtenu est censé ne plus pouvoir être positif

o.up_2();

La question qui ne me semble pas si trivial c’est "est ce que c’est le faute de Derived ou de Bar ?". Parce que c’est Bar qui casse un contrat temporel en permettant mul même si c’est Derived qui va déclencher la situation qui casse le contrat au final. Et le problème de cette propriété c’est qu’on ne la voit pas localement.

Je suis toujours en désaccord. Je vais développer avec ton exemple complété.

Le contrat de départ (et les protocoles et propriétés que tu peux construire depuis celui-ci) te dis en effet

Si un objet devient négatif pendant un protocole valable sur le type de base, il ne peut plus devenir positif.

Sauf que ton opération o.up_2() revient au message mul qui est invalide sur un objet du type de base, il ne fait donc pas parti d’un protocole valable sur le type de base. Par contre ça concerne bien les lignes 3–5 de ton code pour lequel la propriété que tu as identifié est bien respectée.

A ce moment là, on interdit complètement l’appel d’une méthode ajoutée par un objet enfant dans le jeu des appels virtuels. Je veux bien, mais là tu passes sur une situation où tu dois en permanence vérifier une énorme propriété globale. C’est extrêmement restrictif, beaucoup plus que le LSP.

Pourquoi tu conclus à cette interdiction ? Pour moi ton code respecte le LSP, alors que tu penses que non, j’ai du mal à voir en quoi je suis plus restrictif du coup !?

Si je reformule un peu j’ai l’impression que la formulation du LSP que tu supposes ressemble à :

Toute propriété valable sur un objet d’un type doit l’être sur les objets d’un sous-type.

Ça me semble au contraire plus restrictif que la formulation que j’évoque qui se contente des protocoles valables sur un objet du type de base — qui sont inclus par la formulation sur l’ensemble des propriétés.

D’accord. Je vois mieux.

Mais le principe du LSP est de garantir que tout est interchangeable en s’assurant que le contrat reste respecté lorsque l’on change un objet pour son sous-type. Or ici, ce n’est pas le cas : j’ai changé un objet (en l’occurrence deux) pour des objets de sous-types et ma propriété finale (externe) ne tient plus. Si par exemple j’avais un programme qui récupérait la valeur de l’objet pour un appel qui a comme précondition que la valeur est négative, la précondition de l’appel en question serait cassée, ce qui par respect du LSP ne devrait pas pouvoir arriver.

Pour formaliser un peu plus ¹. Si je note :

• $S_T$ST​ l’ensemble des états possibles ² d’un type $T$T, et $o\in S_T$o∈ST​ un objet de type $T$T;
• $U\mid T$U∣T la relation de sous-typage (en particulier $T\mid T$T∣T) et $S$S qui associe a un objet et un de ses sur-types la partie de son état associée a ce sur-type, i.e. $S:o\in S_U,U\mid T\mapsto S(o,T)\in S_T$S:o∈SU​,U∣T↦S(o,T)∈ST​
• $M_T$MT​ l’ensemble des messages associés au type $T$T et $I$I la fonction associant a une message et un type son implémentation — i.e. $I:m\in M_T,U\mid T\mapsto I(m,U)\in {S_U}^{S_U}$I:m∈MT​,U∣T↦I(m,U)∈SU​SU​
• $V_T$VT​ l’ensemble des propriétés caractérisant un objet de type $T$T, cad l’appartenance de cet objet a un sous-ensemble des états possible — les états caractérises par cette propriété — i.e. $V_T\equiv P\left(S_T\right)$VT​≡P(ST​), et pour une propriété $p\in V_T$p∈VT​ on note $v\left(o\right)$v(o) la valeur de vérité de cette propriété sur un objet $o\in S_{U\mid T}$o∈SU∣T​, i.e. $v\left(o\right)\equiv S(o,T)\in v$v(o)≡S(o,T)∈v.

A partir de la je construis deux choses:

• $P_T$PT​ l’ensemble des des protocoles valables associés au type $T$T — i.e $P_T\subset M_T^N$PT​⊂MTN​, et pour un protocole valable $p={(m_n\in M_T)}_{n\in N}\in P_T$p=(mn​∈MT​)n∈N​∈PT​ et un objet $o\in U\mid T$o∈U∣T on note $p\left(o\right)$p(o) l’état a l’issu du protocole, i.e. $p\left(o\right)\equiv {\lim }_{}I(m_n,U)\circ \cdots \circ I(m_0,U)\left(o\right)$p(o)≡limn→∞​I(mn​,U)∘⋯∘I(m0​,U)(o) ³;
• $C_T\equiv V_T,C_T$CT​≡VT​,CT​ le contrat du type $T$T, la première qui a un protocole associe un ensemble de propriétés — les pré-conditions possibles. Et la seconde qui a un protocole et un type — l’implémentation — associe une map entre les pré-conditions et un autre ensemble de propriétés — les post-conditions correspondantes : $V_T:p\in P_T\mapsto V_T\left(p\right)\subset V_T$VT​:p∈PT​↦VT​(p)⊂VT​ $C_T:p\in P_T,U\mid T\mapsto [v^{\prime }\in V_T(p)\mapsto \{S\left(p\right(o),T)\mid o\in U\text{ et }{v}^{\prime }(o\left)\right\}]$CT​:p∈PT​,U∣T ↦ [v′∈VT​(p)↦{S(p(o),T) ∣ o∈U et v′(o)}]

A partit de la, le LSP s’écrit pour moi: $U{\mid }_{LSP}T⟺\forall p\in P_T,\forall v^{\prime }\in V_T\left(p\right),C_T(p,U)\left(v^{\prime }\right)\subset C_T(p,T)\left(v^{\prime }\right)$U ∣LSP​ T⟺∀p∈PT​, ∀v′∈VT​(p), CT​(p,U)(v′)⊂CT​(p,T)(v′)

¹ Vous m’excuserez les notations probablement pas usuel, je n’ai pas les outils formels usuels.
² Ici possible n’implique pas accessible.
³ La convergence est supposée.

Edit: Je n’ai pas lu ta dernière réponse avant d’edit pour ne pas me laisser influencer par ton message. Edit2: Simplification d’une relation.

Mais le principe du LSP est de garantir que tout est interchangeable en s’assurant que le contrat reste respecté lorsque l’on change un objet pour son sous-type.

Ça je pense qu’on est tous d’accord que c’est bien l’objectif du LSP.

Le code en entier (pour reprendre) :

class Foo {
public:
  /*@
    requires this->val >= 0
    ensures this->val > \old(this->val) ;
  */
  void incr();

  /*@
    ensures this->val < \old(this->val) ;
  */
  void decr();
};


class Bar : public Foo {
public:
  /*@
    ensures this->val == \old(this->val) * x ;
  */
  void mul(int x) ;
}

class Other {
public:
  Other();
  void up_1(){ m_foo.dec(); }
  virtual void up_2();
  virtual Foo& get(){ return m_foo ; }
private:
  Foo m_foo ;
};

class Derived : public Other {
public:
  void up_2(){ m_bar.mul(-2); }
  Foo& get() { return m_bar ; }
private:
  Bar m_bar ;
};

Other o ;

while(o.get().is_positive()){
  o.up_1();
}
//ici l'objet obtenu est censé ne plus pouvoir être positif

o.up_2();

Pour reprendre ce que tu viens de dire lorsque l’on change un objet pour son sous-type ca implique quand meme que si je remplace le sous-type (dans les situations ou le LSP est d’intérêt — ce qui est sensé être le cas dans nos exemples, sinon l’exemple n’est plus pertinent pour le LSP) par le type mère, le code doit rester valable — puisque c’est le type mère qui définit le contrat de départ. Or si tu peux remplacer un éventuel Derived o ; par Other o ;, tu ne peux pas remplacer Bar m_bar ; par Foo m_bar ; dans l’exemple ici.

C’était pour simplifier l’exemple. J’ai tout à fait le droit d’écrire :

class Other {
public:
  Other(){
    m_foo = &actual_foo ;
  }
protected:
  Foo* m_foo ;
  Foo actual_foo ;
};

class Derived {
public:
  Other(){
    m_foo = &in_fact_bar ;
  }
  void up_2(){
    in_fact_bar.mul(-2);
  }
protected:
  Bar in_fact_bar ;
};

Ce code ne présente pas de remplacement qui soit invalide. Avant m_foo référençait un Foo, maintenant il référence un Bar qui est censé être un sous-type. Sauf que de fait on peut faire un appel qui l’empêche d’avoir la propriété temporelle de son sur-type.

Concernant ton morceau de formalisation, le problème est amha que tu supposes que si l’on remplace un objet alors nécessairement le protocole qu’on lui applique restera le même. Et ça me semble une contrainte hyper forte. En particulier dans le morceau que j’ai mis en gras, c’est une contrainte très forte. Ça veut dire qu’un objet enfant ne peut soit jamais ajouter de méthodes, soit jamais passer par un contexte où l’on a une meilleure connaissance de son type.

Il n’y a pas a priori de raison de dire que l’on ne peut pas faire ce remplacement, sauf à dire que les méthodes appelable de l’objet ne comprennent pas mul (ce qui revient à interdire l’usage de toute méthode ajoutée), ou à interdire protected qui rend le LSP safe même sur une propriété temporelle de manière à peu près triviale je pense.

Je ne vois pas ce qui change dans ton exemple, je peux toujours pas remplacer Bar in_fact_bar ; par Foo in_fact_bar ; (je fais pas attention au ref/pointeur, c’est un detail technique pour cette discussion). C’est sur cette ligne qu’est le LSP pour moi.

Tu as raté la partie implémentation dans le formalisme que je montre. Il ne m’interdit pas d’écrire :

class Foo {
public:
  /*@
    requires this->val >= 0
    ensures this->val > \old(this->val) ;
  */
  virtual void incr();

  /*@
    ensures this->val < \old(this->val) ;
  */
  void decr();
};


class Bar : public Foo {
public:
  /*@
    ensures this->val == \old(this->val) * x ;
  */
  void mul(int x) ;

  void incr()
  { this->mul(-2); }
}

J’ajoute une fonction mul et je l’utilise. Par contre ça casse le LSP.

Avec des mots, une protocole c’est juste une suite de noms, de message, auquel l’objet répond. Par exemple la suite foo,bar,foo,foo,bar, tout ce que je dis c’est que pour considérer le LSP tu dois déjà avoir deux types tel que les objets de ces types répondent a ce protocole peu importe comment (c’est le sens de la note [1]). C’est ensuite le LSP qui vient rajouter la contrainte le comportement, en terme de pré et post condition, doit être le même.

Dis autrement, pour moi, le LSP n’intervient qu’a partir du moment ou:

void lsp_test(base& b) {
    //Suite d'instructions sans structure de contrôle
    //C'est la suite de message
}

base b;
derived d;

lsp_test(b);
lsp_test(d);

Est valide.

Or je n’ai pas l’impression que le cas considéré ici puisse être écrit de cette manière.

Edit: Pour le morceau que tu as mis en gras, on est bien d’accord que je considère cette substitution fille -> mère uniquement pour la discussion du LSP. Je ne considère pas ça comme nécessaire de manière générale. Je ne trouve pas ça si fort, la formulation du LSP — peu importe laquelle — est toujours de la forme:

Si xxx sur mere alors xxx sur fille

On parle donc d’un implication, et tout ce que je dis c’est que pour discuter de cette implication c’est mieux d’être dans le cas ou l’antécédent est vrai. Ça te semble vraiment fort comme condition ?

C’est pas ce que je fais non. J’ai bien remplacé une référence vers un objet d’un certain type par un objet qui est censé être d’un sous-type de ce type. À moins que l’ajout de mul casse le LSP, c’est une opération valide, j’ai le droit de changer cet objet.

Oui mais justement c’est la question de départ : est ce que cette contrainte en terme de pré/post est suffisante pour garantir que ça marche pour des propriétés temporelles. Et clairement, non puisque tu contraints les remplacements à ne s’effectuer que sur des traces qui ne changent pas lorsqu’il y a sous-typage. Ce qui, du fait que l’on ne remplace pas forcément qu’un objet à la fois dans un programme, est une condition forte : il faut non seulement vérifier le LSP localement mais aussi globalement à travers les traces générées par d’autres objets.

En haut, la trace de base est changée par la conjonction de deux remplacements. En gros : c’est Derived qui casse le LSP sur Other, en proposant un objet qui temporellement peut redevenir positif. Seulement, vu que ce comportement cassé à travers Bar qui prétend remplacer parfaitement Foo, qui est vraiment le fautif ?

Ok, je crois que je vois mieux où est le problème selon toi. Prenons le cas suivant (c’est pas exactement la même chose, mais j’y vois un lien) :

struct A {
  //require i >= 0
  //ensure i <= 0
  //ensure abs(i) == old(i) 
  virtual void bar() {
    i = -i;
  }
  //ensure i >= 0
  //ensure i == old(i*i)
  virtual void goo() {
    i = i*i;
  }
  //ensure abs(i) == old(i*i)
  virtual void foo() {
    this->goo();
  }
private:
  int i;
};

struct B : A {
  void foo() {
    this->goo()
    this->bar()
  }
};

Est-ce que dans cette situation le LSP est violé ?

(Je ne prétends pas avoir la réponse au problème posé, simplement que tous les éléments temporels sont plus subtils qu’il n’y paraissent à mon avis et que si on autorise le mot clé protected/public le respect des contraintes sur les pré et post-conditions me semble léger pour maintenir des propriétés temporelles. C’est d’ailleurs pour ça que je trouve qu’il est généralement une mauvaise pratique d’avoir des propriétés temporelles sur les objets pour les appels de fonctions membres, et encore plus quand on autorise la dérivation).

C’est effectivement aussi une violation, plus directe, mais également due à une propriété cachée (implicitement foo assure i positif, mais sa surcharge non). Et en fait, ce qui est intéressant une nouvelle fois c’est que le problème ne va apparaître que si le développeur a fait des suppositions supplémentaires sur le programme.

Ici on peut raisonnablement considérer que les contrats sont imprécis. Mais sur les propriétés temporelles, on ne peut pas spécifier si simplement ce qui rend ce genre d’imprécisions encore mieux planquées. Il y a une différence qui est assez importante entre cet exemple et le premier. On ne peut pas si facilement expliciter une propriété temporelle et il est encore plus difficile de la vérifier.