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์ ์ด์ ๊ฐ ๋๋ค.
