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.
mmi1991 hat geschrieben:Ü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.