Die Implementierung wurde angepasst. Bestimmte Teile wurden entfernt oder
überarbeitet. Die Struktur und Funktion des Codes sollte jedoch ungefähr
erhaltengeblieben sein.

Bitte dokumentieren Sie Ihre Vorgehensweise. Sie müssen in der Lage sein, die
Beweise im Praktikum vorzuführen und ggf. Ihre Änderungen am
Programm/Spezifikation im einzelnen zu erläutern.


Im folgenden betrachten wir die Klasse Kartenleser.


1. Die Klasseninvariante ist syntaktisch nicht korrekt. Beheben Sie den Fehler,
die Absicht der Invariante soll erhaltenbleiben.

2. Zeigen Sie, daß die Methode prüfePIN() die Invariante erhählt. Sollte dies
nicht mglich sein, ergänzen/korrigieren Sie die Implementierung und/oder die
Spezifikation auf eine SINNVOLLE Weise.

3. Die Nachbedingung der Methode prüfePIN() ist nicht korrekt. Beheben Sie den
Fehler, die Absicht der Nachbedingung soll erhaltenbleiben.

4. Zeigen Sie, daß die Methode prüfePIN() ihre Spezifikation erfüllt. Sollte
dies nicht möglich sein, ergänzen/korrigieren Sie die Implementierung und/oder
die Spezifikation auf eine SINNVOLLE Weise.



Allgemeine Hinweise



   1) Sie koennen alle Heuristiken aktivieren (außer
      simplify_instanceof_static). Als maximale Anzahl der Schritte empfiehlt
      sich ca. 1000.

   2) Stellen Sie bitte sicher, daß unter dem KeYExtensions-Menu in der
      Werkzeugleiste von Together bei den OCL RefinementSettings die
      Erweiterung 'use null' aktiviert ist. Stellen Sie weiterhin sicher, daß
      im KeYExtensions-Menu "UML Model Souce" auf "TogetherCC data structures"
      eingestellt ist.

   3) Bei Verwendung des @pre-Konstrukts tauchen in der Sequenz Formeln mit 
      Allquantoren auf, die den Wert im Vorzustand mit Hilfe einer Gleichung
      "speichern". Damit kann dieser Wert später verwendet werden.

      Tip: Oft ist es geschickter, den o.g. Allquantor /am Anfang/ manuell
      zu instantiieren.