I've recently become incredibly confused about the notion of "strengthening/weakening a precondition/postcondition". I think my confusion lies in my interpretation of the words "precondition" and "postcondition". Here is why I'm confused:

In the rules of Hoare Logic, one can "strengthen the precondition and/or weaken the postcondition", as per this question.

However, according to LSP, one can only "weaken the precondition and/or strengthen the postcondition", as per this question.

I attempted to work through it myself, and I convinced myself that you can "strengthen the precondition and weaken the postcondition", but I did so using LSP (sorta). To do so, I considered a function Y f(C c) that takes an object of type C and returns an object of type Y. Now, C inherits from B, and D inherits from C, and Y inherits from X and Z inherits from Y (Z : Y : X and D : C : B).

To strengthen the pre/post-condition would be, in my mind, to replace C with D and Y with Z. My rationale is that a subtype is "stricter" than its parent because it satisfies every condition its parent satisfies plus some extra conditions. To weaken the pre/post-condition would be to replace C with B and Y with X. The parent type is "weaker" than the subtype because it has to satisfy "less" conditions than the subtype.

Now, it appears that we can "strengthen" the precondition without failure, because by LSP if f works with an object of type C then it must work if we replace C with a subtype of C (i.e. D). This makes sense to me because D satisfies everything C satisfies, but more, whereas B may not satisfy everything C satisfies, and thus may not satisfy every condition f needs to function properly. Hence, I have "shown" that we can strengthen the precondition, and cannot weaken it.

As for the postcondition, it seems to me that we can only strengthen it. If f were to return an object of type X, this would be totally fine, since an object of type Y is also an object of type X. However, f cannot necessarily return a Z. My counterexample to demonstrate this is the inheritance tree Rect : Shape and Circle : Shape. If f returns a Shape, that Shape may not necessarily be a Rect, it may be a Circle, or it may be neither. Hence we can't strengthen the postcondition.

In summary, I demonstrated to myself that:

• You can strengthen the precondition and weaken the postcondition.

Obviously this doesn't comply with the second question above. Apparently I violated LSP. Is it in my definition of "strengthen" and "weaken", or my idea of "precondition" and "postcondition", or my analogy? Where is the fault in my understanding? Are the ideas of Hoare Logic and LSP simply incompatible?

I've recently become incredibly confused about the notion of "strengthening/weakening a precondition/postcondition". I think my confusion lies in my interpretation of the words "precondition" and "postcondition". Here is why I'm confused:

In the rules of Hoare Logic, one can "strengthen the precondition and/or weaken the postcondition", as per this question.

However, according to LSP, one can only "weaken the precondition and/or strengthen the postcondition", as per this question.

I attempted to work through it myself, and I convinced myself that you can "strengthen the precondition and weaken the postcondition", but I did so using LSP (sorta). To do so, I considered a function Y f(C c) that takes an object of type C and returns an object of type Y. Now, C inherits from B, and D inherits from C, and Y inherits from X and Z inherits from Y (Z : Y : X and D : C : B).

To strengthen the pre/post-condition would be, in my mind, to replace C with D and Y with Z. My rationale is that a subtype is "stricter" than its parent because it satisfies every condition its parent satisfies plus some extra conditions. To weaken the pre/post-condition would be to replace C with B and Y with X. The parent type is "weaker" than the subtype because it has to satisfy "less" conditions than the subtype.

Now, it appears that we can "strengthen" the precondition without failure, because by LSP if f works with an object of type C then it must work if we replace C with a subtype of C (i.e. D). This makes sense to me because D satisfies everything C satisfies, but more, whereas B may not satisfy everything C satisfies, and thus may not satisfy every condition f needs to function properly. Hence, I have "shown" that we can strengthen the precondition, and cannot weaken it.

As for the postcondition, it seems to me that we can only strengthen it. If f were to return an object of type X, this would be totally fine, since an object of type Y is also an object of type X. However, f cannot necessarily return a Z. My counterexample to demonstrate this is the inheritance tree Rect : Shape and Circle : Shape. If f returns a Shape, that Shape may not necessarily be a Rect, it may be a Circle, or it may be neither. Hence we can't strengthen the postcondition.

In summary, I demonstrated to myself that:

• You can strengthen the precondition and weaken the postcondition.

Obviously this doesn't comply with the second question above. Apparently I violated LSP. Is it in my definition of "strengthen" and "weaken", or my idea of "precondition" and "postcondition", or my analogy? Where is the fault in my understanding? Are the ideas of Hoare Logic and LSP simply incompatible?

I've recently become incredibly confused about the notion of "strengthening/weakening a precondition/postcondition". I think my confusion lies in my interpretation of the words "precondition" and "postcondition". Here is why I'm confused:

In the rules of Hoare Logic, one can "strengthen the precondition and/or weaken the postcondition", as per this question.

However, according to LSP, one can only "weaken the precondition and/or strengthen the postcondition", as per this question.

I attempted to work through it myself, and I convinced myself that you can "strengthen the precondition and weaken the postcondition", but I did so using LSP (sorta). To do so, I considered a function Y f(C c) that takes an object of type C and returns an object of type Y. Now, C inherits from B, and D inherits from C, and Y inherits from X and Z inherits from Y (Z : Y : X and D : C : B).

To strengthen the pre/post-condition would be, in my mind, to replace C with D and Y with Z. My rationale is that a subtype is "stricter" than its parent because it satisfies every condition its parent satisfies plus some extra conditions. To weaken the pre/post-condition would be to replace C with B and Y with X. The parent type is "weaker" than the subtype because it has to satisfy "less" conditions than the subtype.

Now, it appears that we can "strengthen" the precondition without failure, because by LSP if f works with an object of type C then it must work if we replace C with a subtype of C (i.e. D). This makes sense to me because D satisfies everything C satisfies, but more, whereas B may not satisfy everything C satisfies, and thus may not satisfy every condition f needs to function properly. Hence, I have "shown" that we can strengthen the precondition, and cannot weaken it.

As for the postcondition, it seems to me that we can only strengthen it. If f were to return an object of type X, this would be totally fine, since an object of type Y is also an object of type X. However, f cannot necessarily return a Z. My counterexample to demonstrate this is the inheritance tree Rect : Shape and Circle : Shape. If f returns a Shape, that Shape may not necessarily be a Rect, it may be a Circle, or it may be neither. Hence we can't strengthen the postcondition.

In summary, I demonstrated to myself that:

• You can strengthen the precondition and weaken the postcondition.

Obviously this doesn't comply with the second question above. Apparently I violated LSP. Is it in my definition of "strengthen" and "weaken", or my idea of "precondition" and "postcondition", or my analogy? Where is the fault in my understanding? Are the ideas of Hoare Logic and LSP simply incompatible?

I've recently become incredibly confused about the notion of "strengthening/weakening a precondition/postcondition". I think my confusion lies in my interpretation of the words "precondition" and "postcondition". Here is why I'm confused:

In the rules of Hoare Logic, one can "strengthen the precondition and/or weaken the postcondition", as per this question.

However, according to LSP, one can only "weaken the precondition and/or strengthen the postcondition", as per this question.

I attempted to work through it myself, and I convinced myself that you can "strengthen the precondition and weaken the postcondition", but I did so using LSP (sorta). To do so, I considered a function Y f(C c) that takes an object of type C and returns an object of type Y. Now, C inherits from B, and D inherits from C, and Y inherits from X and Z inherits from Y (Z : Y : X and D : C : B).

To strengthen the pre/post-condition would be, in my mind, to replace C with D and Y with Z. My rationale is that a subtype is "stricter" than its parent because it satisfies every condition its parent satisfies plus some extra conditions. To weaken the pre/post-condition would be to replace C with B and Y with X. The parent type is "weaker" than the subtype because it has to satisfy "less" conditions than the subtype.

Now, it appears that we can "strengthen" the precondition without failure, because by LSP if f works with an object of type C then it must work if we replace C with a subtype of C (i.e. D). This makes sense to me because D satisfies everything C satisfies, but more, whereas B may not satisfy everything C satisfies, and thus may not satisfy every condition f needs to function properly. Hence, I have "shown" that we can strengthen the precondition, and cannot weaken it.

As for the postcondition, it seems to me that we can only strengthen it. If f were to return an object of type X, this would be totally fine, since an object of type Y is also an object of type X. However, f cannot necessarily return a Z. My counterexample to demonstrate this is the inheritance tree Rect : Shape and Circle : Shape. If f returns a Shape, that Shape may not necessarily be a Rect, it may be a Circle, or it may be neither. Hence we can't strengthen the postcondition.

In summary, I demonstrated to myself that:

• You can strengthen the precondition and weaken the postcondition.

Obviously this doesn't comply with the second question above. Apparently I violated LSP. Is it in my definition of "strengthen" and "weaken", or my idea of "precondition" and "postcondition", or my analogy? Where is the fault in my understanding? Are the ideas of Hoare Logic and LSP simply incompatible?