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 Geldautomat, Methode pruefePIN().


1. Erfüllt die Methode pruefePIN() die angegebene Spezifikation? Falls nicht,
ergänzen/korrigieren Sie die Implementierung und/oder die Spezifikation auf
eine SINNVOLLE Weise.


2. Ergänzen Sie nun die Nachbedingung, indem Sie die vorhandene mit dem Ausdruck 

		((result=true) implies (fehlVersuche=0))
		
konjunktiv verbinden. Erfüllt die Methode diese Spezifikation? Falls nicht,
ergänzen/korrigieren Sie die Implementierung und/oder die Spezifikation auf
eine SINNVOLLE Weise.


3. Erhält die Methode die Klasseninvariante? Warum oder warum nicht?



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.