ĐẶC TẢ NGÔN NGỮ LẬP TRÌNH_Ngữ nghĩa tiền đề

ĐẶC TẢ NGÔN NGỮ LẬP TRÌNH NGỮ NGHĨA TIÊN ĐỀ TS. Nguyễn Hứa Phùng Khoa CNTT – ĐHBK TPHCM 2007 Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM2 NGỮ NGHĨA TIÊN ĐỀ z {P} S {Q} – P : tiền điều kiện – S : phát biểu – Q : hậu điều kiện z Nếu P đúng thì sau khi S được thực thi thì Q sẽ đúng {x = A} x := x + 1 { x = A + 1} {y ≠ 0} x := 1 / y { x = 1 / y } Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM3 NGỮ NGHĨA TIÊN ĐỀ (tt) z S, Q → P : ngữ nghĩa của S z Nếu P1⇒ P2 thì P2 yếu hơn P1 { y > 0 } x := 1 / y { x = 1 / y} y > 0 ⇒ y ≠ 0 z wp(S,Q): tiền điều kiện yếu nhất – wp(x := 1 / y, x = 1 / y) ≡ y ≠ 0 – wp(n := n + 1, n > 0) ≡ n ≥ 0 Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM4 HỆ LUẬT HOARE L1: Nếu ({P} S {Q}) ∧ (Q ⇒ R) thì {P} S {R} L2: Nếu ({P} S {Q}) ∧ (R ⇒ P) thì {R} S {Q} L3: {Px→E} x:= E {P}, với E là biểu thức và Px→E là P trong đó x được thay bằng E Ví dụ: Chứng minh: {f = i!} i := i + 1 {f * i = i!} P ↔ f * i = i! E ↔ i + 1 Pi→E↔ f *(i+1) = (i+1)! Theo L3: {f *(i+1) = (i+1)!} i := i + 1 {f * i = i!} Vì f = i! ⇒ f *(i+1) = (i+1)! nên theo L2 ta có điều cần cm Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM5 HỆ LUẬT HOARE (tt) L4: Nếu ({P} S1 {Q}) ∧ ({Q} S2 {R}) thì {P} S1; S2 {R} Ví dụ: Chứng minh {f =i!} i := i + 1; f := f * i {f = i!} Theo ví dụ trước, ta có {f = i!} i := i + 1 {f * i = i!} (1) Ta chứng minh {f * i = i!} f := f * i {f = i!} (2) P ↔ f = i! E ↔ f * i Pi→E↔ f *i = i! Theo L3, (2) được chứng minh Theo L4 và (1),(2) ta có điều phải chứng minh Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM6 HỆ LUẬT HOARE (tt) L5: Nếu ({P ∧ B} S1 {Q}) ∧ ({P ∧ ¬B} S2 {Q}) thì {P} if B then S1 else S2 {Q} L6: Nếu ({P ∧ B} S1 {Q}) ∧ ((P ∧ ¬B) ⇒ Q) thì {P} if B then S1 {Q} Ví dụ: {xy y then max := x else max :=y {max > 0} Theo L3, ta có {x > 0} max := x {max > 0} Vì (xy y) ⇒ (x > 0) nên theo L2 ta có {(xy y)} max := x {max > 0} Tương tự {(xy 0} Áp dụng L5 ta có điều cần chứng minh Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM7 HỆ LUẬT HOARE (tt) L7: Nếu {P ∧ B} S {P} thì {P} while B do S {P ∧ ¬B} Ví dụ: {f =i!} while i≠n do begin i := i +1; f := f * i end {f=n!} Theo ví dụ trước ta đã chứng minh {f =i!} i := i + 1; f := f * i {f = i!} Vì (f = i!) ∧ (i≠n) ⇒ f = i! nên theo L2 {(f = i!) ∧ (i≠n)} i := i + 1; f := f * i {f = i!} Với P ↔ f = i! B ↔ i≠n S ↔ i := i + 1; f := f * i theo L7: {f =i!} while i≠n do begin i := i +1; f := f * i end {(f=i!) ∧ (i=n)} mà (f=i!) ∧ (i=n) ⇒ f = n! nên theo L1 ta có điều cần phải chứng minh Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM8 CHỨNG MINH CHƯƠNG TRÌNH {P} Prog {Q} z Đúng đắn bộ phận: nếu P đúng, sau khi thực hiện Prog thì Q đúng z Đúng đắn toàn phần: thì Prog đúng đắn bộ phận và nếu P đúng thì Prog dừng Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM9 VÍ DỤ Chứng minh {n ≥ 0} i := 0; f := 1; while i ≠ n do begin i:= i +1; f := f * i end {f = n!} Ta đã chứng minh {f = i!} while i ≠ n do begin i:= i +1; f := f * i end {f = n!} Áp dụng L3 với P ↔ f = i! E↔ 1 Pf →E↔ 1 = i! ta được {1 = i!} f := 1 {f = i!} Áp dụng L3 với P ↔ 1 = i! E↔ 0 Pi→E↔ 1 = 0! ta được {1 = 0!} i := 0 {1 = i!}Vì 1 = 0! luôn luôn đúng nên n ≥ 0 ⇒ 1 = 0!. Theo L2 ta được {n ≥ 0} i := 0 {1 = i!}. Áp dụng L4 ta có điều cần phải cm Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM10 VÍ DỤ Chứng minh: {n ≥ 0} i := n; f := 1; while i > 0 do begin f := f * i ; i := i -1; end {f = n!} Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM11 (2) Ta chứng minh {f = i*...*n ∧ i -1 ≥ 0} i := i – 1; {f = (i+1)*...*n ∧ i ≥ 0} Áp dụng L3 ta dễ dàng cm (2) (3) Ta chứng minh {f = (i+1)*...*n ∧ i -1 ≥ 0} f := f * i; {f = i*...*n ∧ i -1 ≥ 0} Áp dụng L3 ta xác định tiền điều kiện của f := f * i là f * i = i *...* n ∧ i -1 ≥ 0 ≡ f = (i+1)*...* n ∧ i -1 ≥ 0 Áp dụng L2 ta cm (3) (1) Ta chứng minh: {f = (i+1)*...n ∧ i ≥ 0} while i > 0 do begin f := f * i; i := i – 1; end {f = n!} Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM12 Áp dụng L4 cho (2) và (3) ta được: {f = (i+1)*...*n ∧ i -1 ≥ 0} f := f*i; i := i-1 {f = (i+1)*...*n ∧ i ≥ 0} Gọi P = {f = (i+1)*...n ∧ i ≥ 0} và B = i > 0, ta có P ∧ B → {f = (i+1)*...*n ∧ i -1 ≥ 0}, do đó theo L2 ta được {P ∧ B} f := f*i; i := i-1 {P} Áp dụng L7 cho phát biểu while, ta có {P} while B do begin ... end {P ∧ ¬B} Mà P ∧ ¬B = (f = (i+1)*...*n ∧ i ≥ 0) ∧ i ≤ 0 → f = (i+1)*...*n ∧ i = 0 đa → f = n! Áp dụng L1, ta đã cm (1). Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM13 Áp dụng L3 cho f := 1 ta dễ dàng chứng minh {1 = (i+1)* ...* n ∧ i ≥ 0} f := 1 {f = (i+1)* ...* n ∧ i ≥ 0} (4) Áp dụng L3 cho i := n ta cũng cm được {1 = 1 ∧ n ≥ 0} i := n {1 = (i+1)* ...* n ∧ i ≥ 0} Vì 1 = 1 là true nên {n ≥ 0} → {1 = 1 ∧ n ≥ 0} Vậy theo L2 ta có {n ≥ 0} i := n {1 = (i+1)* ...* n ∧ i ≥ 0} (5) Áp dụng L4 cho (4), (5) và (1) ta có điều cần chứng minh Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM14 ĐÚNG ĐẮN TOÀN PHẦN z L8: if {P ∧ B ∧ 0 ≤ E = E0} C {P ∧ 0 ≤ E < E0} then {P ∧ 0 ≤ E }while B do C {P ∧ ¬B} z E: an integer expression called variant Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM15 Ví dụ { n ≥ 0} ⇒ f := 1; i := 0; while (n ≠ i) { i := i + 1; f := f * i; } { f = n!} Để cm (1), ta cm (2): {f = i! ∧ n ≠ i ∧ 0 ≤ n – i = E0} i := i + 1; f := f * i; { f = i! ∧ 0 ≤ n – i < E0} Ta cm (1): {f = i! ∧ 0 ≤ n – i} while (n ≠ i) { i := i + 1; f := f * i; } { f = n!} Mà theo L3, ta có {f = i! ∧ 0 ≤ n – i – 1 < E0} i := i + 1; {f*i = i! ∧ 0 ≤ n – i < E0} f := f * i; { f = i! ∧ 0 ≤ n – i < E0} f = i! ∧ n ≠ i ∧ 0 ≤ n – i = E0 ⇒ f = i! ∧ 0 ≤ n – i – 1 < E0? Ngữ Nghĩa Tiên Đề Khoa CNTT-DHBK TPHCM16 KIỂM CHỨNG KHI THỰC THI #include ... assert(n >= 0); i := n; f := 1; while i > 0 do begin f := f * i ; i := i -1; end if (n < 0) throw Exception; i := n; f := 1; while i > 0 do begin f := f * i ; i := i -1; end