Kiểm chứng tính đúng đắn của chương trình Verifying Program Correctness

University of FloridaDept. of Computer & Information Science & EngineeringCOT 3100Applications of Discrete StructuresDr. Michael P. Frank Slides for a Course Based on the TextDiscrete Mathematics & Its Applications (5th Edition)by Kenneth H. Rosen Module #17:Kiểm chứng tính đúng đắn của chương trình Verifying Program Correctness Rosen 5th ed., §3.6 ~18 slides, ~1 lecture Tính đúng đắn của chương trình§3.6: Program Correctness Ta muốn có khả năng chứng minh rằng chương trình đã cho đáp ứng được yêu cầu đề ra. Điều đó thông thường có thể làm bằng tay hoặc các công cụ kiểm chứng chương trình tự động. Một ví dụ là PVS (People’s Verification System). Chương trình là đúng nếu nó tạo ra đầu ra đúng cho mỗi đầu vào hợp lệ. Chương trình có tính đúng đắn bộ phận nếu nó tạo ra đầu ra đúng cho mỗi đầu vào khi nó chắc chắn dừng. Xác nhận ban đầu và cuối cùng Đặc tả vào ra của chương trình có thể sử dụng xác nhận ban đầu và kết thúc. Xác nhận ban đầu (initial assertion) p là điều kiện mà đảm bảo đầu vào của chương trình phải thỏa mãn. Xác nhận kết thúc (final assertion) q là điều kiện mà đầu ra của chương trình yêu cầu phải thỏa mãn. Ký hiệu bộ ba Hoare: Ký hiệu p{S}q nghĩa là, với mọi đầu vào I sao cho p(I) là đúng, chương trình S (với đầu vào I) dừng và tạo đầu ra O = S(I), thì q(O) là đúng. Có nghĩa là, S là đúng đắn bộ phận ứng với đặc tả p,q. Ví dụ hiển nhiênA Trivial Example G/s S là đoạn chương trình “y := 2; z := x+y” G/s p là xác nhận ban đầu “x = 1”. Biến x nhận giá trị bằng 1 tại mọi trạng thái ban đầu. G/s q là xác nhận kết thúc “z = 3”. Biến z phải nhận giá trị 3 tại mọi trạng thái kết thúc. Chứng minh p{S}q. Proof: If x=1 in the program’s input state, then after running y:=2 and z:=x+y, z will be 1+2=3. Luật suy diễn của bộ ba HoareHoare Triple Inference Rules Các luật tổng hợp cho các bộ ba Hoare. Ví dụ đơn giản: Luật kết hợp p{S1}q q{S2}r∴ p{S1; S2}r Điều đó cho biết: Nếu c/trình S1 với điều kiện p sẽ tạo nên điều kiện q, và S2 với điều kiện q tạo nên r, thì chương trình “S1 nối tiếp S2”, nếu cho trước p, sẽ tạo nên r. Luật suy diễn cho lệnh ifInference rule for if statements (p  cond){S}q (p  ¬cond)→q∴ p{if cond then S}q VD: Chỉ ra rằng: T {if x>y then y:=x} y≥x. C/m: nếu ban đầu x>y, thì nếu thực hiện thân chương trình, đặt y=x, và sau đó hiển nhiên y≥x là đúng. Ngược lại, x≤y và vì vậy y≥x. Trong trường hợp này không làm gì và y≥x vẫn là đúng. Khi áp dụng qui tắc đó, các yêu cầu đều thỏa mãn. if-then-else rule (p  cond){S1}q (p  ¬cond){S2}q∴ p{if cond then S1 else S2}q VD: Chỉ ra rằng T {if x<0 then abs:=−x else abs:=x} abs=|x| Nếu x<0 thì sau thân chương trình if, abs sẽ bằng |x|. Nếu ¬(x<0), t.l., x≥0, thì sau thân else, abs=x, mã cũng là |x|. Vậy qui tắc được áp dụng. Bất biến vòng lặpLoop Invariants Đối với vòng lặp “while cond S”, ta nói p là bất biến vòng lặp của vòng lặp trên nếu (pcond){S}p. Nếu p (và tiếp theo là điều kiện tiếp diễn cond) là đúng trước khi thực hiện thân vòng lặp, và p vẫn luôn đúng từ đó trở đi. Và vì vậy p luôn đúng qua mọi bước lặp. Nó dẫn đến luật suy diễn sau: (p  cond){S}p∴ p{while cond S}(¬cond  p) Ví dụ bất biến vòng lặpLoop Invariant Example Chứng minh bộ ba Hoare sau thỏa mãn: T {i:=1; fact:=1; while i<n {i++; fact*=i}}(fact=n!) Proof. Nhận thấy p:≡“fact=i!  i≤n” là bất biến vòng lặp, và nó đúng trước khi vào vòng lặp. Vì vậy, sau vòng lặp ta có ¬condp  ¬(i<n) fact=i!  i≤n  i=n  fact=i!  fact=n!. ■ Ví dụ lớn - Big Example procedure multiply(m,n: integers) m,nZif n<0 then a:=−n else a:=n a=|n|k:=0; x:=0 x = mk  k≤a while k<a { Maintains loop invariant: x += m; k++ x = mk  k≤a} x = mk  k=a ∴ x = ma = m|n|  ∴ (n<0  x=−mn)  (n≥0  x=mn)if n<0 then prod := −x else prod:=x prod = mn Tìm kiếm nhị phân Giải thích Tiền điều kiện: Danh sách L(1..n) được sắp xếp i = 1, j = n Điều kiện dừng của vòng lặp Bước i < j Bất biến vòng lặp: Key trong L(1..n)  key trong L(i..j) Khi thoát khỏi vòng lặp i=j, kiểm tra key = L[i]? (cũng là key có trong L(1..n)?) Ước chung lớn nhất Giải thích Tiền điều kiện: a, b là nguyên dương Bất biến vòng lặp: GCD(x,y) = GCD(a,b) x = b; y = a mod b Điều kiện dừng y = 0, khi đó x là GCD(a,b)