Trường Đại học Công Nghệ Thông Tin, ĐHQG-HCM
Khoa Công Nghệ Phần Mềm

Chương 5: Đặc tả hàm
PGS.TS. Vũ Thanh Nguyên

PGS.TS. Vũ Thanh Nguyên

4/5/2019
CuuDuongThanCong.com

1
/>

Nội dung
 Tổng quan về hàm
 Đặc tả hàm không tường minh
 Đặc tả hàm tường minh
 Đặc tả đệ quy và sử dụng hàm phụ
 Một số cấu trúc điều khiển

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
2



Hàm xác định giá trị tuyệt đối
abs: Z → N
abs(i) ≜ if i
4


Tổng Quan Về Hàm
 Hàm chia hết
divides: N1 N → B
divides(i,j) ≜ j mod i = 0
Sử dụng toán tử dạng infix

i divides j

Hàm xác định số chẵn
is-even: N → B
is-even(i) ≜ 2 divides i
Hàm xác định số lẻ
is-odd: N → B
is-odd(i) ≜ ¬is-even(i)
4/5/2019


 Hàm xác định số nguyên tố
is-prime: N → B
is-prime(i) ≜ i 1
d N1 d divides i

d=1

d=i

hoặc có thể định nghĩa
is-prime(i) ≜ i 1
d {2,…,i-1} ¬(d divides i)

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
7


Các phép tổng quát trên ngôn ngữ VDM

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

pre true
post y=xn

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
10


Đặc tả hàm không tường minh
 Đặc tả hàm không tường minh (implicit definition):
 Đặc tả hàm không tường minh mô tả cái được tính toán
thay vì định nghĩa trực tiếp vấn đề, chúng ta không phải chỉ
ra kết quả được tính toán như thế nào.
 Có nhiều nguyên nhân để chúng ta phải đặc tả không tường
minh. Có lẽ nguyên nhân rõ ràng nhất là đặc tả thưởng
ngắn gọn hơn so với định nghĩa cụ thể.
 Đặc tả không tường minh thường có ý nghĩa chính xác với
bài toán mong muốn hơn so với đặc tả tường minh (hay cài
đặt).

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

 Đặc tả không tường minh phải thỏa toàn bộ các tính chất
mà người dùng mong muốn trả về kết quả đúng nhất từ đặc
tả.

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
13


Đặc tả hàm không tường minh
 Đặc tả hàm không tường minh (implicit definition):
 Phát biểu trạng thái hệ thống trước và sau khi thực hiện
hàm
 Không cần nêu ra các bước để thực hiện xử lý trong hàm
tên_hàm (thamsố1: Kiểu1, thamsố2: Kiểu2…) kq: Kiểukq
pre
Vị từ pre-condition
post Vị từ post-condition

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên


- và

- hoặc

- nếu và chỉ nếu (if and only if)

- kéo theo

- với mọi

- tồn tại
 ¬ - nó không phải là trường hợp

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
16


Đặc tả hàm không tường minh
 Theo cấu trúc chuẩn của đặc tả hàm không tường minh:
 Mỗi hàm có tối đa 1 kết quả trả về
 Các tham số đầu vào đều là dạng read-only (tham trị)
 Vấn đề: Làm cách nào đặc tả hàm cần trả về nhiều nội dung
thông tin?
 Giải pháp: Định nghĩa kiểu cấu trúc để chứa tất cả các thành phần

Đặc tả hàm không tường minh
 Các ưu điểm của đặc tả hàm không tường minh
 Sự miêu tả trực tiếp các tính chất mà người sử dụng quan
tâm
 Mô tả một tập các kết quả có thể bởi vị từ post-condition
 Giá trị tường minh (giá trị true hoặc false) của vị từ precondition
 Ít xem xét tới đặc tả thuật toán
 Dự kiến cho tên của kết quả

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
19


Đặc tả hàm không tường minh
 Ví dụ:
max_of_set (s: ℕ-set)
pre
s {}
post (r s)
( n

r: ℕ
s n


CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
21


Đặc tả hàm không tường minh
 Ví dụ: tính căn bật hai của một số nguyên
int_sqr (x: ℕ) z:ℕ
pre
x≥1
post

(z2 ≤ x)

(x < (z+1)2)

 Ví dụ: hàm trả lại số dư của số nguyên y chia cho số nguyên x
mod (x,y:N)m:ℕ
pre
(x > 0) (y > 0)
post
d Z (y=d x+m) (0≤m) (m
Phiên bản 1’:
issubstr (s: String, t: String) r: B
pre
true
post
r = ( p, f String t = p ⃕ s ⃕ f )
4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
24


Đặc tả hàm không tường minh
 Ví dụ: Hàm kiểm tra chuỗi p có phải là prefix của chuỗi s
trong chuỗi t hay không?
is-prefix (p: String, s: String, t: String) r: B
pre
post r = ( f String t = p ⃕ s ⃕ f )

 Ví dụ: Hàm kiểm tra chuỗi p có phải là prefix ngắn nhất của
chuỗi s trong chuỗi t hay không?
is-shortest-prefix (p: String, s: String, t: String) r: B
pre
post is-prefix (p, s, t)
q String ( is-prefix (q, s, t) len q len p)
4/5/2019