Added safe predicate and modified the definition of the hoare triple. Proofs of while, read, and allocate still remain.