Programmverifikation, wie sieht die Vorbedingung aus?

[RainerH88]

Guten Abend ,

kennt sich hier jemand mit Programmverifikationen aus?

Ich habe hier folgenden code:

x := a; 

y := b;  

p := 0;

while x > 0 do

begin

  p := p + y;

  x := x - 1;

end;

die Inv müsste lauten: x*y+p=a*b und die Post-Bedingung: p=a*b

wie aber muss die Pre-Bedingung aussehen? a und b >0 und p=0?

Gruß Rainer