verifikation hoare-kalkül < Algor.+Datenstr. < Theoretische Inform. < Hochschule < Informatik < Vorhilfe
|
| Status: |
(Frage) überfällig  | | Datum: | 13:47 So 16.11.2008 | | Autor: | gossyk |
| Aufgabe | | http://img19.myimg.de/temp56162.jpg |
hallo, zu diesem algorithmus soll ich mittels des hoare kalküls verifizieren.
ich komme nicht weiter bei der schleifenvariante.
diese ist vermutlich sehr einfahc, da das array einfach nur umgekehrt angeordnet wird, aber da ich auf soetwas das erste mal stoße kann ich damit überhaupt nicht umgehen!
mein hauptproblem ist die schleifenvariante selbst (bin nicht sicher ob meine ideen überhaupt korrekt sind) und dass in der while schleife ein term steht, wo ein array b einem array a zugewiesen wird.
wie soll ich damit umgehen im bezug auf die variante.
ich hatte ein paar ideen zur schleifenvariante wie zb a[k-1] = b[n-k] (was ja eigentlich a[k]=b[n-k-1] entspricht..*hust*) oder das, was ganz unten auf dem zettel steht (das was bewiesen werden soll) dabei mit j=k-1...
habe dazu eine tabelle aufgestellt, und bin der meinung dass diese ideen in der ganzen tabelle gültig sind...
weiter hilft mir das jetzt aber kaum.
ich habe beides (und einige andere) ausprobiert, aber bin damit nicht sonderlich weitergekommen, da an der stelle
a[k] = b[n-1-k] im algorithmus doch sowieso die schleifenvariante hierdurch ersetzt wird?!
geht es ab diesem punkt immer gleich weiter, egal welche schleifenvariante ich vorher gewählt habe?
also im endeffekt bin cih mit keiner der schelifenvarianten die ich als richtig erachtet hab sonderlich weit gekommen mit der verifikation...
ich würde sehr dankbar sein wenn mir das jemand klarer machen könnte...
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 14:39 Di 18.11.2008 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
