ProgrammingPearls/Column4

Writing Correct Programms

• For writing correct programms.
  • Problem Definition.
  • Algorithm Design.
  • Data Structure Selection.

The shallange of binary search

• 100명의 프로페셔널 프로그래머들에게 Binary search를 짜보라고 시켰다. 결과는? 90퍼센트의 사람은 버그 있는 Binary search를 짰다고 한다.
• 이 칼럼의 이야기는 여기서부터 이어져 나간다.

Writing the Program

• 그냥 Binary search 만들어 가는 과정을 보여주고 있다.

Understanding the Program

• 프로그램의 correctness를 판별하기 위해, 프로그램의 중간중간에 assert를 집어넣고 있다.
• Loop에서의 correctness
  • Initialization
  • Preservation
  • Termintion
• 프로그램을 한줄한줄씩 따라 내려가면서 Loop에서는 위의 원칙을 적용해 corret한가를 검사하고 있다.

Principles

• Verification을 위한 general한 principles을 제공하고 있다.
  • Assertions : 입력, 변수, 출력간의 관계는 프로그램의 상태를 묘사해준다. assertion은 그들의 관계를 정확히 말해준다.
  • Sequential Control Structures : 이 문장 다음에 저 문장. 그 사이에 assertion을 집어넣는다. 그럼 프로그램 문장 하나하나의 각각의 진행상황을 체크할수가 있다.
  • Selection Control Structures : 조건문에서 쓰인다. 각각의 조건마다, 확실히 맞다는 assertion을 집어넣어준다.
  • Iteration Control Structures : 위에서도 말했듯이, 초기화, 유지, 종료조건이 확실한가를 체크해야한다.
  • Functions : precondition - 함수 시작 전에 보장되어야 할 조건 -과 postcondition - 함수 끝날때에 보장되어야 할 조건 -을 명시해준다.(...) 이러한 방법을 "Programming by contract"라 한다.

The Roles of Program Verification

• 가장 많이 쓰는 verification방법은 Test Case이다.
• 코드를 간결하게 유지하는 것은 대개 correctness의 열쇠가 된다.

---

ProgrammingPearls