Bài giảng Nguyên lý và phương pháp lập trình - TS. Nguyễn Tuấn Đăng

Nguyên lý và phương pháp lập trình<br /> <br /> Kiểm chứng tính ñúng ñắn của<br /> chương trình<br /> TS. Nguyễn Tuấn ðăng<br /> <br /> 1<br /> <br /> Nội dung<br /> •<br /> •<br /> •<br /> •<br /> •<br /> <br /> Lập trình có cấu trúc<br /> Các phương pháp hình thức<br /> Lập trình có cấu trúc theo tiếp cận top-down<br /> Cách tiếp cận kết hợp<br /> Các cấu trúc trình tự (sequences)<br /> – Các cấu trúc trình tự – hình thức hóa<br /> – Các cấu trúc trình tự – kiểm chứng<br /> – Các cấu trúc trình tự – sơ ñồ kiểm chứng<br /> <br /> • Các cấu trúc ñiều kiện<br /> – Các cấu trúc ñiều kiện – hình thức hóa<br /> – Các cấu trúc ñiều kiện – kiểm chứng<br /> – Các cấu trúc ñiều kiện – sơ ñồ kiểm chứng<br /> 2<br /> <br /> Nội dung (tt)<br /> • Các cấu trúc vòng lặp<br /> –<br /> –<br /> –<br /> –<br /> –<br /> <br /> Các cấu trúc vòng lặp – ví dụ<br /> Các cấu trúc vòng lặp – chương trình dẫn xuất<br /> Các cấu trúc vòng lặp – kết quả<br /> Các cấu trúc vòng lặp – sơ ñồ kiểm chứng<br /> Các cấu trúc vòng lặp – các lỗi trong kiểm chứng<br /> <br /> • Tóm lược<br /> <br /> 3<br /> <br /> Lập trình có cấu trúc<br /> • Chương trình sử dụng các cấu trúc ñiều khiển căn<br /> bản theo nguyên tắc 1-in, 1-out :<br /> –<br /> –<br /> –<br /> –<br /> <br /> Cấu trúc trình tự : begin S1 S2 end<br /> Cấu trúc chọn lựa : if E then S1 else S2 end<br /> Cấu trúc vòng lặp : while E loop S1 end<br /> Các cấu trúc ñiều khiển trên còn bao gồm thêm : if với<br /> elseif, case, for, etc.<br /> <br /> • Boehm và Jacopini, 1966<br /> – Chứng minh rằng cấu trúc ñiều khiển của bất kỳ một<br /> lược ñồ chương trình nào cũng có thể ñược biểu ñạt mà<br /> không cần dùng các phát biểu gotos, chỉ cần dùng các<br /> cấu trúc: trình tự, chọn lựa và vòng lặp.<br /> 4<br /> <br /> Lập trình có cấu trúc<br /> • Edsger Dijkstra, 1970<br /> – Lý luận rằng các phát biểu goto là có hại trong chương<br /> trình, ñồng thời ñưa ra ý tưởng về việc kiểm chứng tính<br /> ñúng ñắn của chương trình bằng các phương pháp hình<br /> thức.<br /> <br /> 5<br /> <br />