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μ μ΄μ κ° λλ€.