The specifications for deref-exp and setref-exp are not quite correct

[dwayne]

See page 109.

I'll just explain the issue with the deref-exp specification since the issue is the same for the setref-exp specification.

Take (value-of exp ρ σ_0) = (l, σ_1). l is an ExpVal. This means to get the reference we have to do (expval->ref l). The specification as written doesn't do that.

Suggestion 1:

      (value-of exp ρ σ_0) = ((ref-val l), σ_1)
---------------------------------------------------------------
(value-of (deref-exp exp) ρ σ_0) = (σ_1(l), σ_1)

Suggestion 2:

                  (value-of exp ρ σ_0) = (val, σ_1)
------------------------------------------------------------------------------------
(value-of (deref-exp exp) ρ σ_0) = (σ_1((expval->ref val)), σ_1)

[mwand]

You are right, of course. Your suggestion 1 is probably what we should have written. Thanks. --Mitch

…

On Fri, Jul 29, 2022 at 7:17 AM Dwayne Crooks ***@***.***> wrote: I'll just explain the issue with the deref-exp specification since the issue is the same for the setref-exp specification. Take (value-of exp ρ σ_0) = (l, σ_1). l is an ExpVal. This means to get the reference we have to do (expval->ref l). The specification as written doesn't do that. Suggestion 1: (value-of exp ρ σ_0) = ((ref-val l), σ_1) --------------------------------------------------------------- (value-of (deref-exp exp) ρ σ_0) = (σ_1(l), σ_1) Suggestion 2: (value-of exp ρ σ_0) = (val, σ_1) ------------------------------------------------------------------------------------ (value-of (deref-exp exp) ρ σ_0) = (σ_1((expval->ref val)), σ_1) — Reply to this email directly, view it on GitHub <#30>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAR3CMHKEG7LRXC566OQJALVWO4WBANCNFSM55ANIEZA> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>