black-box and white box

black-box testing
-can work with code that cannot be modified
-does not need to analyze or study code
-code can be in any format(managed, binary, obfuscated)

White-box testing
-efficient test suite
-potentially better coverage

HttpPost localHttpPost = new HttpPost(...);
(new DefaultHttpClient()).execute(localHttpPost;

Automated testing is hard to do
probably impossible for entire system

A pre-condition is a predicate
A post-condition is a predicate

class Stack{
	T[] array;
	int size;

	Pre: s.size() > 0
	T pop() { return array[--size]; }
	Post: s'.size() == s.size() -1

	int size() { return size; }
}

int foo(int[] A, int[] B){
	int r = 0;
	for (int i = 0; i < A.length; i++){
		r += A[i] * B[i];
	}
	return r;
}