1043 ;;Quote: exhaustive test of binary search by all successes, all failures, and boundary conditions

1043 ;;Quote: exhaustive test of binary search for n=0 to 10 catches empty array, one, two, three, powers of two, one away from power of two

1043 ;;Quote: correct code by using sound principles during design, verification by analysis, and exhaustive testing of small cases

1043 ;;Quote: a loop is correct if the loop invariant is established by initialization and preserved each iteration; also prove final result and termination

1043 ;;Quote: verify a subroutine by its pre and postconditions; if preconditions satisfied then postconditions will be after execution

1043 ;;Quote: informal verification usually consists of executing a test case by hand

1043 ;;Quote: verification gives programmers a language for understanding the program as it is written; important explanations become assertions