Formale Systeme

Vorlesung im Wintersemester 2015/2016

Prof. Dr. Bernhard Beckert (BB)
Dr. Thorsten Bormer (TB), Dr. Vladimir Klebanov (VK), Dr. Mattias Ulbrich (MU)

Praxisaufgabe 2: Spezifikation und Verifikation

In dieser Praxisaufgabe sollen Sie eine Javamethode mit einem Methodenvertrag in der Java Modeling Language (JML) spezifizieren und mit Hilfe des Theorembeweisers KeY verifizieren.

(Anklicken für ein größeres Bild)

Ziel in dieser Praxisaufgabe ist es, das Verhalten der Methode in der folgenden Klassenspezifikation formal zu spezifizieren und mittels KeY zu beweisen, dass die Implementierung Ihre Spezifikation einhält:

        class
        SubsetArray {
          
            /*@ public normal_behaviour
            @ assignable \nothing;
            @ ensures ...;
            @*/
          
          public
          static
          boolean
          isSubset(int[] a, int[] b) {
            
              /*@ loop_invariant ...;
              @ assignable \nothing;
              @ decreases ...;
              @*/
            
            for (int i=0; i < a.length; i++) {
              boolean found = false;
              
                /*@ loop_invariant ...;
                @ assignable \nothing;
                @ decreases ...;
                @*/
              
              for (int j=0; j < b.length; j++) {
                if (a[i] == b[j]) found = true;
              }
              if (!found) return false;
            }
            return true;
          }
        }
      

Für die vollständige Lösung dieser Praxisaufgabe erhalten Sie 10 Übungspunkte für die Abschlussklausur (bitte beachten Sie die Erlauterung zu Übungspunkten auf der Webseite zur Vorlesung).

Auch für unvollständige Teillösungen werden Punkte anteilig vergeben.

Material

• Bitte verwenden Sie in jedem Fall die KeY-Version von dieser Seite und nicht die Versionen auf den Seiten des Tools.
• Webstart für die aktuelle KeY Version. Bitte beachten Sie, dass sich diese Version von der Version auf der Webseite unterscheiden kann.
• Java Archive (KeY.jar) für die aktuelle KeY-Version zum Herunterladen. Bitte beachten Sie, dass sich diese Version von der Version auf der Webseite unterscheiden kann.
  Ausführen: java -jar KeY.jar
• Das Aufgabenblatt zur Praxisaufgabe
• Einführung in Beweisen prädikatenlogischer Aussagen mit KeY
• SubsetArray.java - Java-Datei mit der Implementierung zur Aufgabe

Abgabe

Die Abgabe der Praxisaufgabe erfolgt über unsere Seiten im ILIAS-Portal.