Relation between Hoare Type Theory and pointers

My understanding is that in Hoare Type Theory every imperative statement has a type of the form {Pre}res:T{Post} where T is the type of the result of the computation and Pre and Post are propositions representing respectively the pre and postconditions of the statement and res is the result of type T which can appear in the postcondition.

Given the following program in pseudo-C:

int i=0;
int*p=&i;
*p=1
return i;

How can Hoare type theory represent the the fact that i must be 1?After all,it's not clear i is modified in the above snippet,and it can be hidden even from the programmer if we begin to add lambdas and partial application

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=&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.

StackExchange Computer Science Q#81971, answer score: 8