循環不變Hoare邏輯

Question

我有一個程序，我應該找到一個循環不變量，然後提供一個證明。

 {x>=0 && y>=0} // precondition 
res:=0; 
i:=0; 
while (i<y) do 
res:=res+x; 
i:=i+1; 
od 
     {res:=x*y} //postcondition 

唯一合乎邏輯的循環不變對我來說是res<=x*y，這是後置條件簡單，但我不認爲它最好的一個同去。也許還有其他建議？

Answer 1

這項工作？

{x>=0 && y>=0} // precondition 
res:=0; 
i:=0; 
while (i<y) do 
    {res=x*i} // invariant 
    res:=res+x; 
    i:=i+1; 
    {res=x*i} // invariant 
end 
{res=x*y} //postcondition 

通過這些條件，你應該能夠同時顯示，該方案是完全正確（即，如果循環結束，答案是正確的），它終止。儘管我認爲你需要y是一個整數的前提條件。