프로그래밍 언어(PL 분야) (3) 썸네일형 리스트형 safety 검증을 초고속으로 하는 방법이 뭐가 있을까.. 프로그램 전체에 걸친 invariant를 사용해서 safety를 검증하는건 기존에 많다. 이런 방식은 여러 safety 속성에 대해 강화하기도, 약화하기도 하며 검증을 계속 하는 구조로 되어있다. 이는 경우에 따라, 하나의 코드에 대해 10일 이상이상 검증이 종료되지 않는다는 것을 의미한다. 그래서 검증기들은 보통 timeout을 걸게되고, 이는 10분 내로만 사용한다. 그러면 검증기는 10분동안 invariant를 바꿔가며 safety를 검증한다. 만약 코드의 크기가 매우 커서, Integer Overflow를 검증해야하나 안전 속성인 NoOverFlow를 invariant로 사용하지 못한다면 검증기는 Unproven을 낸다. 하지만, 정말 안전한 경우일 수도 있지 않나. NoOverFlow의 비용이.. Incorrectness Logic? Correctness 아냐? 본 게시글은 소프트웨어공학 및 검증에 관심있는 분들을 대상으로 합니다. 1900년대에 Correctness를 증명하는 Hoare Logic이 나왔었죠. 올바름(오류 없음)을 증명하는 논리로, 우리의 선조인 Hoare 아저씨가 제시한 패러다임입니다. 이는 지금 발전하여, 학계에서 활발히 사용되고 있습니다. 산업계에서도 정적분석기를 만드는 곳에서는 사용하고 있습니다. 전력 회사에서 IoT 장비를 만들다 온 저로서는 익숙하지 않은 개념이었습니다. 하지만, Facebook 등의 큰 기업에서는 활발히 연구되고 있는 분야입니다. 대표적으로는 O'Hearn 아저씨가 있습니다. Incorrectness Logic(POPL 2020)을 처음 보았을 땐, 무슨 뜬구름 잡는 이야기인가 했습니다.Correctness Logi.. correctness, 알고리즘.. computer science가 왜 필요해? 개발만 잘하면 되지 이렇게 생각했던 때도 있었으나, 돌이켜보니, 특출난 개발자들은 모두 이 소양이 출중한 사람이었다. 아는만큼 보인다고 하던가. 일례로 임베디드 환경에선 메모리 계산이 수반되서야 한다. 모 차장님이 말하셨던 말이 떠오른다. 이대리가 짜는건 돌아가지, 데스크탑에서. 근데 이건 임베디드 시스템이야. 이렇게 하면 큰일 나. 몇십만개 장비 다 돌아다니면서 수정할거야? 지금 생각해도 맞는 말이다. correctness는 어떤가? 개발자라면 memory leak을 보면 스트레스 받을거라 생각한다. valgrind 정도 사용해서 분석을 시도할 수 있었다.(내 주변 한정) 다 짜여진 코드를 분석하는건 사막 위에서 바늘 찾기라고 본다 짤 때부터 correctness에 대한 기본소양이 장착되어 있어야 문제.. 이전 1 다음