Added preliminary definitions for read, write, deallocate, and allocate. Also, all the previous hoare triples have now been proven with the new assertion type.