Search code examples
verifiable-c

PLCC book. page 23. Is it a misprint, and should sigma be replaced by sigma prime?


In Programming Logics for Certified Compilers book, on page #23, in the expression :

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

It seems to me, that, since σ represents the whole list v, and σ' represents tail, the last expression should be: listrep σ' (t, 0). Is that correct, and it's just a misprint in the book?


Solution

  • Yes, you are right; it should be sigma-prime.