Lab3 BonusA

himbaer
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 28. Apr 2010 19:29
Kontaktdaten:

Lab3 BonusA

Beitrag von himbaer » 14. Feb 2014 16:05

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???
meine Testsignatur :!:

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Lab3 BonusA

Beitrag von Nathan Wasser » 14. Feb 2014 17:09

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
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 28. Apr 2010 19:29
Kontaktdaten:

Re: Lab3 BonusA

Beitrag von himbaer » 14. Feb 2014 17:37

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?
meine Testsignatur :!:

Benutzeravatar
mmi1991
Computerversteher
Computerversteher
Beiträge: 349
Registriert: 20. Okt 2011 18:46
Wohnort: Hattersheim

Re: Lab3 BonusA

Beitrag von mmi1991 » 14. Feb 2014 18:11

himbaer hat geschrieben: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.
Ophasentutor SoSe 2014, WiSe 2015/16
Alle Angaben wie immer ohne Gewähr

himbaer
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 28. Apr 2010 19:29
Kontaktdaten:

Re: Lab3 BonusA

Beitrag von himbaer » 14. Feb 2014 18:14

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.
meine Testsignatur :!:

rindphi
Mausschubser
Mausschubser
Beiträge: 55
Registriert: 3. Sep 2009 20:52
Kontaktdaten:

Re: Lab3 BonusA

Beitrag von rindphi » 14. Feb 2014 21:23

himbaer hat geschrieben: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
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 28. Apr 2010 19:29
Kontaktdaten:

Re: Lab3 BonusA

Beitrag von himbaer » 15. Feb 2014 18:14

Gibts es trotzdem eine Möglichkeit in JML zu potenzieren?
meine Testsignatur :!:

himbaer
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 28. Apr 2010 19:29
Kontaktdaten:

Re: Lab3 BonusA

Beitrag von himbaer » 16. Feb 2014 13:37

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?!
meine Testsignatur :!:

Boddlnagg
Mausschubser
Mausschubser
Beiträge: 54
Registriert: 10. Dez 2012 12:07

Re: Lab3 BonusA

Beitrag von Boddlnagg » 16. Feb 2014 15:10

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

himbaer
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 28. Apr 2010 19:29
Kontaktdaten:

Re: Lab3 BonusA

Beitrag von himbaer » 16. Feb 2014 16:50

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. :roll:
meine Testsignatur :!:

livingst0n
Neuling
Neuling
Beiträge: 10
Registriert: 14. Okt 2011 10:17

Re: Lab3 BonusA

Beitrag von livingst0n » 16. Feb 2014 17:31

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
variant.png (58.39 KiB) 1312 mal betrachtet
Gruss,
Chris

himbaer
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 28. Apr 2010 19:29
Kontaktdaten:

Re: Lab3 BonusA

Beitrag von himbaer » 16. Feb 2014 18:18

Ahhhh..... PERFEKT.
DANKE. Mit diesem Teil der Folien habe ich es nun endlich hinbekommen.
meine Testsignatur :!:

Antworten

Zurück zu „Archiv“