Program Verification
Given a precondition, a postcondition and some code verify that the code when executed in a state satisfying the given precondition achieves the given postcondition.
{Q} : {Array b has values}
i,s:= 1,b[0]
Do i <> N
i,s := i +1, s+b[i];
Od
{R}: {s = ? k: 0<=k:b[k])}
Previous slide
Next slide
Back to first slide
View graphic version