Programming Notes – Programming Solutions Part 2

 

Theorem 1: given k£n, ("i|k£i£n:P[i] {r} R[i]) Þ (Çi|k£i£n:P[i]) {r} (Çi|k£i£n:R[i])

(Given k£n, prove LHS Þ RHS using induction)

Case n=k

("i|k£i£k:P[i] {r} R[i])

º(Arithmetic, one point rule)

      P[k] {r} R[k]

º(one point rule)

      (Çi|k£i£k:P[i]) {r} (Ç|k£i£k:R[i])

End of Proof Case n=k

 

Case n=m,m+1

(Given true for n=m, prove true for n=m+1)

("i|k£i£m+1:P[i] {r} R[i])

º(Split off term)

("i|k£i£m:P[i] {r} R[i]) Ù P[m+1] {r} R[m+1]

º(Given)

(Çi|k£i£m:P[i]) {r} (Çi|k£i£m:R[i]) Ù P[m+1] {r} R[m+1]

Þ(Program Solution Part 1 Theorem 7 for two Hoare Triples)

((Çi|k£i£m:P[i])ÇP[m+1]) {r} (Çi|k£i£m:R[i])ÇR[m+1])

º(Split off terms)

(Çi|k£i£m+1:P[i]) {r} (Çi|k£i£m+1:R[i])

End of Proof Case n=m,m+1

End of Proof

 

Theorem 2: ("i|k£i£n:P[i] {r} R[i]) Þ (Èi|k£i£n:P[i]) {r} (Èi|k£i£n:R[i])

(Prove LHS Þ RHS using induction)

Case n<k

("i|k£i£n:P[i] {r} R[i])

º(Arithmetic)

("i|false:P[i] {r} R[i])

º(empty range)

      true

º(Program Solution Theorem 16[R := Æ])

      Æ {r} Æ

º(Empty Range)

      (Èi|false:P[i]) {r} (È|false:R[i])

º(n<k, arithmetic)

      (Èi|k£i£n:P[i]) {r} (È|k£i£n:R[i])

End of Proof Case n=k

 

Case n=m,m+1

(Given true for n=m, prove true for n=m+1)

("i|k£i£m+1:P[i] {r} R[i])

º(Split off term)

("i|k£i£m:P[i] {r} R[i]) Ù P[m+1] {r} R[m+1]

º(Given)

(Èi|k£i£m:P[i]) {r} (Èi|k£i£m:R[i]) Ù P[m+1] {r} R[m+1]

Þ(Program Solution Part 1 Theorem 8 for two Hoare Triples)

((Èi|k£i£m:P[i])ÈP[m+1]) {r} (Èi|k£i£m:R[i])ÈR[m+1])

º(Split off terms)

(Èi|k£i£m+1:P[i]) {r} (Èi|k£i£m+1:R[i])

End of Proof Case n=m,m+1

End of Proof

 

Theorem 3: given k£n, ("i|k£i£n:P {r} R[i]) º P {r} (Çi|k£i£n:R[i])

(Given k£n, prove LHS º RHS using induction)

Case n=k

("i|k£i£k:P {r} R[i])

º(Arithmetic, one point rule)

      P {r} R[k]

º(one point rule)

      P {r} (Ç|k£i£k:R[i])

End of Proof Case n=k

 

Case n=m,m+1

(Given true for n=m, prove true for n=m+1)

("i|k£i£m+1:P {r} R[i])

º(Split off term)

("i|k£i£m:P {r} R[i]) Ù P {r} R[m+1]

º(Given)

P {r} (Çi|k£i£m:R[i]) Ù P {r} R[m+1]

º(Program Solution Part 1 Theorem 9 for two Hoare Triples)

P {r} (Çi|k£i£m:R[i])ÇR[m+1])

º(Split off terms)

P {r} (Çi|k£i£m+1:R[i])

End of Proof Case n=m,m+1

End of Proof

 

Theorem 4: ("i|k£i£n:P[i] {r} R) º (Èi|k£i£n:P[i]) {r} R

(Prove LHS Þ RHS using induction)

Case n<k

("i|k£i£n:P[i] {r} R)

º(n<k, arithmetic)

("i|false:P[i] {r} R)

º(empty range)

      true

º(Program Solution Theorem 16)

      Æ {r} R

º(Empty Range)

      (Èi|false:P[i]) {r} R

º(n<k, arithmetic)

      (Èi|k£i£n:P[i]) {r} R

End of Proof Case n=k

 

Case n=m,m+1

(Given true for n=m, prove true for n=m+1)

("i|k£i£m+1:P[i] {r} R)

º(Split off term)

("i|k£i£m:P[i] {r} R) Ù P[m+1] {r} R

º(Given)

(Èi|k£i£m:P[i]) {r} R Ù P[m+1] {r} R

º(Program Solution Part 1 Theorem 10 for two Hoare Triples)

((Èi|k£i£m:P[i])ÈP[m+1]) {r} R

º(Split off term)

(Èi|k£i£m+1:P[i]) {r} R

End of Proof Case n=m,m+1

End of Proof

 

 

 

 

References:

 

Dijkstra, Edsgar, 1976, A Discipline of Programming, Englewood Cliffs, NJ: Prentice-Hall

 

Fejer, Peter and Simovici, Dan A., 1991, Mathematical Foundations of Computer Science, New York, NY: Springer-Verlag

 

Gries, David, 1981, The Science of Programming, New York, NY: Springer-Verlag

 

Gries, David and Schneider, Fred B., 1993, A Logical Approach to Discrete Math, New York, NY: Springer-Verlag