Correctness of Design
Prove that the initial states correspond to one another
Prove that for each operation in the design, that it is correct and applicable (this corresponds to proving the correctness criterion for the retrieve function).
To prove that the initial states correspond in the abstract and concrete worlds we prove that InitClass2’ ? Class1Class2’ ? InitClass1’ is a theorem of FOL.
Class1Class2 is like the retrieve function we talked about earlier.