U E D R , A S I H C RSS

Programming Pearls/Column4



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의 열쇠가 된다.


Valid XHTML 1.0! Valid CSS! powered by MoniWiki
last modified 2009-05-27 07:09:19
Processing time 0.0846 sec