verifiable-c - PLCC 书。第 23 页。它是不是印刷错误，应该用 sigma prime 代替 sigma 吗？

Question

在 Programming Logics for Certified Compilers 一书第 23 页的表达式中：

(v ≠ 0 ∧ ∃σ' ∃h∃t. σ = h · σ' ∧ v.head->h ∗ v.next->t ∗ listrep σ (t, 0))

在我看来，既然 σ 代表整个列表 v，而 σ' 代表尾部，那么最后一个表达式应该是：listrep σ' (t, 0)。对吗，只是书上的错别字吗？

Answer 1

是的你是对的; 它应该是 sigma-prime。