7.2 Correctness Flashcards
1
Q
What is the difference between partial and full correctness
A
Partial: All executions that terminate are correct
Full: All executions terminate and are correct
2
Q
How to prove partial correctness
A
- Assume derive state exists
- Determine post-condition to prove
- Prove post-condition using loop in-variant
3
Q
Why is this invariant not strong enough (to prove post-condition for euclid)
A
Does not reference initial values
