指针逻辑的出发点是：所有不同的访问路径都代表不同的对象，除非能证明它们代表同一个对象。因此指针逻辑需要收集有效指针相等信息，以便知道哪些不同访问路径代表同一个对象。这是指针逻辑不用引入新连接词的原因。 这比较符合习惯：在通常的逻辑中，不相同的名字总代表不同的对象，没有别名的概念。Hoare逻辑就是基于不同名字代表不同对象。