Relation between Hoare Type Theory and pointers
A pointer to a variable creates an alias. When the alias is modified, the corresponding variable is modified as well. Therefore, the rule for an assignment in Hoare's logic is not just update the value, but update the value for all associated aliases. Let's apply it to the example:

{True}        int i=0;  {i = 0}
{i = 0}       int*p=&amp;i; {i = 0; [*p, i]}  /* *p and i are now aliases */
                                          /* The postcondition can be written as: */
                        {[*p, i] = 0}     /* In particular, *p = 0 */
{[*p, i] = 0} *p=1;     {[*p, i] = 1}     /* In particular, i = 1 */
{[*p, i] = 1} return i; {i = 1}


The general rules to reason about programs with pointers are given by Separation logic. The information whether two expressions reference the same memory location is obtained by pointer analysis and alias analysis.