KeY EnsuresPost Task laden klappt nicht

[ToKaM]

Wenn ich für die Maze.java z.B. die Move Methode im Prover wähle und dann den EnsuresPost Task laden möchte reagiert KeY einfach nicht.
Es zeigt zwar an über die Java GUI, dass auf den Button geklickt wurde, es erscheint aber keine Fehlermeldung oder ein Open-Task in KeY.

Auch schließt der Modulare Dialog des Provers nicht.

Ich verwende KeY Version 1.6

Wenn ich via Ubuntu die verlinkte jnlp für "KeY for FGDI 3" Datei öffnen möchte wird diese mit Firefox geöffnet, hier fehlt wohl was (für Java Webstart).

Alle Einstellungen in KeY habe ich bereits überprüft.

Was mache ich falsch wie würdet Ihr weiter vorgehen?

[khaled]

Nachdem du die Methode auswählst mit EnsuresPost dann musst du auf play klicken, dann fängt KeY zu beweisen da musst dann auf continue klicken solange KeY unten sagt x remaining und nur dann wenn x = 0 ist dann sagt er dir ob er deine Nachbedingung bewiesen hat (durch ein Fenster mit der Anzahl der nodes und branches) wenn du das aber nicht siehst dann heißt das, dass er deine Nachbedingung nicht beweisen konnte.

Khaled

[Ankou]

Kann das Problem bestätigen. Wenn man die Konsole per javaws -viewer aktiviert stellt sich raus dass KeY eine NullPointerException wirft, ist wohl ein Bug(und nicht der einzige...). Bis zu dem Zeitpunkt wo man auf play klicken muss kommt KeY da gar nicht. Das Problem besteht auf meinem Rechner, auf zumindest einem Rechner im IGD und bei noch jemand anderem in meiner Arbeitsgruppe. Es funktioniert hingegen auf den Poolrechnern und wiederum bei jemand anderem in meiner Arbeitsgruppe. Java 6/7 scheint keine Rolle zu spielen, 32/64-bit auch nicht

[ToKaM]

Nach der Installation von libnetx-java lässt sich die JNLP Datei mit der verlinkten Key Version 1.65 unter Ubuntu starten.

Damit funktioniert das starten des Beweises.