OOPM1617 Übungswoche 08 (09.01-15.01.17)

Zielsetzung für die Übung

  • Besprechung der Hausaufgabe aus letzter Woche
    • Spezifikation abstrakter Datentypen
    • Implementation abstrakten Datentypen
  • Beweis von Eigenschaften
    • Anwendung von Gleichungen
      • Beispiele aus Vorlesungsfolien
    • Erschöpfende Fallunterscheidung
      • Beispiele aus Vorlesungsfolien
    • Vollständige Induktion
      • [add-assoc] siehe Vorlesungsfolien S. 31/32
      • add(zero,y) = add(y,zero) siehe unten und S. 33
    • Strukturelle Induktion
      • [app-assoc] siehe unten
zu zeigen: add(zero,y) = add(y,zero)
Vollständige Induktion über y

IA: y = zero
add(zero,zero) = add(zero,zero) q.e.d.

IS: y = k
    IV: add(zero,k) = add(k,zero)
    IB: add(zero,succ(k)) = add(succ(k),zero)

add(zero,succ(k))       ->[1]
= succ(k)               <-[1]
= succ(add(zero,k))     ->IV
= succ(add(k,zero))     <-[2]
= add(succ(k),zero)     q.e.d.

[1] add(zero,n) = n 
[2] add(succ(n),m) = succ(add(n,m))
zu zeigen append(l1,append(l2,l3)) = append(append(l1,l2),l3)        [app-assoc] 

Strukturelle Induktion über l1

IA: l1 = nil
append(nil,append(l2,l3))        ->[1]
= append(l2,l3)                  <-[1]
= append(append(nil,l2),l3)      q.e.d.

IS: l1 = k
    IV: append(k,append(l2,l3)) = append(append(k,l2),l3)
    IB: append(cons(t,k),append(l2,l3)) = append(append(cons(t,k),l2),l3)

append(cons(t,k),append(l2,l3))         ->[2]
= cons(t, append(k, append(l2,l3)))     ->IV
= cons(t, append(append(k,l2),l3))      <-[2]
= append(cons(t, append(k,l2)), l3)     <-[2]
= append(append(cons(t, k), l2), l3)    q.e.d.

[1] append(nil, l) = l
[2] append(cons(e, l1), l2) = cons(e, append(l1, l2))

Zielsetzung für das Programmierpraktikum

  • Wrapper Klassen
  • equals, compareTo…
  • Generics