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

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.
Nội dung trích xuất từ tài liệu:
Bài giảng Nguyên lý và phương pháp lập trình - TS. Nguyễn Tuấn ĐăngNguyên lý và phương pháp lập trìnhKiểm chứng tính ñúng ñắn củachương trìnhTS. Nguyễn Tuấn ðăng1Nội dung•••••Lập trình có cấu trúcCác phương pháp hình thứcLập trình có cấu trúc theo tiếp cận top-downCách tiếp cận kết hợpCá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ứng2Nộ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ấtCá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ứngCác cấu trúc vòng lặp – các lỗi trong kiểm chứng• Tóm lược3Lậ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ănbản theo nguyên tắc 1-in, 1-out :––––Cấu trúc trình tự : begin S1 S2 endCấu trúc chọn lựa : if E then S1 else S2 endCấu trúc vòng lặp : while E loop S1 endCác cấu trúc ñiều khiển trên còn bao gồm thêm : if vớielseif, 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ộtlượ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áccấu trúc: trình tự, chọn lựa và vòng lặp.4Lậ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ươngtrì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 hìnhthức.5