1. Writing Correct Programms ¶
- For writing correct programms.
- Problem Definition.
- Algorithm Design.
- Data Structure Selection.
1.1. The shallange of binary search ¶
- 100명의 프로페셔널 프로그래머들에게 Binary search를 짜보라고 시켰다. 결과는? 90퍼센트의 사람은 버그 있는 Binary search를 짰다고 한다.
- 이 칼럼의 이야기는 여기서부터 이어져 나간다.
1.2. Writing the Program ¶
- 그냥 Binary search 만들어 가는 과정을 보여주고 있다.
1.3. Understanding the Program ¶
- 프로그램의 correctness를 판별하기 위해, 프로그램의 중간중간에 assert를 집어넣고 있다.
- Loop에서의 correctness
- Initialization
- Preservation
- Termintion
- 프로그램을 한줄한줄씩 따라 내려가면서 Loop에서는 위의 원칙을 적용해 corret한가를 검사하고 있다.
1.4. Principles ¶
- Verification을 위한 general한 principles을 제공하고 있다.
- Assertions : 입력, 변수, 출력간의 관계는 프로그램의 상태를 묘사해준다. assertion은 그들의 관계를 정확히 말해준다.
- Sequential Control Structures : 이 문장 다음에 저 문장. 그 사이에 assertion을 집어넣는다. 그럼 프로그램 문장 하나하나의 각각의 진행상황을 체크할수가 있다.
- Selection Control Structures : 조건문에서 쓰인다. 각각의 조건마다, 확실히 맞다는 assertion을 집어넣어준다.
- Iteration Control Structures : 위에서도 말했듯이, 초기화, 유지, 종료조건이 확실한가를 체크해야한다.
- Functions : precondition - 함수 시작 전에 보장되어야 할 조건 -과 postcondition - 함수 끝날때에 보장되어야 할 조건 -을 명시해준다.(...) 이러한 방법을 "Programming by contract"라 한다.
1.5. The Roles of Program Verification ¶
- 가장 많이 쓰는 verification방법은 Test Case이다.
- 코드를 간결하게 유지하는 것은 대개 correctness의 열쇠가 된다.
