I'm confused on the semantic application of design by contract to
inheritance stating an A' can be used everywhere an A is used. (A'
inherits from A). I thought that
 
K => P, {P} S {Q}, Q => W
--------------------------
{K} S {W}
 
where => means stronger than.
I took the design by contract representation of that formula to mean that
{K} S {W} can be used anywhere {P} S {Q} can be used b/c K is stronger
than P and W is weaker than Q. So, {K} S {W} relates the subclass, and
{P} S {Q}
relates to the super class. But in class, you mention that the
precondition in the subclass has to be weaker than the super class, and
the postcondition in the subclass is stronger than the post condition in
the super class. Can you relate your lecture to this formula somehow?

Consider

K => P, {P}S{Q}, Q=>W
---------------------
{K} S {W}
 
This rule tells you how to get a new valid triple for program
S, {K}S{W}, from one that you know, {P}S{Q}, also for program
S.
 
In design by contract, we use the above rule to answer a different question.
Here, the idea is that you have a program, say S0;S1 where S1 is
a method call defined in class C with specification {P1}S1{P2}.
Given that specification for S1, assume you can show {P0} S0 {P1} S1 {P2}
and thus {P0} S0;S1 {P2} and that this program meets your requirements.
Now, suppose that you define a new class C' extends C and you
override method S1--we'll call the new method S1' just to
distinguish them in the discussion. The type system will
allow you to replace the C object with a C' object, and when you
invoke S1, you are really invoking S1'. The question then becomes
what specification does S1' need to satisfy so that you can immediately
conclude {P0} S0 ; S1' {P2}?
 
Suppose you know {P1'} S1' {P2'} where P1 => P1' and P2' => P2. In
other words, you have taken the specification of S1 and weakened the
precondition and strengthened the postcondition.
 
You know {P0} S0 {P1}, and since P1 => P1', from the inference rule, you
can conclude {P0} S0 {P1'}. Thus, you get {P0}S0{P1'}S1'{P2'}, or
{P0}S0;S1'{P2'}. You want a postcondition of P2, not P2', but since
P2' => P2, you can use the inference rule again to conclude {P0}S0;S1'{P2}.
 
This gives what we want--you can replace S1 with S1' in any context 
provided the precondition has been weakened (or stays the same, of 
course) and the postcondition strengthened, and the modified program 
will still satisfy its original specification.