Relazione tra teoria del tipo di hoare e puntatori

Question

La mia comprensione è che nella teoria del tipo di hoare ogni affermazione imperativa ha un tipo di forma {Pre}res:T{Post} dove T è il tipo di risultato del calcolo e Pre e Post sono proposizioni che rappresentano rispettivamente le pre e le postcondizioni della dichiarazione e res è il risultato del tipo T che può apparire in postcondizionamento.

Dato il seguente programma in Pseudo-C:

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

In che modo la teoria del tipo di hoare può rappresentare il fatto che i Deve essere 1? Dopo tutto, non è chiaro i viene modificato nello snippet sopra e può essere nascosto anche dal programmatore se iniziamo ad aggiungere lambdas e applicazione parziale