KeY EnsuresPost Task laden klappt nicht

ToKaM
Windoof-User
Windoof-User
Beiträge: 33
Registriert: 17. Mär 2011 21:20
Kontaktdaten:

KeY EnsuresPost Task laden klappt nicht

Beitrag von 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?
Hier geht es zu meinem Android Blog.

khaled
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 102
Registriert: 28. Mai 2012 01:16

Re: KeY EnsuresPost Task laden klappt nicht

Beitrag von 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
Mausschubser
Mausschubser
Beiträge: 85
Registriert: 15. Mai 2011 18:23

Re: KeY EnsuresPost Task laden klappt nicht

Beitrag von 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
Windoof-User
Windoof-User
Beiträge: 33
Registriert: 17. Mär 2011 21:20
Kontaktdaten:

Re: KeY EnsuresPost Task laden klappt nicht

Beitrag von 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.
Hier geht es zu meinem Android Blog.

Antworten

Zurück zu „Archiv“