Reasoning Example

N := 10;

Sum := 10;

while N > 1 do

begin

N := N - 1;

Sum := Sum + N

end

{pre: N = 10}

{inv: N >= 1 & Sum = sigma(X, N ? X ?10)}

{post: Sum = sigma(x, 1 to 10)}

Previous slide

Next slide

Back to first slide

View graphic version