Lab3 Problem 3.1

Hoang
Erstie
Erstie
Beiträge: 11
Registriert: 6. Nov 2013 15:02

Lab3 Problem 3.1

Beitrag von Hoang »

Hi,

Beim Problem 3 kommen wir (gar) nicht zurecht, und zwar:

1. Was sollen wir beim 3.1 tun? Den ganzen Beweis manuell zu machen? Ist das doch impossible, weil sogar die einfache Codes in der Übung kosten Hundert Schritte..
Oder sollen wir einpaar (erste) Schritte manuell "klicken" und lass dann den Rest für KeY?


2. Wie wird ein Java code in DL durchs KeY System "übersetzt"? Hier ist die Sequenz die wir am Anfang kriegen: (die markierte Positionen kapieren wir nicht, und das Ganze bleibt uns auch sehr unklar...)

Bild


3. Wie funktioniert "Methods inlining" eingentlich? Die Vorlesung liefert uns kaum etwas, Die Musterlösung für Übung 6 enthält leider nur die editierte Java codes. Wir haben daher keine Ahnung wie man solche Treatment im KeY manipuliert..?


4. Selbe Frage für "Use Operation Contract".
(Diese Antwort von Nathan viewtopic.php?f=182&t=29916 reicht uns nicht :( )


5. Hier ist unser Setting fürs 3.1, ist das schon korrekt?
Bild


6. Wir versuchen das Problem automatisch zu beweisen, es geht aber nicht. Warum? Wir können Probleme, die nicht automatisch durch KeY bewiesen werden können, mit den Händen beweisen?

Vielen Dank im voraus,
mfG
Hoang

Minker
Windoof-User
Windoof-User
Beiträge: 25
Registriert: 28. Sep 2009 16:11

Re: Lab3 Problem 3.1

Beitrag von Minker »

Hallo,

ihr sollt den Beweis so weit wie möglich automatisch führen. Da ihr aber "Method Treatment" (richtigerweise, steht ja so in der Aufgabenstellung) auf "None" gesetzt habt, wird er bei Methodenaufrufen anhalten. Dort müsst ihr manuell den Methodenaufruf behandeln und dann den automatischen Beweiser weitermachen lassen. Wenn ihr eine Stelle erreicht, an der der automatische Beweis nicht weiter kommt, die aber kein Methodenaufruf ist (sollte nur ein einziges Mal vorkommen), führt ihr einen anderen Interaktionsschritt aus und lasst dann den automatischen Beweis weiter laufen. Dazu beachtet den Tipp in der Aufgabenstellung dazu, welche Regeln sinnvoll sein könnten. Die Stelle, an der ihr die Regel anwendet, könnt ihr zum Beispiel suchen, indem ihr euch überlegt, welche Aussage der Kontrakt macht, den ihr beweisen sollt, welche Aussagen die benutzten Kontrakte machen, und wie das zusammenhängt. Es kann auch hilfreich sein, ungeschlossene Beweisunterbäume (mit dem Scherensymbol in der oberen Leiste) abzuschneiden, um zu sehen, wie das ursprüngliche Goal aussah, bevor KeY es erfolglos bearbeitet hat.

Zum Thema wie funktioniert "Method Inlining" und "Use Operation Contract" finde ich Nathans Antwort sehr eindeutig. Hier nochmal in anderen Worten:
Wenn ein Methodenaufruf erreicht wird, habt ihr zwei Möglichkeiten:
- ihr nutzt Method Inlining wie im Bild dargestellt. Dabei wird der Code in die Modalität hinein kopiert (statt des Aufrufs).
- ihr benutzt (falls vorhanden) einen Vertrag der Methode (die Verträge stehen als JML-Spezifikation in der Java-Datei), der euch (wenn ihr die requires-Bedingungen garantieren könnt), garantiert, dass die ensures-Garantien eingehalten werden. Deshalb bekommt ihr bei der Benutzung zwei Subgoals: eins, in dem ihr zeigen müsst, dass im Prestate (also vor dem Aufruf) die requires-Bedingungen erfüllt sind, und eins, in dem ihr zeigen müsst, dass ihr im Poststate (also nach dem Aufruf) unter Annahme der ensures-Garantien euer Goal beweisen könnt. Das ist vergleichbar der Anwendung eines Lemmas in mathematischen Beweisen.
Wenn ihr nicht nur eine einzelne Übungsaufgabe habt, sondern einen vollständigen Beweis für einen Kontrakt führen möchtet, müsst ihr natürlich alle benutzten Kontrakte auch beweisen (Wird für das Lab NICHT verlangt!). Trotzdem ist der Design-By-Contract-Ansatz sinnvoll, denn der Beweis wird modularer und die Goals dadurch übersichtlicher.

Welche der Methoden (Inlining oder Vertrag) Sinn macht, hängt davon ab, wie sehr ein Inlining des Codes das Goal verkomplizieren würde, wie sinnvoll für das Goal die zur Auswahl stehenden Kontrakte sind (man sollte den passendsten auswählen), etc. Hier beim Lab sollt ihr nicht selbstständig neue Kontrakte schreiben, sondern nur aus den vorhandenen auswählen.

Minker
Windoof-User
Windoof-User
Beiträge: 25
Registriert: 28. Sep 2009 16:11

Re: Lab3 Problem 3.1

Beitrag von Minker »

Zum Verständnis des generierten Goals:
- self ist die KeY-Repräsentation von this.
- self.<inv> sind die Klasseninvarianten (die in JML in der Java-Datei z.B. in der Form "public invariant" stehen).
- javaUnaryMinusInt ist die Übersetzung des unären Minusoperators. Für andere arithmetische Operatoren sieht die Übersetzung ähnlich aus, z.B. "javaAddInt" für +.
- "m(args)@package.Class" steht für eine Methode "m" mit den Parametern "args" in der Klasse "Class" im Package "package". In eurem Fall ist das Methode "performBinarySearch" aus der Klasse "BinarySearch".

Antworten

Zurück zu „Archiv“