Princeton University Computer Science Dept.

Computer Science 496 Automated Theorem Proving Andrew W. Appel

Spring 2001

As discussed in class, modify the prover so that can prove verification conditions about types, such as vc2 generated from the query

%query 1 1 vcgen precond2 prog2 postcond2 VC.

Show other examples of type-based VC's that your prover can prove, and show some examples that your prover can't solve.

Also consider a program such as the following:

 Precondition: true
 r2 := 100
 m[r2] := 5
 m[r2+1] := 7
 Postcondition:  r2 has type record2(char,char).