weakest precondition

[BlackSalad]

Hallo,

wir machn grad das wp-Kalkül, aber irgendwie verstehe ich garnicht was sich dahinter verbirgt.

Wikipedia hat mir leider auch ned so wirklich weiter geholfen. Ich weiß nur, dass es dazu da ist, festzustellen ob dein Programmcode korrekt ist. (zumindest hab ichs so verstanden).


Und ich glaube man muss schauen ob vor und nach der schleife, die bedingungen eingehalten sind.

Aber was soll da der Begriff "schwächste Vorbedingung" ?

Ich werd daraus nicht ganz schlau. :noe:

 

[Empire Phoenix]

Mal kurz bei wiki überflogen soweit wie ich das verstehe.

Du hast eine gütlige Nachbedingung.
Jetzt versuchst du rückwärts daraus die kleinste menge an Krams zu machen die zu diesem Ergebnis führt.(also die kleinste Menge an Bedinungen die eingehalten werden muss damit das ergebnis rauskommt)

 

[Empire Phoenix]

aka

code

i=i%2

Ergebnis = 0
-> Rückwärts code verfolgen
-> kleinste vorbedingung i = {x*2|x element N(mit0)}