게시판 인덱스

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

숙제 3 안내사항 모음(뼈대코드와 파서가 수정되었습니다.)(0510 추가)

 
글 쓰기   답변 달기     게시판 인덱스 -> 4541.664A Program Analysis (Spring 2017)
이전 주제 보기 :: 다음 주제 보기  
글쓴이 메시지
이동권



가입: 2012년 9월 9일
올린 글: 191

올리기올려짐: 2017년5월5일 10:37    주제: 숙제 3 안내사항 모음(뼈대코드와 파서가 수정되었습니다.)(0510 추가) 인용과 함께 답변

숙제3에서 제대로 도는 프로그램만을 입력으로 받는다는 것은 아래의 뜻을 함축하고 있습니다.

+ 혹은 &&, || 등의 연산에서 타입에 맞지 않는 프로그램에 대해서는 고려할 필요가 없습니다.

예를들어 1 + true, true && 1 과 같은 경우는 연산을 굳이 정의할 필요가 없습니다.

단, 요약실행의미를 정의하고 구현하실 때에는 요약도메인 디자인에 따라 위와 유사한 상황을 잘 처리해야 할 경우가 있을 것입니다. (요약된 값이 정수와 논리값을 동시에 포함하고 있는 경우 등)

디자인과 구현에 참고하시기 바랍니다.

0506 추가:

과제 문서에서 Exp의 inductive한 정의 중 true 와 false가 빠져있습니다.
true, false에 대한 디자인 및 구현도 해주세요.


0506 추가:

문제 2번에서, 뼈대코드의 요약도메인 정의가 수정되었습니다.
정수 요약도메인이 powerset domain에서 상수인지 아닌지만을 확인하는 도메인으로 간단하게 바뀌었고, 주소를 요약하는 도메인에서 top이 사라졌습니다.

본래는 정수 요약을 좀더 정확하게 하기 위해서 powerset domain을 사용하려고 했으나, 문제의 스펙과 맞지 않는 부분도 있고, TOP_Z가 아닌 무한집합을 표현하기 애매해지는 문제가 있어 보다 간단한 도메인으로 바꾸었습니다.

그리고 프로그램 실행중 나타나는 변수의 개수는 유한하다는 가정을 추가하여, TOP_LOC도 없는것으로 바꾸었습니다.

혼돈을 드려 죄송합니다.


0506 추가

분석기 채점기준에 대한 문의를 주셔서 추가로 공지합니다. 코딩과제 채점은 분석기가 돌아간 이후(analyzer함수의 결과값) 최종 메모리상태를 출력하여,
1. 그것이 실제 실행결과를 안전하게 포섭하는지
2. 문제에서 요구한 스펙에 맞는 분석결과를 잘 내었는지
3. 혹 유한시간내에 끝나지 않는 경우는 없는지(와이드닝 미구현시)
4. 얼마나 정확한지(모든 값에 대해 무조건 top을 내놓는 경우는 위 세가지를 모두 만족하지만 제대로 된 점수를 받을 수 없습니다.)
제가 직접 보고 이 네가지 기준들에 따라 점수를 부여할 예정입니다.

또한 코딩이 아니라 디자인하는 과제에서, 도메인 디자인을 뼈대코드와 같게 하는 것을 권장드리기는 하지만(디자인한 그대로 구현하면 되므로) 필수는 아닙니다. 말이 되는 디자인이고, 안전함이 증명되었고, 분석하고자 하는 목표를 잘 분석한다고 판단되면 제대로 점수를 드릴 예정입니다.

0506 추가

값 도메인 관련해서 문의주신 분이 계셔서 추가공지합니다. C언어처럼 0이면 false고 1이면 true인 것으로 T,F를 해석하지 마시고, Value = Integer + Boolean 으로 생각하시고 정수와 논리값을 별개로 처리해주세요. 슬라이드 10-1을 기반으로 드린 숙제이기 때문에 숙제1처럼 true/false를 판별하시면 안됩니다. 뼈대코드 도메인을 보시면 보다 이해가 쉬울 것입니다.

마찬가지 맥락으로 문제 2의 경우는 Value = Interger + Boolean + Location이 될것입니다.


0507 추가

파서가 unary minus연산자를 인식하지 못하는 버그가 발견되어 수정본으로 업로드하였습니다.
아직 작업을 시작하지 않으신 분들은 새로운 뼈대코드 위에서 작업을 시작해주시면 되고,
이미 작업을 하고계신 분들은 parser.mly 파일만 새로운 파일로 업데이트해주시면 됩니다.


0507 추가

2번 연습문제 뼈대코드에서 수정한 파서를 테스트하다가 제공해드린 테스트케이스에 이상이 생겼는데, test0.k-에서 첫부분을 x := true; y := 1;로 고치시면 될것같습니다. 어차피 테스트케이스는 보통 이러한 경우를 가지고 테스트한다는 뜻이므로 적당히 조금씩 고치시면서 테스트해보시면 되겠습니다. 혼돈을 드려 죄송합니다.


0508 추가

assume함수의 뼈대코드를 제공해드린 부분에서, e가 NUM i 인 경우 bottom memory를 리턴하도록 구현해두었는데요. 올바른 프로그램만 들어온다는 가정하에 NUM i인 경우나 ADD, MINUS등의 경우는 구현할 필요가 없는 것이 맞지만, 이번 숙제에서는 편의상 bottom memory를 리턴하도록 구현해주시면 되겠습니다. 사실 올바르지 않은 프로그램에 대한 테스트는 하지 않을 예정이므로 bottom memory가 아니라 다른 값을 리턴하셔도 상관은 없습니다.


0510 추가

assume을 디자인/구현할때 not/and/or로 묶인 exp들에 대해 어떻게 구현해야 할지 어려워하시는 분들이 있어 힌트를 드리고자 합니다. assume과 assumeNot을 서로 재귀하도록(mutual recursive) 디자인/구현하면 위와 같은 경우들을 매우 편리하게 구현할 수 있습니다.


-조교 드림.
위로
사용자 정보 보기 비밀 메시지 보내기
이전 글 표시:   
글 쓰기   답변 달기     게시판 인덱스 -> 4541.664A Program Analysis (Spring 2017) 시간대: GMT + 9 시간(한국)
페이지 11

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


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