[김덕환]

토론의 결과에 조교의 의견을 첨가하여 K- 의미를 정리해봤습니다. 몇 번 점검을 했습니다만, 혹시라도 오타나 어색한 부분이 발견되면 지적해주시기 바랍니다.

See http://ropas.snu.ac.kr/~ta/4190.310/05/hw2/k-.pdf
_________________
TheyAreAsSmartAsYouAre

[정민재]

NOT 이 없네요..

[정민재]

FOR 에서 n1<=n2 인경우 FOR문의 BODY 인 E3 를 실행하고 LOOP 를 돌아야 하는것 아닌가요?

[김덕환]

버그를 패치한 의미 정의 v0.2를 업데이트하였습니다. 달라진 점은 다음과 같습니다.

• NOT에 대한 정의를 추가하였습니다. (정민재, 이기석)
  
• FOR (E1, E2, E3)의 몸체인 E3가 실행되지 않는 버그를 수정하였습니다. (정민재)
  

버그를 알려주신 분들께 감사드립니다.
_________________
TheyAreAsSmartAsYouAre

[김남중]

EQUAL부분을 보면, n1=n2와 b1=b2의 두가지가 같아 보이는데 두번 나와 있는 것은,
n1=n2의 경우 정수가 같은 것을 말하는 것이고,
b1=b2는 불린 값의 비교를 말하는 것인가요?

그리고 원래 LESS(F,T)면 참을 반환하는게 일반적인가요?
한번도 불린값으로 비교를 해본적이 없어서요.

마지막으로, SEQ는 마지막으로 실행된 E의 결과값이 반환되는 거죠?
그것이 불린이든, 정수이든 마지막에 실행된 값이 반환되나요?

[김남중]

제가 이해한바로는 FOR(x,E1,E2,E3)는 다음의 순서로 수행될 것 같습니다.
1. M의 메모리에서 E1을 실행해 n1을 얻고 메모리를 M1으로 변경
2. M1의 메모리에서 E2를 실행해 n2를 얻고 메모리를 M2로 변경
3. n1과 n2의 값을 비교하여 n1>n2면 종료, n1<=n2면 다음을 수행
4. M2 메모리에 n1을 변수 x의 주소에 기록하여 얻은 메모리에서 E3를 수행하여 값 v를 얻고, 메모리는 M3로 변경
5. 앞 loop의 n1값보다 1큰 값을 가지고 FOR(x,n1+1,E2,E3)를 수행

그렇다면, 변수 x에 n1의 값을 기록하여 메모리 상태가 바뀌는 것은 항상 E3를 수행하기 전에만 일어나나요?
저는 E1이 수행되어 n1의 값이 구해졌을 때, 변경된 M1이 이미 n1의 값을 반영하고 있다고 생각했는데,
M2[n1/sigma(x)]라고 나와 있길래 헷갈립니다.

M2[n1/sigma(x)]의 의미를 M2메모리 상태에서 변수 x의 주소에 값 n1을 기록한 메모리 상태라고 해석하는 것이 맞습니까?

[김덕환]

[김덕환]

[임연섭]

식들을 잘못 이해하고 있는건지는 모르겠지만

k-에서

x:=1

이라는 프로그램을 실행하면 바인딩 안되었다고 에러가 나야 하나요?

x:=1;
write x
하면 write x에서 선언되지 않은 변수를 사용했다는 에러가 나야 하는거

아닌가요?

x:=1 이 x를 바인딩하고 1을 메모리에 저장하는게 아닌가 해서 질문드립니다.

바인딩 되어 있다면 바인딩 되어 있는 주소에 1을 저장하구요.

정의가 그렇게 되어 있는건가요.. 아닌거 같아서 긴가민가.. ^^;

[임연섭]

티피에 그대로 나와있네요.

위에꺼 지울라고 했더니.. 손님은 안되나보네요.. ㅜ.ㅜ

그럼 의미가..

제가 이해한게 틀린건가요..

수업 듣고도 이해못하는 중생을 구제해주십사.. ^^;

[김덕환]