6 posts
클린룸 검증은 검증 조건을 생성하고 해소하는 것을 요구한다. 여기서 LLM이 주석과 VC 생성을 자동화하여 실제 어려운 증명에 집중할 수 있게 하는 방법을 소개한다.
클린룸 소프트웨어 공학은 코드를 컴파일하기 전에 그 정당성을 증명할 것을 요구한다. 그것은 고귀하게 들리지만, 열 개의 정수를 정렬하는 함수를 위해 루프 불변식을 세 시간 동안 작성하다 본다면 상황이 달라진다. 병목 지점은 증명 자체가 아니다. 상용구이다. 검증 조건을 생성하고,…
Cleanroom software engineering 은 defect rate 를 100배 낮추지만, 완전 도입에는 별도의 test team 과 formal proof 가 필요하다. 여기서는 overhead 없이 그 대부분의 benefit 을 얻을 수 있는 pragmatic subset 을 소개한다.
Cleanroom software engineering 은 1,000줄당 0.1개의 defect 를 달성한다. 업계 평균은 10에서 50이다. 문제는 완전한 Cleanroom 을 위해서는 팀을 author 와 verifier 로 분할하고, 모든 module 앞에 formal…
IBM의 Cleanroom engineering은 업계 평균보다 100배 나은 defect rate를 달성한 뒤 사라졌다. 사라진 이유는 그것이 작동했는지와는 아무런 관련이 없었다.
IBM의 Cleanroom software engineering process는 천 줄당 0.1개의 defect를 달성했다. 당시 업계 평균은 10에서 50 사이였다. 이 process는 문서화되었고, 여러 프로젝트와 언어에 걸쳐 replicate되었으며, 독립적으로 검증되었다.…
Cleanroom software engineering은 디버깅 대신 mathematical verification을 통해 zero-defect increment를 약속했다. 우리는 IBM의 실제 프로젝트 데이터를 살펴보아 그 주장이 성립했는지 본다.
1980년대 소프트웨어 업계 평균은 천 줄당 30~60개의 결함이었다. IBM의 Cleanroom 팀은 2만 줄짜리 컴파일러 인크리먼트를 테스트에서 53개의 결함이 발견된 상태로 출시했다. 이는 KLOC당 2.6개이다. 1만 줄짜리 개별 인크리먼트 중 일부는 시스템 테스트에서 결함이…
Box Structure는 모듈이 무엇을 하는지, 무엇을 기억하는지, 어떻게 동작하는지를 세 개의 별개이면서 검증 가능한 겹으로 정의하도록 강제한다. Cleanroom이 어떻게 디버깅을 제거하는지 알아보자.
먼저 코드를 쓰고, 다음에 테스트를 쓰고, 그제야 코드가 틀렸다는 걸 알게 된다. 이게 표준 루프다. 그래서 디버깅은 대부분의 프로젝트 타임라인 절반을 잡아먹는다. Box Structure는 이를 뒤집는다. 코드를 쓰기 전에 동작을 정의하고, 그 정의를 수학적으로 검증한 뒤, 한 겹씩…
IBM의 Cleanroom 엔지니어링 프로세스는 버그를 찾는 대신 미연에 방지함으로써 업계 평균보다 100배 우수한 결함률을 달성했다. 이것이 어떻게 작동했는지, 왜 거의 아무도 사용하지 않는지, 그리고 오늘 당신이 도입할 수 있는 것은 무엇인지 알아보자.
IBM은 NASA 위성 제어 시스템을 천 줄당 0.1개 결함이라는 수준으로 출시했다. 당시 업계 평균은 10에서 50 사이였다. 그들이 이를 달성한 것은 더 똑똑한 엔지니어를 고용하거나 더 오래 일해서가 아니다. 개발자가 자신의 코드를 실행하지 못하게 함으로써 달성한 것이다. 이것이…