Bài giảng Kiểm chứng tính đúng đắn của chương trình

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 hình thức. 5 Các phương pháp hình thức • Dựa trên ý tưởng rằng các chương trình là những đối tượng tốn học – Một chương trình “hữu hạn” (ie. cĩ tính dừng) là biểu diễn của một hàm, hàm này ánh xạ các trạng thái nào đĩ của bộ nhớ (các trạng thái bắt đầu) đến các trạng thái khác của bộ nhớ (các trạng thái kết thúc). – Một chương trình “vơ hạn” (ie. khơng dừng) cĩ thể được diễn đạt như một module “hữu hạn” (ie. cĩ tính dừng) trong một vịng lặp vơ hạn. 6 Các phương pháp hình thức (tt) • Tony Hoare, 1969 – Viết một bài báo tựa đề: “An Axiomatic Basis for Computer Programming”. Bài báo này mơ tả sự dẫn xuất của mã chương trình từ các tiên đề, theo cách đĩ thì tính đúng đắn của chương trình cĩ thể chứng minh một cách hình thức. • Harlan Mills, 1987 – Phát triển kỹ thuật “Cleanroom Software Engineering” dựa trên các phương pháp hình thức để kiểm tra tính đúng đắn của chương trình. 7 Các phương pháp hình thức (tt) • Ưu điểm: – Cung cấp một phương pháp cĩ thể kiểm chứng được để khai triển các đặc tả thành chương trình – Dựa trên các kỹ thuật tốn học hình thức – Cách hiệu quả để kiểm chứng tính đúng đắn của chương trình – ðược hỗ trợ bằng một số ngơn ngữ hình thức (Z, VDM- SL, REFINE), các hệ thống kiểm tra-kiểm chứng. • Nhược điểm: – Một số các khái niệm của phương pháp này đơi khi cịn chưa rõ – 8 Lập trình cĩ cấu trúc theo tiếp cận top-down • Phương pháp – Lập trình bằng cách mịn hĩa từng bước – Dùng các cấu trúc điều khiển dạng 1-in/1-out – Các kỹ thuật kiểm chứng • Bắt đầu với: – Một phát biểu chưa được mịn hĩa – Một đặc tả hình thức của phát biểu 9 Lập trình cĩ cấu trúc theo tiếp cận top-down (tt) • Mịn hĩa từng bước các phát biểu để đạt được kết quả là thay thế chúng (nếu cĩ) bằng: – Các cấu trúc trình tự – Các cấu trúc điều kiện – Các cấu trúc lặp – Các phát biểu thực thi (gán, gọi hàm) • Kiểm tra tính đúng đắn ở mỗi bước 10 Hướng tiếp cận kết hợp • Xây dựng chương trình bằng lập trình cĩ cấu trúc theo cách tiếp cận top-down • Mịn hĩa chương trình bằng cách sử dụng các biến đổi bảo tồn ngữ nghĩa (Semantics-Preserving Transformations - SPTs) 11 Hướng tiếp cận kết hợp P P P is a function defined by (a) an informal comment (b) a formal specification X and Y are functions top-down refinement continues until only begin X Y end begin X Y executable code remains if Q then R else S end while B loop M end end Q R S B M SPT executable code (use compiler, interpreter, or prototyping tool) optimized code in target language 12 Các cấu trúc trình tự 1. Vấn đề: làm mịn phát biểu sau [ F: let x = y * | z | ] 2. Bước 1: Thay F bằng các phát biểu sau [ G: let k = | z | ] F [ H: let x = y * k ] 3. Phương pháp thay F bằng cấu trúc trình tự: – Chọn G G H 13 Các cấu trúc trình tự (tt) – Chọn H sao cho (a) H được xây dựng trên cơ sở G và H phải tương đương với F – Kiểm tra (a) F 14 G H Các cấu trúc trình tự – Hình thức hĩa 4. Hình thức hĩa: thay thế mỗi phát biểu bằng một đặc tả hình thức với các tiên đề P, Q, và R: formal spec PDL [ F: let x = y * | z | ]{P} F {R} [ G: let k = | z | ] [ H: let x = y * k ] {P} G {Q} {Q} H {R} where P = (x, y, z are integers) Q = (P and K is integer and k = |z|) R = (P and x = y * |z|) 15 Các cấu trúc trình tự – Hình thức hĩa (tt) • {P}F{R} cĩ nghĩa: “Nếu P đúng trước khi F được thực hiện, thì R sẽ đúng sau khi F được thực hiện.” • P được gọi là tiền điều kiện (precondition) của F • R được gọi là hậu điều kiện (postcondition) của F 16 Các cấu trúc trình tự – Kiểm chứng 5. Giả sử G và H đã được kiểm chứng đúng, nghĩa là: {P} G {Q} and {Q} H {R} 6. Thì F đúng, vì {P} F {R} 7. Bước (6) được suy ra từ bước (5) bằng qui tắc kiểm chứng: {P} G {Q}, {Q} H {R} {P} G H {R} 17 Các cấu trúc trình tự – Sơ đồ kiểm chứng G P Q H R Proof rule for sequences {P} G {Q}, {Q} H {R} {P} G H {R} 18 GT F Các cấu trúc điều kiện 1. Vấn đề: mịn hĩa phát biểu sau [ G: let k = | z | ] 2. Bước 2: Thay thế G với cấu trúc điều kiện DC B G: if z < 0 [test B] then [ C: let k = -z ] else [ D: let k = z ] end 19 GT F Các cấu trúc điều kiện 3. Phương pháp thay thế G bằng một cấu trúc điều kiện: – Chọn điều kiện B – Chọn C và D sao cho (a) C thực hiện G khi B đúng DC B (b) D thực hiện G khi B sai – Kiểm tra (a) và (b) 20 Các cấu trúc điều kiện – Hình thức hĩa 4. Các đặc tả hình thức cho G, C, D: formal spec PDL [ G: let k = | z | ] G: if z < 0 [test b]{P} G {Q} {P and B} C {Q} {P and not B} D {Q} where P = (x, y, z are integers) B = (z < 0) Q = (P and k is integer and k = |z|) then [C: let k = -z] else [D: let k = z] end 21 Các cấu trúc điều kiện – Hình thức hĩa (tt) 5. Nếu C và D đúng, G được kiểm chứng bằng qui tắc: {P and B} C {Q}, {P and not B} D {Q} {P} if B then C else D end {Q} 22 Các cấu trúc điều kiện – Kiểm chứng 6. Bước mịn hĩa cuối cùng: thay C, D, và H bằng các phát biểu (của ngơn ngữ lập trình) thỏa mãn đặc tả: G: if z < 0 [kiểm tra B] then C: k := -z else D: k := z end H: x := y * k 23 Các cấu trúc điều kiện – Kiểm chứng (tt) 7. Kiểm chứng tính đúng đắn: {P and B} C {Q} [định nghĩa phát biểu gán] {P and not B}D{Q} [định nghĩa phát biểu gán] {P} G {Q} [Qui tắc kiểm chứng cho các cấu trúc điều kiện] {Q} H {R} [định nghĩa phát biểu gán] {P} F {R} [Qui tắc kiểm chứng cho các cấu trúc trình tự] 24 Các cấu trúc điều kiện – Kiểm chứng (tt) 8. Áp dụng các biến đổi bảo tồn ngữ nghĩa, nhận được: if z < 0 then z := -z end x := y * z 25 Các cấu trúc điều kiện – Sơ đồ kiểm chứng DC B false P true P and not B Qui tắc kiểm chứng cho các điều kiện: {P and B} C {Q}, {P and not B} D {Q} {P} if B then C else D end {Q} Q 26 Các cấu trúc vịng lặp 1. Dạng tổng quát cho vịng lặp while : formal spec PDL {P} F {R} {P} G {Q} {Q and B} H {Q} [F: ... function] [G: ... initialization] while B loop [H: ... body] end 27 Các cấu trúc vịng lặp (tiếp theo) 2. Qui tắc kiểm chứng cho vịng lặp while: {P} G {Q}, {Q and B} H {Q} {P} G; while B loop H end {Q and not B} 3. Phương pháp thay thế F bằng cấu trúc vịng lặp while: – Chọn Q (bất biến vịng lặp) và B (điều kiện vịng lặp) sao cho (Q and not B) bao hàm R – Chọn G và H sao cho (a) G làm cho Q đúng (b) B cĩ thể sai (để vịng lặp kết thúc) (c) thực hiện H khi B và Q đúng – Kiểm tra (a), (b), và (c) 28 Các cấu trúc vịng lặp – Ví dụ 4. Vấn đề: mịn hĩa phát biểu [F: Tìm phần tử nhỏ nhất a(j) trong dãy các phần tử a(i..n) của mảng a] 5. ðặc tả hình thức: {P} F {R} trong đĩ P=(a ∈ integer array and i, n ∈ integer and 1 ≤ i ≤ n ≤ size(a)) R=(P and j ∈ integer and i≤j≤n and a(j)=min(a(i..n))) 6. Giải pháp: Q=(P and j, k ∈ integer and i≤j≤k≤n and a(j)=min(a(i..k))) B=(k<n) 29 a i j k n min of Các cấu trúc vịng lặp – Ví dụ 7. Kiểm tra: (Q and not B) bao hàm k=n ∴ (Q and not B) bao hàm R a i j k n min of 30 Các cấu trúc vịng lặp – Chương trình dẫn xuất [ P: 1 ≤ i ≤ n ≤ size(a) ] G: j := i k := i [ Q: P and i ≤ j ≤ k ≤ n and a(j)=min(a(i..k)) ] while k < n [test B] loop [ L1: Q and B ] H: k := k + 1 [để B cĩ thể sai] [ L2: P and a(j)=min(a(i..k-1)) ] [để Q đúng] if a(j) > a(k) then [ T1: L2 and a(k) < a(j) ] 31 Các cấu trúc vịng lặp – Chương trình dẫn xuất (tt) j := k [ T2: a(j)=min(a(i..k)) ] else [ F1: a(j) ≤ a(k) ] end end [ R: Q and not B ] 32 Các cấu trúc vịng lặp – Kết quả proc f (a [array], i, n [integers] ) descr [f(a, i, n) = j where a(j) = min(a(i..n))] local j, k [integers] pre [1 ≤ i ≤ n ≤ size(a) ] post [1 ≤ i ≤ j ≤ n ≤ size(a) and a(j)=min(a(i..n)) ] begin if not (1<=i and i<=n and n<= size(a)) then write("input error") return nil end j := i k := i while k < n 33 Các cấu trúc vịng lặp – Kết quả (tt) loop [loop invariant: a(j)=min(a(i..k)) and 1 ≤ i ≤ j ≤ k ≤ n ≤ size(a) ] k := k + 1 if a(j) > a(k) then j := k end end return j end 34 Các cấu trúc vịng lặp – Sơ đồ kiểm chứng G B false Q Q and not B P Q Qui tắc kiểm tra cho vịng lặp while là : {P} G {Q}, {Q and B} H {Q} {P} G; while B loop H end {Q and not B} H true R Q and B 35 Các cấu trúc vịng lặp – Các lỗi trong kiểm chứng • Các lỗi phổ biến trong việc kiểm chứng tính đúng đắn của chương trình: – Khơng xác định đúng bất biến vịng lặp Q. Một bất biến vịng lặp là một khẳng định khơng thay đổi, chẳng hạn như Q đúng: • Trước khi thực hiện vịng lặp • Sau mỗi bước của vịng lặp • Sau khi kết thúc vịng lặp – Khơng kiểm tra xem vịng lặp cĩ kết thúc hay khơng – trường hợp các vịng lặp vơ hạn 36 Tĩm lược • Cĩ thể áp dụng kiểm chứng hình thức đối với: – Các cấu trúc trình tự – Các cấu trúc điều kiện – Các cấu trúc vịng lặp • Mỗi phát biểu cĩ: – Một tiền điều kiện – Một hậu điều kiện • Mỗi thủ tục cĩ: – Một tiền điều kiện – Một hậu điều kiện 37 Tĩm lược (tt) • Mỗi cấu trúc vịng lặp cĩ: – Một tiền điều kiện – Một hậu điều kiện – Một bất biến vịng lặp 38