[정지민]

조교님 안녕하세요,

hw4-1에서 ASSIGNF의 assign to record field라는 설명이 정확히 어떤 의미인지 조금 헷갈려 질문드립니다.

주어진 pdf에서 RECASSIGN에 해당하는 것으로 보이는데

주어진 record를 확장하는 역할을 하는 것이 아니라

e1에 주어진 record로부터
location인 e1.x를 읽고
memory의 e1.x 주소에 e2로부터 나온 값 v를 할당
하는 것이 맞나요?

감사합니다.

[이재호]

안녕하세요,

말씀주신 표현이 명확하지 않아, K- 설명서에 적힌 RECASSIGN 규칙을 풀어서 설명드리도록 하겠습니다. (일단 RECASSIGN에 나온 규칙이 모호함이 없는 정확한 의미입니다.)

환경 σ와 메모리 M이 주어졌을 때 e1.x := e2를 계산한 결과는,
환경 σ와 메모리 M이 주어졌을 때 e1을 계산한 값이 r (변화된 메모리 M1),
다시 환경 σ와 메모리 M1이 주어졌을 때 e2을 계산한 값이 v (변화된 메모리 M2)으로 주어졌을 때,
값은 v이고 새로운 메모리는 [주소가 r(x)일 때는 v를, 나머지는 M2와 같은 메모리]입니다.

문서의 2절 Domains에서 보시듯 Record r은 변수 이름을 주소로 대응시키는 유한한 함수입니다.

Record는 C계열 언어에 있는 struct와 유사하다고 생각하시면 됩니다.
JS나 파이썬처럼 "확장" 가능한 object가 아닙니다.


감사합니다.

조교 드림


TA 이재호
e-mail: jhlee@ropas.snu.ac.kr