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