게시판 인덱스

 
 FAQFAQ   검색검색   멤버리스트멤버리스트   사용자 그룹사용자 그룹   사용자 등록하기사용자 등록하기 
 개인 정보개인 정보   비공개 메시지를 확인하려면 로그인하십시오비공개 메시지를 확인하려면 로그인하십시오   로그인로그인 

마찬가지로 CalF에 관련된 질문

 
이 게시판은 잠겼으므로 글을 올리거나, 답변을 하거나 수정을 할 수 없습니다   이 주제는 잠겼으므로 답변을 하거나 수정을 할 수 없습니다     게시판 인덱스 -> 4541.664A Program Analysis (Spring 2009)
이전 주제 보기 :: 다음 주제 보기  
글쓴이 메시지
임경영



가입: 2009년 4월 5일
올린 글: 27

올리기올려짐: 2009년5월21일 18:47    주제: 마찬가지로 CalF에 관련된 질문 인용과 함께 답변

calF가 무슨 '역할'을 하는 함수의 정의가 애매한듯한데..


정리를 해보면,
calF가 K언어로 구현된 어떤 cmd에 대해서
cmd와 state를 받아서 state를 반환해주는 함수를 받으면,

요약된 형태의
cmd와 state를 받아서 state를 반환해주는 함수로 바꾸어주는 역할을 하는 함수인가봅니다.

(cmd->state->state)에서
(cmd->state->state)로 가는 함수이다보니..
그 역할이 애매한것 같습니다.

요약의미 방정식을 결정한다는 것이니..
일단은 domain이 변경된 값으로 cmd를 처리하는 어떤 함수로 바뀌는 것 같네요..


일단

제 질문은..
1. calF에 대한 정의나, state나 value의 정의를
자신 임의대로 생각해서 풀어도 될지!
(저는 일단 state나 value의 값을 interval domain으로 생각해서 바로 구현하려고합니다)

2. READ에 대한 처리는 어떻게 하면 좋을지(무난하게 TOP이 맞을 것 같네요)
입니다.
위로
사용자 정보 보기 비밀 메시지 보내기
공순호



가입: 2005년 9월 29일
올린 글: 363
위치: 302동 312-2호

올리기올려짐: 2009년5월22일 7:06    주제: 인용과 함께 답변

인용:

calF가 무슨 '역할'을 하는 함수의 정의가 애매한듯한데..


calF에 대해서는 강의 노트와 숙제 문서에 명백하게 정의되어 있습니다.


강의 노트 10-2.pdf 에서 설명하고 있는 것과 같이

프로그램의 의미 를 정의할 때,

이것을 상위 함수 가 만들어내는 의미 방정식의 해로 정의할 수 있습니다.


숙제에서는 프로그램의 요약 의미 를 찾기 위해서

이것의 상위의 함수

를 정의하고, 이를 이용해서 주어진 프로그램 C에 대한 분석을 하는 것 입니다.


인용:

1. calF에 대한 정의나, state나 value의 정의를
자신 임의대로 생각해서 풀어도 될지!
(저는 일단 state나 value의 값을 interval domain으로 생각해서 바로 구현하려고합니다)


state와 value의 정의는 숙제 문서에 나와 있습니다.

value에 대해서만 이야기해보면, K 프로그램에서 value는 정수일 수도, 주소값일 수도 있습니다.

value를 interval domain으로 바로 요약하면, 정수값은 요약할 수 있지만, 주소값은 어떻게 되는걸까요?

state와 value의 정의는 숙제 문서에 나와 있습니다. 단지 뼈대 코드에 명시적으로 타입을 정의하지 않았을 뿐입니다.

인용:

2. READ에 대한 처리는 어떻게 하면 좋을지(무난하게 TOP이 맞을 것 같네요)
입니다.


저는 무난하게 -5부터 5 사이의 모든 정수로 하는 것이 좋다고 생각합니다만,

교수님께 여쭤보고 다시 답글 달도록 하겠습니다.

-----

web에서 하는 이어서 type setting이 예쁘지 않습니다. 이해하시는데는 무리 없으시리라 생각합니다. 죄송합니다.
_________________
- soon@ropas
위로
사용자 정보 보기 비밀 메시지 보내기 글 올린이의 웹사이트 방문
공순호



가입: 2005년 9월 29일
올린 글: 363
위치: 302동 312-2호

올리기올려짐: 2009년5월22일 14:36    주제: 인용과 함께 답변

read 의 요약 의미는 [-inf, +inf] 로 합니다.
_________________
- soon@ropas
위로
사용자 정보 보기 비밀 메시지 보내기 글 올린이의 웹사이트 방문
임경영



가입: 2009년 4월 5일
올린 글: 27

올리기올려짐: 2009년5월22일 18:52    주제: 인용과 함께 답변

read는 -inf부터 +int 이군요

^^ 감사합니다

일단 state와 value가 정의가 나와 있다하셨는데..
state가
인용:
기계상태는 각 메모리 주소가 가질 수 있는 값들

이라는 건가요
아니면
인용:
요약된 정수 공간은 수업시간에 다룬 인터벌 도메인

인가요
인용:
요약된 주소공간은 프로그램에 나타나는 변수들의 집합

이라는 건가요?;;

state와 value에 대한 것은 문제에서 정의되지 않은것 같은데요?

state에 대한것은
인용:
K언어의 요약 의미 방정식을 결정해주는 의미함수
F:(pgm->State->State)->(Pgm->State->State)

에서만 추정이 가능한데,

따라서
요지는 state, value, calF에 대한 정의가 모호하게 되지 않을까하는 걱정에서 하는 질문입니다.

interval의 예는,
도메인의 변경에 대한 과정을 생략해도 되냐는 질문의 예였는데,
즉, x:=1 과 같은 진술의 경우 x에 [1,1]을 대입하는 과 같은 방식으로 구현해도 무방하느냐라는 질문이었습니다.

그럼 이렇게 질문은 하면 더 좋을것 같네요..

프로그램 뼈대에서의 value는 요약된 공간에서의 정의와 같도록 구현하면 좋을까요?
아니면 요약되기 전과 요약된 상태 모두를 포함하게 구현 해야하나요?
그에 따라서 state도 구현방식을 달리해야하나요?

가 질문입니다.. ^^;;
위로
사용자 정보 보기 비밀 메시지 보내기
공순호



가입: 2005년 9월 29일
올린 글: 363
위치: 302동 312-2호

올리기올려짐: 2009년5월23일 9:40    주제: 인용과 함께 답변

* 기계 상태는 각 메모리 주소가 가질 수 있는 '값'입니다.

문제는 어떤 '값'을 사용할 것인가입니다.


* 값(Value)에 대해서 생각해보면,

요약된 값에는 요약된 정수공간과 요약된 주소공간이 모두 포함되어야 합니다.


* 요약된 정수공간과 요약된 주소공간이 문제에 정의되어 있습니다.

이를 이용해서 구성하는 요약된 값공간은 자명합니다.

또한 이를 이용하는 요약 기계 상태 역시 자명하다고 생각합니다.


인용:

프로그램 뼈대에서의 value는 요약된 공간에서의 정의와 같도록 구현하면 좋을까요?
아니면 요약되기 전과 요약된 상태 모두를 포함하게 구현 해야하나요?
그에 따라서 state도 구현방식을 달리해야하나요?


value는 요약된 공간에서의 값입니다.
state 역시 요약된 기계 상태가 되도록 정의하면 됩니다.
_________________
- soon@ropas
위로
사용자 정보 보기 비밀 메시지 보내기 글 올린이의 웹사이트 방문
이전 글 표시:   
이 게시판은 잠겼으므로 글을 올리거나, 답변을 하거나 수정을 할 수 없습니다   이 주제는 잠겼으므로 답변을 하거나 수정을 할 수 없습니다     게시판 인덱스 -> 4541.664A Program Analysis (Spring 2009) 시간대: GMT + 9 시간(한국)
페이지 11

 
건너뛰기:  
새로운 주제를 올릴 수 없습니다
답글을 올릴 수 없습니다
주제를 수정할 수 없습니다
올린 글을 삭제할 수 없습니다
투표를 할 수 없습니다


Powered by phpBB 2.0.21-7 (Debian) © 2001, 2005 phpBB Group
Translated by kss & drssay