KeY: Invarianten und Instanzvariablen

[deadlock]

Hallo,

mir gelingt es mit KeY nicht, die einfachsten Invarianten zu beweisen, sofern diese etwas über Instanzvariablen aussagen. Beispiel:

Code: Alles auswählen

public class Test {

	public static int a;
	public int b;

	/*@ public static invariant a >= 0; */
	public static void test_static() {
		a = 1;
	}

	/*@ public instance invariant b >= 0; */
	public void test() {
		b = 1;
	}
}

test_static() kann ich beweisen, test() jedoch nicht. In den offenen Goals steht dann sowas wie "self = m_0_0 FALSE", in der zu beweisenden Formel steht unter anderem self.<created> = TRUE in der Prämisse und "self = null" in der Konklusion. Wenn ich aber so etwas wie "self != null" oder "\created(self)" voraussetze, hilft mir das auch nicht. Muss man irgendwas spezielles bei Instanzvariablen beachten? Konnte in den Folien nichts dazu finden.

Danke im Voraus.

[mmi1991]

Hallo.

Es müsste funktionieren, wenn du gleichzeitig eine Invariante hast, die besagt, dass zwei versch. Instanzen von Test ein anderes b referenzieren müssen (mit ==). Wobei ich mir unsicher bin, ob das geht, solange b public ist…
Ich würde b lieber privat machen - dann sollte es auf jeden Fall gehen.
Dasselbe Problem hatten wir auch bei einem Beweis von Lab 4 mit Maze.
KeY meint quasi: Hey, du könntest theoretisch händisch zwei Instanzen von Test erzeugen und deren Referenzen durcheinanderbringen - zumindest war das unser Problem bei Maze, da ein Array zumindest ja ein Objekt ist.

EDIT:
Über deinem Code kann ich aber problemlos ohne Änderung preserveInv von test() beweisen?
Benutzt du die KeY-Version von der FGdI3-Seite?

[deadlock]

Danke für die Antwort.
Ja, mir ist auch aufgefallen, dass man dann beweisen muss, dass für alle Test-Instanzen gilt: Test t != 0 & \created(t) ==> t.b >= 0.

Über deinem Code kann ich aber problemlos ohne Änderung preserveInv von test() beweisen?
Benutzt du die KeY-Version von der FGdI3-Seite?

Komisch, ich habe es auch mit der verlinkten Version probiert. Ich bin dabei so vorgegangen: Test.java geladen, Methode test() und preservesInv() ausgewählt, unter assumed Invariants habe ich keine ausgewählt, unter ensuredInvariants nur self.b >= 0. Nach dem automatischen Beweisen entsteht dann ein offenes Goal. Vor dem Beweisen wurden die Einstellungen gesetzt, die auf den submission guidelines angegeben waren. Sollte ja auch eigentlich nicht möglich sein zu beweisen, dass nach self.b := 1 für alle Test-Instanzen t gilt: t.b >= 0.

[Nathan Wasser]

Nimmt man die Invariante an (für alle Instanzen), so kann man beweisen, dass die Invariante auch danach erhalten bleibt (für alle Instanzen). Nimmt man die Invariante nicht an, so muss man zeigen, dass jede Instanz, die vorher die Invariante nicht eingehalten hat, nach der Methode die Invariante einhält. Da die Methode nur ihre eigene Variable ändert bedeutet das, dass nur diese eine Instanz vorher die Invariante verletzen durfte. Der Beweis bleibt also in so einem Zustand hängen:

t_0_0.b <= -1,
t_0_0.<created> = TRUE,
inReachableState,
self.<created> = TRUE
==>
t_0_0 = self,
self = null,
t_0_0 = null

Das bedeutet soviel wie: Wenn es eine Instanz t_0_0 gibt, in dem b nicht >= 0 ist, so ist dieses t_0_0 genau unsere Instanz self.

(Dieses "ODER self = null ODER t_0_0 = null" auf der rechten Seite ist eine logische Umformulierung, die für uns Menschen nicht sonderlich verständlich ist. Am besten denkt man sich die Sachen negiert auf der linken Seite, also: Wenn t_0_0 != null UND self != null, DANN ist t_0_0 = self.)