Đặ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