Lab3 BonusA

[himbaer]

Ich wollte mal fragen, ob es überhaupt möglich ist, in der decreasing Behauptung eine Aussage mittels des (\sum Operators zu machen.

Meine Idee war nämlich gewesen, dass es immer weniger false Werte in line geben wird. Dies habe ich mit dem (\sum... ) Operator ausgesagt. Leider bekomme ich von Key folgende Fehlermeldung:

Code: Alles auswählen

Building a term failed. Normally there is an arity mismatch or one of the subterms' sorts is not compatible (e.g. like the '2' in "true & 2")
The top level operator was bsum{[false,false,true]}(Sort: int); its expected arg sorts were:
1.) sort: int, sort hash: 26003033
2.) sort: int, sort hash: 26003033
3.) sort: int, sort hash: 26003033

The subterms were:
1.) Z(0(#))(sort: int, sort hash: 26003033)
2.) length(boolean[]::select(heap,self,Bonus::$line))(sort: int, sort hash: 26003033)
3.) equals(boolean::select(heap,boolean[]::select(heap,self,Bonus::$line),arr(c)),TRUE)(sort: Formula, sort hash: 30188878)

Daher meine Frage:
Ist es überhaupt möglich den (\sum...) Operator in dem decreasing Teil zu benutzen???

[Nathan Wasser]

Ja, es ist möglich. Vermutlich aber nicht so, wie Du es probierst. Kann es sein, dass Du versuchst boolean Werte aufzuaddieren? Eventuell wird auch durch fehlende Klammerung anders geklammert als vielleicht vermutet.

Deine Grundaussage ist aber falsch: Es werden in jedem Durchlauf nicht weniger false Werte. Als Gegenbeispiel sei als Eingabe ein Array, welches am Anfang mindestens ein true Wert hat. In dem Schritt wo dieses auf true gesetzt wird ändert sich nicht die Anzahl der false Werte.

[himbaer]

Erstmal vielen Dank für die Antwort. Ich habe meine Aussage nun mit (\num_of...) umgesetzt. Das war eigentlich das was ich haben wollte. Leider kann ich damit Bonus A noch nicht beweisen

Muss der decreasing Term also wirklich in jeder Iteration kleiner werden? So wie ich meinen Tutor am Mittwoch verstanden habe, dachte ich nämlich, dass diese "Funktion" sich einfach nur wie eine monoton fallende Funktion verhalten muss. Nach Ihrer Aussage muss die decreasing "Funktion" jedoch STRENG monoton fallend sein?!

***EDIT: Ist es irgendwie möglich zu potenzieren?

[mmi1991]

Muss der decreasing Term also wirklich in jeder Iteration kleiner werden? So wie ich meinen Tutor am Mittwoch verstanden habe, dachte ich nämlich, dass diese "Funktion" sich einfach nur wie eine monoton fallende Funktion verhalten muss. Nach Ihrer Aussage muss die decreasing "Funktion" jedoch STRENG monoton fallend sein?!

Nicht-offizielle Antwort:
Meines Verständnisses nach sorgt der decreasing Term dafür, die Variante der Funktion zu beweisen; also dass das Teil überhaupt terminiert. Man kann für manche Probleme ja einen Algorithmus erfinden, der, sofern er terminiert, immer das richtige Ergebnis liefert. Wenn er aber nicht immer terminiert, ist er nicht korrekt.
Wäre der decreasing-Term nur monoton fallend, könnte man ja einfach die Konstante 1 hernehmen. Das würde aber nicht beweisen, dass der Loop terminiert.
Es muss AFAIK strikt kleiner werden, also wirklich streng monoton, damit sichergestellt ist, dass er terminiert. Denn wenn er in jeder Iteration strikt kleiner wird, kann es ja irgendwann nicht mehr kleiner werden => terminiert.

[himbaer]

Danke. Weißt du vll ob es in JML möglich ist zu potenzieren? Ich habe nun noch einen decreasing Term gefunden. Dieser benötigt allerdings alternierende Vorzeichen und dafür fällt mir eben nur die Potenzierung ein.

Viele Dank schonmal für deine/eure Antworten.

[rindphi]

So wie ich meinen Tutor am Mittwoch verstanden habe, dachte ich nämlich, dass diese "Funktion" sich einfach nur wie eine monoton fallende Funktion verhalten muss. Nach Ihrer Aussage muss die decreasing "Funktion" jedoch STRENG monoton fallend sein?!

Der decreasing-Term muss natürlich streng monoton fallen, ansonsten würde er uns nicht weiterhelfen, da er zeigen muss, dass die Schleife "wohlfundiert" ist (es also keine unendlichen Ketten gibt). Dazu sollte sich zusätzlich aus dem Term in Kombination mit der Invarianten ergeben, dass er nicht unendlich lange fallen kann.

[himbaer]

Gibts es trotzdem eine Möglichkeit in JML zu potenzieren?

[himbaer]

Ich brauchte das Potenzieren um wechselnde Vorzeichen zu produzieren. Das habe ich nun aber folgendermaßen, ohne Potenzieren hinbekommen:

(1 - (2 *((i+1)%2))) * (line.length - i);

Ich denke meine "Funktion" ist streng monoton fallend. Und außerdem kann sie nicht unendlich fallen, da -1 * Vectorlänge immer der kleinstmögliche Wert ist.
Leider konnte ich damit das Problem immernoch nicht beweisen. Kann mir jemand vielleicht erklären, wieso das jetzt immernoch nicht beweisbar ist und mir eventuell einen Denkanstoß für die Lösung des Problems geben. Momentan weiß ich nämlich sonst echt nicht weiter und anscheinden denke ich ja in die falsche Richtung?!

[Boddlnagg]

Tipp: In Java (und JML) gibt es noch einen ternären Operator.

[himbaer]

Sorry aber das hat mir irgendwie noch gar nicht geholfen.
Meine Formel sieht jetzt zwar etwas lesbarer aus, aber beweisen kann ich damit trotzdem noch nichts.
Ich frage mich allerdings immernoch wieso?
Mein Formel sieht nun so aus:

Code: Alles auswählen

@ decreasing (i%2==1)? line.length-i:-(line.length-i);

Für ein Array mit der Länge 5 würde ich also pro Iteration folgende Ausgabe erhalten:
4
2
0
-1
-3
-5

Das ist doch eine streng monoton fallende Folge von Zahlen. Außerdem wird die "Funktion" nie unter -line.length fallen.
Mir fällt mittlerweile auch kein anderer Ansatz für einen "Hebel" ein.

[livingst0n]

Hi,

es reicht nicht, dass die Folge streng monoton fallend ist. Hier ein Auszug aus Folie 21 der Vorlesung zu Schleifen Invarianten. Ich denke das wird dir weiterhelfen.

variant.png (58.39 KiB) 1461 mal betrachtet

Gruss,
Chris

[himbaer]

Ahhhh..... PERFEKT.
DANKE. Mit diesem Teil der Folien habe ich es nun endlich hinbekommen.