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 2021-02-07 05:24:03
Processing time 0.0211 sec