05.DacTaHam Dac Ta Hinh Thuc

11/20/2014
TS. Vũ Thanh Nguyên
1
Chương 5: Đặc tả hàm
TS. Vũ Thanh Nguyên
Trường Đại học Công Nghệ Thông Tin, ĐHQG-HCM
Khoa Công Nghệ Phần Mềm
11/20/2014
TS. Vũ Thanh Nguyên
2
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
11/20/2014
TS. Vũ Thanh Nguyên
3
Tổng Quan Về Hàm
Hàm là một khái niệm trừu tượng toán học: là ánh xạ giữa hai tập giá trị.
function_name: domain → range, ở đó
function_name: tên của hàm
domain: miền xác định của tập giá trị mà ở đó hàm có thể ứng dụng
range: phạm vi xác định của tập giá trị mà ở đó hàm chứa đựng kết quả của ứng dụng hàm.
giữa domain và range cách nhau bằng →
Nếu miền xác định có từ 2 giá trị trở lên, cần dùng dấu
gcd: N1xN1 → N1

11/20/2014
TS. Vũ Thanh Nguyên
4
Tổng Quan Về Hàm
Định nghĩa hàm.
Hàm có thể được định nghĩa nhờ vào các phép toán và hằng số
Ví dụ:
Hàm định nghĩa trực tiếp (tường minh) của bình phương
square: Z → N
square(i) ≜ i*i
Hàm xác định giá trị tuyệt đối
abs: Z → N
abs(i) ≜ if i<0 then –i else i

11/20/2014
TS. Vũ Thanh Nguyên
5
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)
11/20/2014
TS. Vũ Thanh Nguyên
6
Tổng Quan Về Hàm
Hàm ước số chung của 2 số
is-common-divisor: NNN1 → B
is-common-divisor(i,j,d) ≜ d divides i  d divides j

Hàm xác định giá trị nhỏ hơn 3
less-than-three: N → B
less-than-three(i) ≜ i<3


11/20/2014
TS. Vũ Thanh Nguyên
7
Tổng Quan Về Hàm
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)
11/20/2014
TS. Vũ Thanh Nguyên
8
Các phép tổng quát trên ngôn ngữ VDM
11/20/2014
TS. Vũ Thanh Nguyên
9
Đặc tả hàm
Ví dụ:
Hàm luỹ thừa có thể được xác định bằng phương pháp tường minh bằng hàm exponent_x như sau:
exponent_x: ZN→Z
exponent_x(x,n) ≜
if n=0
then 1
else xexponent_x(x,n-1)

11/20/2014
TS. Vũ Thanh Nguyên
10
Đặc tả hàm
Ví dụ:
Hàm luỹ thừa củng có thể được xác định bằng phương pháp không tường minh như sau:
EXPONENT(x:Z, n:N)y:Z
pre true
post y=xn
11/20/2014
TS. Vũ Thanh Nguyên
11
Đặ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

11/20/2014
TS. Vũ Thanh Nguyên
12
Đặc tả hàm không tường minh
Định nghĩa tên hàm, tên và kiểu của các tham số đầu vào, tên và kiểu của kết quả trả về (tham số đầu ra)
Vị từ Pre-condition và Post-condition là biểu thức điều kiện logic, có thể có giá trị là true hoặc false.
Biểu thức điều kiện có thể chứa một hoặc nhiều vị từ. Các từ được liên kết bởi các phép liên kết logic, lượng từ và có thể chứa đựng hàm, tham số, hằng số và biến
Xác định Vị từ Pre-condition để phát biểu điều kiện về giá trị của các tham số đầu vào
Xác định Vị từ Post-condition để phát biểu mối quan hệ giữa các tham số đầu vào với kết quả trả về của hàm
11/20/2014
TS. Vũ Thanh Nguyên
13
Đặc tả hàm không tường minh
Các phép liên kết logic của vị từ Pre-condition và Post-condition
 - 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
11/20/2014
TS. Vũ Thanh Nguyên
14
Đặ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 thông tin sẽ trả về (Chương 6)
Giải pháp khác???
11/20/2014
TS. Vũ Thanh Nguyên
15
Đặc tả hàm không tường minh
Hàm được gọi là không tường minh vì vị từ post-condition không có sự giải thích cách thực hiện thuật toán  không thể tự động tính được giá trị đầu ra từ vị từ post-condition đối với các giá trị đầu vào được cho.
11/20/2014
TS. Vũ Thanh Nguyên
16
Đặ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ừ pre-condition
Ít xem xét tới đặc tả thuật toán
Dự kiến cho tên của kết quả
11/20/2014
TS. Vũ Thanh Nguyên
17
Đặc tả hàm không tường minh
Ví dụ:
max_of_set (s: ℕ-set) r: ℕ
pre s  {}
post (r  s)  (n  s  n  r)

Ví dụ:
abs (z: ℤ) r: ℕ
pre true
post ((r = z)  (z  0))
 ((r = -z)  (z < 0))
11/20/2014
TS. Vũ Thanh Nguyên
18
Đặc tả hàm không tường minh
Ví dụ: hàm tính ước số chung lớn nhất bằng phương pháp không tường minh sử dụng lượng từ như sau:
gcd (i:N1, j:N1) r:N1
pre true
post is-common-divisor (i,j,r) 
¬ sN1  is-common-divisor (i,j,s)  s>r
11/20/2014
TS. Vũ Thanh Nguyên
19
Đặ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)  (m11/20/2014
TS. Vũ Thanh Nguyên
20
Đặc tả hàm không tường minh
Ví dụ: Hàm trả về vị trí xuất hiện đầu tiên của chuỗi pt trong chuỗi cx, hoặc trả về 0 nếu chuỗi pt không xuất hiện trong cx ?
Thảo luận:?
11/20/2014
TS. Vũ Thanh Nguyên
21
Đặc tả hàm không tường minh
Ví dụ: Hàm kiểm tra s có là chuỗi con của t hay không?
Phiên bản 1:
issubstr (s: String, t: String) r: B
pre
post ( (r = true)  ( p, f  String  t = p ⃕ s ⃕ f ) )
 ( (r = false)   ( p, f  String  t = p ⃕ s ⃕ f ) )

Phiên bản 1’:
issubstr (s: String, t: String) r: B
pre true
post r = ( p, f  String  t = p ⃕ s ⃕ f )
11/20/2014
TS. Vũ Thanh Nguyên
22
Đặ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)
11/20/2014
TS. Vũ Thanh Nguyên
23
Đặc tả hàm không tường minh
Ví dụ: Hàm trả về vị trí xuất hiện đầu tiên của chuỗi pt trong chuỗi cx, hoặc trả về 0 nếu chuỗi pt không xuất hiện trong cx
location (pt: String, cx: String) r: ℕ
pre pt  []  cx  []
post ( p  String  is-shortes-prefix(p, pt, cx)  r = (1 + len p))
 (r = 0)
11/20/2014
TS. Vũ Thanh Nguyên
24
Đặc tả hàm tường minh
Đặc tả hàm tường minh (explicit definition)
Đặc tả có sử dụng các cấu trúc điều khiển
Thể hiện cách cài đặt hàm
Lưu ý:
Trong đặc tả không tường minh, mọi giá trị thỏa Vị từ Post-condition đều có thể được chấp nhận là kết quả phù hợp của hàm.
Trong đặc tả tường minh xác định một giá trị cụ thể phù hợp với yêu cầu của hàm

11/20/2014
TS. Vũ Thanh Nguyên
25
Đặc tả hàm tường minh
function_name : input_type → output_type
function_name (input_parameter) ≜ expression
hay
tên-hàm : Tập-nguồn1  Tập-nguồn2 …  Tập-đích
tên-hàm (tham-số1, tham-số2, …) ≜ đặc-tả-dạng-giải-thuật

Ở đó chứa đựng tham số, hằng số, hàm, vị từ, hàm xác định bởi người sử dụng
11/20/2014
TS. Vũ Thanh Nguyên
26
Đặc tả hàm tường minh
Lưu ý:
Trong đặc tả dạng tường minh không đặt tên cho biến kết quả trả về.
Giá trị của kết quả trả về là giá trị được xác định thông qua đặc tả dạng giải thuật
Các tham số đầu vào (ở dòng 2 của đặc tả) có kiểu tương ứng với các tập nguồn ở dòng 1
Ví dụ:
add : ℝ  ℝ  ℝ
add (x, y) ≜ x  y
11/20/2014
TS. Vũ Thanh Nguyên
27
Mối Quan Hệ Giữa Hàm Tường Minh Và Không Tường Minh
11/20/2014
TS. Vũ Thanh Nguyên
28
Cấu trúc điều khiển if-then-else
Cú pháp:
if Biểu-thức-điều-kiện
then giá-trị1
else giá-trị2
Cấu trúc if-then-else có thể lồng nhau
11/20/2014
TS. Vũ Thanh Nguyên
29
Cấu trúc điều khiển if-then-else
Ví dụ: hàm tính giai thừa bằng phương pháp tường minh
factorial : N → N
factorial(n) ≜
if n ≥ 1
then n  factorial(n-1)
else 1
11/20/2014
TS. Vũ Thanh Nguyên
30
Cấu trúc điều khiển if-then-else
Ví dụ:


11/20/2014
TS. Vũ Thanh Nguyên
31
Cấu trúc cases
Cú pháp:
cases index:
( value1, value2  result1,
value3, value4, value5  result2,
…
valuen  resultm
)
11/20/2014
TS. Vũ Thanh Nguyên
32
Cấu trúc cases
Ví dụ: Hàm tính số ngày của 1 tháng trong năm không nhuận
số-ngày-trong-tháng: ℕ  ℕ
số-ngày-trong-tháng (th) ≜
cases index:
( 1, 3, 5, 7, 8, 10, 12  31,
4, 6, 9, 11  30,
2  28
)
11/20/2014
TS. Vũ Thanh Nguyên
33
Sử dụng hàm phụ
Ví dụ: Hàm tính số ngày của 1 tháng trong năm bất kỳ
số-ngày-trong-tháng: ℕ  ℕ  ℕ
số-ngày-trong-tháng (th, nm) ≜
cases index:
( 1, 3, 5, 7, 8, 10, 12  31,
4, 6, 9, 11  30,
2  if là-năm-nhuận(nm)
then 29
else 28
)
11/20/2014
TS. Vũ Thanh Nguyên
34
Sử dụng hàm phụ
Ví dụ: Đặc tả hàm dùng chuyển đổi từ nhiệt độ F (Farenheit) sang C (Celsius):
norm-temp : (Farenheit  Celsius)  Celsius
norm-temp (t) ≜ cases t of
mk-Farenheit(v)  mk-Celsius ((v-32)*5/9),
mk- Celsius(v)  t
end
11/20/2014
TS. Vũ Thanh Nguyên
35
Sử dụng hàm phụ
Ví dụ: Hàm tính USCLN của 2 số nguyên dương
uscln (x : ℕ1, y : ℕ1) r : ℕ1
pre
post là-usc (r, x, y)   n  ℕ1  ( là-usc (n, x, y)  n  r )

là-usc ( z: ℕ1, x : ℕ1, y : ℕ1) r : B
pre
post r = ( chia-hết (x, z)  chia-hết (y, z) )

chia-hết (x : ℕ1, y : ℕ1) r : B
pre
post r =  k ℕ1  x = y*k
11/20/2014
TS. Vũ Thanh Nguyên
36
Sử dụng hàm phụ
Ví dụ: Hàm tính USCLN của 2 số nguyên dương
uscln (x : ℕ1, y : ℕ1) r : ℕ1
pre
post là-usc (r, x, y)   n  ℕ1  ( là-usc (n, x, y)  n  r )

là-usc : ℕ1  ℕ1  ℕ1  B
là-usc (z, x, y) ≜
chia-hết (x, z)  chia-hết (y, z)

chia-hết : ℕ1  ℕ1  B
chia-hết ( x, y) ≜
 k ℕ1  x = y * k
11/20/2014
TS. Vũ Thanh Nguyên
37
Đặc tả đệ quy
Ví dụ: Đặc tả hàm tính độ dài mảng
11/20/2014
TS. Vũ Thanh Nguyên
38
Đặc tả đệ quy
Ví dụ: Đặc tả hàm trả về giá trị của phần tử lớn nhất trong mảng
maxnum (s: ℤ *) r: ℤ
pre s  []
post ( r  elems s )  (x  elems s  x  r )

maxnum (s: ℤ *) r: ℤ
pre s  []
post ( ( r = hd s)  (len s = 1) )
 ( ( r = hd s)  ( r  maxnum (tl s)) )
 ( ( r > hd s)  ( r = maxnum (tl s)) )
11/20/2014
TS. Vũ Thanh Nguyên
39
Đặc tả đệ quy
Ví dụ: Đặc tả hàm trả về giá trị của phần tử lớn nhất trong mảng
maxnum : ℤ*  ℤ
maxnum (s) ≜
if len s = 1
then hd s
else
if hd s  maxnum (tl s)
then hd s
else maxnum (tl s)
11/20/2014
TS. Vũ Thanh Nguyên
40
Khai báo biến tạm bằng let-in
Cú pháp 1:
let định danh (identifier) = Biểu-thức1 in Biểu-thức2
Ý nghĩa:
Xác định giá trị của Biểu-thức1 và gán vào “biến tạm” đinh danh
Thay thế những vị trí xuất hiện của định danh trong Biểu-thức2 bằng giá trị của biến tạm định danh
Ví dụ:
Cho biểu thức
cos (sin(x) – 1) / (sin(x) – 1)
Ta có thể đặt biến tạm y và viết lại như sau:
let y = sin(x) – 1 in cos (y) / y
11/20/2014
TS. Vũ Thanh Nguyên
41
Ký pháp let-in
Ví dụ: Đặc tả hàm tính giá trị tuyệt đối của tích 2 số nguyên như sau:
absprod : ℤ × ℤ  
absprod (i,j) ≜
let k = i*j in
if k<0 then –k else k
11/20/2014
TS. Vũ Thanh Nguyên
42
Ký pháp let-in
Ví dụ: Đặc tả hàm dùng để tính năm nhuận:
inv-Datec : Datec  B
inv-Datec (dt) ≜
is-leapyr(year(dt))  day(dt) ≤ 365
Đặc tả hàm dùng let:
inv-Datec : Datec  B
inv-Datec (dt) ≜
let mk-Datec(d,y) = dt in is-leapyr(y))  d ≤ 365
11/20/2014
TS. Vũ Thanh Nguyên
43
Ký pháp let-in
Ví dụ: Đặc tả hàm dùng chuyển đổi từ nhiệt độ F (Farenheit) sang C (Celsius):
norm-temp : (Farenheit  Celsius)  Celsius
norm-temp (t) ≜
if tFarenheit
then let mk-Farenheit(v) = t
in mk-Celsius ((v-32)*5/9)
else t

11/20/2014
TS. Vũ Thanh Nguyên
44
Ký pháp let-in
Ví dụ: Đặc tả hàm trả về giá trị của phần tử lớn nhất trong mảng
maxnum : ℤ*  ℤ
maxnum (s) ≜
if len s = 1
then hd s
else
let max-in-tail = maxnum (tl s) in
if hd s  max-in-tail
then hd s
else max-in-tail
11/20/2014
TS. Vũ Thanh Nguyên
45
Khai báo biến tạm bằng let-in
Cú pháp 2a:
let định danh  Biểu-thức-tập-hợp in Biểu-thức
Cú pháp 2b:
let định danh  Biểu-thức-tập-hợp s.t. Điều-kiện in Biểu-thức

Ý nghĩa:
Biến tạm định danh nhận giá trị của MỘT phần tử (thỏa Điều-kiện) trong Biểu-thức-tập-hợp
Thay thế những vị trí xuất hiện của định danh trong Biểu-thức bằng giá trị của biến tạm định danh
11/20/2014
TS. Vũ Thanh Nguyên
46
Khai báo biến tạm bằng let-in
Ví dụ: Đặc tả hàm tính tổng các phần tử trong 1 tập hợp
sumset : ℝ-set  ℝ
sumset (s) ≜
if s = {}
then 0
else
let x  s in
x + sum-set ( s – {x} )