[Bài Giảng] Chương 4: Đặc tả và tính đúng đắn của hàm

Chương 4 : Đặc tả và tính đúng đắn của hàm

Nội dung

• Đặc tả và tính đúng đắn của hàm

1. Đặt vấn đề
2. Các phương pháp kiểm tra

• Chứng minh với các luật suy diễn

1. Ký hiệu
2. Các luật suy diễn

Giới thiệu

Ta xét hàm f với đặc tả như sau:

Domain : P(x)
Where: Q(x, y)

Có cài đặt tương ứng là:
Y f(X)
{
lệnh 1;
lệnh 2;
lệnh 3;
//…
}

Bài toán đặt ra ở đây là hãy cho biết cài đặt trên có phù hợp với đặc tả đã có hay không?
Đây chính là bài toán về kiểm tra tính đúng đắn của hàm. Nếu cài đặt cụ thể của hàm f là phù hợp với đặc tả, ta nói cài đặt đó là đúng, ngược lại, cài đặt đó là chưa chính xác.

• Để kiểm tra tính đúng đắn của 1 hàm sau khi cài đặt, người ta sử dụng một số phương pháp khác nhau, hoặc cũng có thể kết hợp đồng thời các phương pháp này.
• Có 2 phương pháp chính:

1. Kiểm tra động
2. Kiểm tra tĩnh

Kiểm tra động

• Phương pháp kiểm tra động (dynamic testing), hay còn được gọi là phương pháp thử nghiệm được thực hiện như sau :

1. Lập các bộ số làm thử nghiệm, hay còn được gọi là các bộ dữ liệu thử nghiệm (test cases).
2. Lần lượt cho thực hiện hàm f với các giá trị x đã chọn, ghi nhận lại kết quả y.
3. So sánh y và y0. 

• Phương pháp này chính là phương pháp kiểm thử chủ đạo được áp dụng trong giai đoạn lập trình và giai đoạn kiểm thử của quy trình phát triển phần mềm trên thế giới hiện nay.
• Các công cụ hỗ trợ phương pháp này:

1. Công cụ phát sinh các dữ liệu thử nghiệm.
2. Công cụ cho phép thực thi hàm và ghi nhận kết quả.
3. Công cụ kiểm tra tính phù hợp của cài đặt hàm so với đặc tả.
4. Các công cụ tự động phát sinh hàm từ đặc tả, cho thực hiện hàm phát sinh và tự động kiểm tra kết quả thực hiện.  

• Phương pháp này còn được biết đến với 1 tên gọi khác là "kiểm thử hộp đen" (black box testing)
• Phương pháp không chú trọng đến cài đặt bên trong của các hàm
• Nó chỉ quan tâm đến kết quả thực hiện của hàm để khẳng định hàm đó có phù hợp với đặc tả không mà thôi
• Chưa đề cập đến việc sửa chữa cài đặt của hàm lại sao cho phù hợp 

Kiểm tra tĩnh

• Phương pháp kiểm tra tĩnh (static testing), còn được gọi là "kiểm thử hộp trắng" (white box testing).
• Phương pháp này thực hiện theo cơ chế lần lượt đọc các lệnh trong chương trình nguồn (phần cài đặt của hàm)
• Sau đó chứng minh bằng tay, hoặc chứng minh tự động tính đúng đắn của hàm sau từng lệnh.

Ta xét hàm f với đặc tả và cài đặt:

Ta xét các kết quả trung gian:

• Q1(x,y): điều kiện sau khi thực hiện lệnh 1
• Q2(x,y): điều kiện sau khi thực hiện lệnh 2
• Q3(x,y): điều kiện sau khi thực hiện lệnh 3
• …
• Qk(x,y): điều kiện sau khi thực hiện lệnh k

Các bước chứng minh:
From P(x)
Q1(x, y) lệnh 1 được thực hiện.
Q2(x, y) lệnh 2 được thực hiện.
...
Qk(x, y) lệnh k được thực hiện.
Infer Q(x, y)

Chứng minh với luật suy diễn

Cho E1, E2 là 2 mệnh đề. Trong quá trình chứng minh, nếu suy diễn được E1 thì cũng suy diễn được E2, ta ký hiệu:

Các luật suy diễn

• Suy diễn trên phép phủ định
• Suy diễn trên phép hội
• Suy diễn trên phép giao
• Suy diễn trên phép kéo theo

Suy diễn trên phép phủ định

i.e: Tôi có nhà.
Vậy: không thể có chuyện tôi không có nhà, và ngược lại.

Các luật suy diễn

1. Suy diễn trên phép phủ định
2. Suy diễn trên phép hội
3. Suy diễn trên phép giao
4. Suy diễn trên phép kéo theo

Suy diễn trên phép hội 

Suy diễn MỞ RỘNG:

i.e: Tôi có nhà.
Vậy: Tôi có nhà hay xe.
 Tôi có xe hay nhà.

Suy diễn THEO TRƯỜNG HỢP:

i.e: Tôi có tiền hoặc vàng.
Có tiền tôi sẽ có xe mới.
Có vàng tôi cũng sẽ có xe mới.
Vậy: Chắc chắn tôi sẽ có xe mới

Suy diễn DE MORGAN:

i.e: Tôi ko có tiền hay vàng gì cả.
Vậy: Tôi không có tiền và cũng chẳng   có vàng, và ngược lại.

Suy diễn KẾT HỢP:

Suy diễn trên phép giao

Suy diễn THEO ĐỊNH NGHĨA:

i.e: Tôi có cả xe lẫn nhà.
Vậy: Không thể có chuyện tôi không có xe hoặc không có nhà, và ngược lại.

Suy diễn RÚT GỌN:



i.e: Tôi có cả xe lẫn nhà.
Vậy: Tôi chắc chắn có nhà.
Tôi chắc chắn có xe.

Suy diễn TỔNG HỢP:

i.e: Tôi có xe.
Tôi cũng có nhà.
Vậy: Tôi có cả xe lẫn nhà.

Suy diễn DE MORGAN:

i.e: Tôi ko có đồng thời cả tiền và vàng
Vậy: Hoặc là tôi không có tiền, hoặc tôi chẳng   có vàng, và ngược lại.

Suy diễn KẾT HỢP:

Suy diễn trên phép kéo theo

Suy diễn BÀI TAM:

Suy diễn DỰA TRÊN MÂU THUẪN:

Suy diễn KÉO THEO:

Suy diễn KÉO THEO 2 CHIỀU:

Chứng minh suy diễn 

Khi chứng minh suy diễn
ta áp dụng dạng thức sau:
From E
Kết quả 1 Luật suy diễn áp dụng(các kquả sd)
Kết quả 2 Luật suy diễn áp dụng(các kquả sd)
...
Infer F

Ví dụ: Chứng minh các suy diễn sau

Bài tập áp dụng
Ví dụ: Chứng minh các suy diễn sau

Tóm tắt chương

• Kiểm thử nhằm mục đích đảm bảo tính đúng đắn của hàm, của chương trình.
• Có 2 phương pháp kiểm thử chính: kiểm thử động và kiểm thử tĩnh.
• Chứng minh tính đúng đắn của hàm dựa vào các luật suy diễn.
• Có các luật suy diễn trên phép phủ định, hội, giao, và kéo theo.

HẾT CHƯƠNG 4

[Bài Giảng] Chương 3: Đặc tả thành phần cơ sở

Nội dung

• Mục tiêu của chương
• Đặc tả kiểu dữ liệu
• Đặc tả hàm
• Đặc tả đệ quy
• Các quy tắc tính toán
• Các sơ đồ trạng thái
• Các đối tượng hình học
• Các ràng buộc
• Tóm tắt chương
• Bài tập

Mục tiêu của chương
Sau chương này, người học có thể dùng ngôn ngữ toán học để:

• Đặc tả các hàm tính toán.
• Đặc tả các tính toán mang tính đệ quy.
• Đặc tả các quy tắc tính toán.
• Đặc tả các sơ đồ trạng thái
• Đặc tả các đối tượng hình học
• Đặc tả các ràng buộc

Đặc tả kiểu dữ liệu
Một kiểu dữ liệu bao gồm :

• Tập hợp các giá trị
• Hệ thống các phép toán cơ sở
• Dựa trên các phép toán này, ta có thể đặc tả các phép toán còn lại. 

Một phép toán (có thể được gọi là 1 hàm) là một ánh xạ riêng phần trên tập D  X :

Domain : điều kiện x Î D
Where: y là ảnh của x.
D được gọi là miền xác định của f
Một số kiểu dữ liệu cơ bản:

Kiểu chuỗi
Kiểu dữ liệu chuỗi:

• Là tập hợp tất cả các chuỗi ký tự.
• Các phép toán cơ sở bao gồm:

1. Chuỗi rỗng

Domain:
Where: b=True <=> s là chuỗi rỗng

2. Khởi tạo

Domain:
Where: s là chuỗi gồm đúng 1 ký tự là c

3. Chèn đầu

Domain:
Where: t được tạo lập bằng cách chèn ký tự c vào đầu chuỗi s

4. Xóa đầu

Domain: ØRong(s)
Where: t được tạo lập bằng cách xóa ký tự đầu tiên ra khỏi chuỗi s

5. Lấy phần tử đầu

Domain: ØRong(s)
Where: c là ký tự đầu tiên của chuỗi s

6. Phép so sánh =

Domain:
Where: b <=> 2 chuỗi s và t giống nhau hoàn toàn.

7. Tìm chiều dài chuỗi:

Domain:
Where: l=số ký tự có trong chuỗi

Đặc tả hàm

Ví dụ 1: Đặc tả các hàm sau:

• Tìm căn bậc 2 của 1 số thực
• Tìm phần nguyên của 1 số thực
• Hàm DIV (2 số nguyên không âm)
• Hàm MOD (2 số nguyên không âm) 

Hàm căn bậc 2:

 

Hàm tìm phần nguyên:

Hàm chia nguyên :

Hàm chia lấy phần dư:

Ví dụ 2: Dựa vào các hàm cơ sở trên kiểu dữ liệu chuỗi, hãy đặc tả các hàm sau:

• Xóa 2 ký tự đầu của 1 chuỗi.
• Tìm phần tử thứ 2 của 1 chuỗi.
• Chèn 1 ký tự vào vị trí thứ 2 của chuỗi.

Xóa 2 phần tử đầu của chuỗi:

Tìm phần tử thứ 2 của chuỗi:

Cách khác  :

Chèn 1 ký tự vào vị trí thứ 2 của chuỗi:

Đặc tả đệ quy

• Đặc tả đệ quy thực chất là cách thức đặc tả hàm theo dạng truy hồi.
• Một đặc tả được gọi là đệ quy nếu trong phần biểu thức Where của hàm có sử dụng đến chính bản thân hàm đang được đặc tả.

Ví dụ 1: Ta xét hàm tìm kích thước của một chuỗi ký tự bất kỳ:

Ví dụ 2: Xét hàm tính tổng các phần tử trong mảng a, kích thước n
MANG = Zn

Ví dụ 3: Xét hàm đếm số lần xuất hiện của 1 số nguyên x trong mảng a, kích thước n

Ví dụ 4: Xét hàm kiểm tra mảng tăng dần

Bài tập áp dụng
1. Đặc tả các hàm tính toán sau:

• Tìm n!
• Tìm A(k,n) – chỉnh hợp chập k
• Tìm C(k,n) – Tổ hợp chập k
• Tìm USCLN của 2 số nguyên dương a, b
• Tìm phần tử thứ n trong dãy Fibonacci:

F(n) = 1 nếu n<=2
F(n) = F(n-1) + F(n-2) nếu n>2

2. Đặc tả các hàm sau trên dữ liệu kiểu chuỗi:

• Xác định phần tử thứ k của chuỗi
• Tìm xem ký tự c có hay không có trong chuỗi
• Đếm số lần xuất hiện của ký tự c trong chuỗi
• Xóa k ký tự đầu của chuỗi
• Xóa phần tử thứ k của chuỗi

3. Cho mảng a gồm toàn các số nguyên, kích thước n (n0). Hãy đặc tả các hàm sau:

• Tìm giá trị lớn nhất, nhỏ nhất trong mảng
• Tính tổng các số chẵn có trong mảng
• Kiểm tra xem mảng có gồm toàn các số dương hay không
• Kiểm tra mảng có gồm các số dương và số âm xen kẽ nhau hay không
• Đếm số run của mảng

Đặc tả các quy tắc tính toán

• Trong quá trình xây dựng các hệ thống phần mềm, đặc biệt là các hệ thống quản lý luôn có 1 yêu cầu không thể thiếu là thực hiện việc tính toán theo 1 hoặc 1 số quy tắc nhất định nào đó
• Do vậy, việc đặc tả các quy tắc này là cần thiết, để nhằm đảm bảo cho việc tính toán được chính xác và đầy đủ

Nguyên tắc chung khi đặc tả các quy tắc tính toán :

1. Đặt tên cho các đại lượng có liên quan đến quá trình tính toán
2. Xác định kiểu dữ liệu của các đại lượng này
3. Đặc tả hàm tính toán cho từng quy tắc

Ta xét phần mềm quản lý thư viện với yêu cầu tính toán tiền phạt cho mỗi quyển sách khi trả sách trễ hạn với các yêu cầu khác nhau có thể có như sau :

1. Mỗi ngày trả trễ phạt 1000đ.
2. Mỗi ngày trả trễ phạt 1000đ, nhưng từ ngày trễ thứ 5 trở đi thì phạt 2000đ/ngày.
3. Có 2 loại sách A và B. Hình thức phạt như câu 2), nhưng mức phạt khác nhau cho mỗi loại sách :

• Loại A : 1000đ và 2000đ
• Loại B : 1500đ và 2500đ

Giải:
Gọi:

• t : số tiền phạt (t Î N)
• n: số ngày trả trễ hạn (n Î N)
• l: loại sách (l Î {A, B})

Câu 1:

Câu 2:

Câu 3:

Đặc tả các sơ đồ trạng thái

• Một sơ đồ trạng thái thường dùng các hình vẽ để mô tả trạng thái và hoạt động của một đối tượng, 1 quá trình nào đó.
• Tuy nhiên, việc sử dụng hình vẽ khi xử lý trên máy tính lại tỏ ra hết sức khó khăn, độ chính xác lại không cao.

Ví dụ: sơ đồ hoạt động của 1 thang máy

Nguyên tắc chung khi đặc tả 1 sơ đồ trạng thái :
1. Gán các giá trị 1, 2, 3, … cho các trạng thái có trong sơ đồ
2. Gọi  

•  t1 : trạng thái hiện hành (t1ÎN)
• t2 : trạng thái có thể chuyển đến trực tiếp từ t1 (t2ÎN)

3. Xây dựng các ràng buộc trên t1 và t2 dưới dạng một mệnh đề để mô tả các tình trạng có thể có của sơ đồ.

Để đặc tả sơ đồ hoạt động của thang máy trong ví dụ trên, ta đặt :

• 1 : Đi lên
• 2 : Dừng
• 3 : Đi xuống
• t1 : trạng thái hiện hành
• t2 : trạng thái có thể chuyển đến từ t1

Ta có đặc tả :

Ví dụ 2: Trạng thái 1 quyển sách

Các đối tượng hình học

Một điểm trên mặt phẳng được biểu diễn dưới dạng (x, y) trong đó x và y là 2 số thực biểu diễn hoành độ và tung độ của điểm đó. Ta định nghĩa kiểu dữ liệu :

Đặc tả 1 đối tượng hình học trên mặt phẳng là đặc tả hàm kiểm tra các điểm có liên quan có thỏa các điều kiện ràng buộc để tạo nên đối tượng hay không.

Dạng thức chung :

Cho A, B, C, D là các điểm trong mặt phẳng. Đặc tả các phát biểu sau :

1. A, B là 2 điểm trùng nhau
2. A, B, C là 3 điểm thẳng hàng
3. A, B, C là 3 đỉnh của 1 tam giác
4. C là trung điểm của AB
5. AB // CD
6. AB  ^ CD
7. Hàm tính độ dài của đoạn thẳng AB
8. Hàm tính khoảng cách từ điểm A đến đường thẳng qua BC

Câu a:

Câu b:
 

Câu c:

Đặc tả các ràng buộc
Bao gồm 2 dạng ràng buộc chính:

1. Ràng buộc trên kiểu dữ liệu
2. Ràng buộc trên sơ đồ logic

Ràng buộc trên kiểu dữ liệu

• Gọi T là tập hợp nền của kiểu dữ liệu T
• Ràng buộc trên kiểu dữ liệu T là hàm kiểm tra tính hợp lệ :

Ví dụ :
Kiểu dữ liệu NGAY, biểu diễn một (ngày, tháng, năm). Kiểu có thể có các tập hợp nền như sau:

Trước tiên, ta đặc tả hàm kiểm tra năm nhuận :

Đặc tả hàm kiểm tra ngày hợp lệ:

Ràng buộc trên sơ đồ logic

1. Các ràng buộc trên sơ đồ logic chính là các ràng buộc toàn vẹn (RBTV) trong cơ sở dữ liệu
2. Khi xác định 1 RBTV cần chỉ rõ:

• Điều kiện của RBTV
• Bối cảnh xảy ra
• Tầm ảnh hưởng
• Hành động cần phải có

Các kiểu RBTV:

• Các ràng buộc khóa nội, khóa ngoại
• Ràng buộc miền giá trị
• Ràng buộc thời điểm
• Ràng buộc liên thuộc tính
• Ràng buộc liên bộ
• Ràng buộc liên quan hệ
• v.v...

Ví dụ 1 : Xét phần mềm quản lý thư viện với sơ đồ logic như sau:

Độc giả (MĐG, MLĐG, Họtên, Địachỉ, Điệnthoại)
Loại ĐG (MLĐG, Tên, Ghichú)
Thể loại (MTL, Tên, Ghichú)
Sách (MS, MTL, Tên, NămXB, Tácgiả)
Mượn (MMượn, MĐG, Ngàymượn,Số sách)
CTMượn (MMượn, MS, Ngàytrả)

Hãy đặc tả các ràng buộc sau :
1. Ràng buộc về khóa nội, khóa ngoại

• MĐG là duy nhất trong Độc giả
• MTL của Sách phải có trong Thể loại

2. Ràng buộc miền giá trị :

• Ngày mượn phải khác rỗng
• Số sách phải lớn hơn 0

3. Ràng buộc liên quan hệ :

• Ngày trả sau ngày mượn
• Số sách trong mỗi hóa đơn phải bằng số bộ có cùng mã HĐ trong CTMượn

4. Ràng buộc thời điểm :

• Tại 1 thời điểm, sách chỉ có thể cho 1 độc giả mượn

Ví dụ 2 : Xét phần mềm quản lý giải bóng đá như sau:

Đội bóng (MĐB, TênĐB, Quốcgia, HLV)
Trậnđấu (MTĐ, Sân,Tỉsố)
Thamgia (MTĐ,MĐB,Lượt)
Trọngtài (MTT, TênTT, Quốctịch)
Điềukhiển (MTĐ, MaTT, Vaitrò)

Hãy đặc tả các ràng buộc sau :

• Các trọng tài trong cùng 1 trận đấu phải cùng thuộc 1 quốc gia
• Trong 1 trận đấu chỉ có 1 trọng tài chính
• Trọng tài và các đội thi đấu không cùng thuộc 1 quốc gia
• Mội trận đấu chỉ có 2 đội tham gia

Tóm tắt chương

• Kiểu dữ liệu bao gồm:

1. Tập các giá trị
2. Các phép toán cơ sở

• Đặc tả hàm: chỉ ra tập nguồn, tập đích, miền xác định và miền giá trị của hàm.
• Đặc tả đệ quy là những đặc tả hàm mà trong mệnh đề Where có lời gọi đến chính hàm đang đặc tả.
• Đặc tả quy tắc tính toán thường được sử dụng trong quá trình xây dựng các hệ thống quản lý, bản chất của nó cũng là đặc tả hàm.
• Đặc tả 1 sơ đồ trạng thái là mô tả những sự chuyển trạng thái hợp lệ trong sơ đồ đó
• Đặc tả 1 đối tượng hình học là đặc tả hàm kiểm tra các điểm liên quan có thỏa các điều kiện ràng buộc để tạo nên đối tượng hay không.

Bài tập
(xem trong phần tài liệu các bài tập lý thuyết)

HẾT CHƯƠNG 3
(còn tiếp…)