Bài giảng Đặc tả hình thức Chương 5: PGS.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

Chương 5: Đặc tả hàm

23-02-2023

TS. Vũ Thanh Nguyên

Nội dung

23-02-2023

TS. Vũ Thanh Nguyên

 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

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, ở đó

 Nếu miền xác định có từ 2 giá trị trở lên, cần dùng dấu

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 →

23-02-2023

TS. Vũ Thanh Nguyên

gcd: N1xN1 → N1

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

23-02-2023

TS. Vũ Thanh Nguyên

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

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

23-02-2023

TS. Vũ Thanh Nguyên

Hàm xác định số lẻ is-odd: N → B is-odd(i) ≜ ¬is-even(i)

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

23-02-2023

TS. Vũ Thanh Nguyên

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

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

23-02-2023

TS. Vũ Thanh Nguyên

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

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

23-02-2023

TS. Vũ Thanh Nguyên

Đặc tả hàm

 Hàm luỹ thừa có thể được xác định bằng phương pháp

 Ví dụ:

tường minh bằng hàm exponent_x như sau: exponent_x: ZN→Z exponent_x(x,n) ≜ if n=0

23-02-2023

TS. Vũ Thanh Nguyên

then 1 else xexponent_x(x,n-1)

Đặc tả hàm

 Hàm luỹ thừa củng có thể được xác định bằng phương

 Ví dụ:

23-02-2023

TS. Vũ Thanh Nguyên

pháp không tường minh như sau: EXPONENT(x:Z, n:N)y:Z pre true post y=xn

Đặc tả hàm không tường minh

 Phát biểu trạng thái hệ thống trước và sau khi thực hiện

 Đặc tả hàm không tường minh (implicit definition):

 Không cần nêu ra các bước để thực hiện xử lý trong hàm

hàm

23-02-2023

TS. Vũ Thanh Nguyên

tên_hàm (thamsố1: Kiểu1, thamsố2: Kiểu2…) kq: Kiểukq Vị từ pre-condition pre post Vị từ post-condition

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

23-02-2023

TS. Vũ Thanh Nguyên

các tham số đầu vào với kết quả trả về của hàm

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

23-02-2023

TS. Vũ Thanh Nguyên

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

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

 Theo cấu trúc chuẩn của đặc tả hàm không tường minh:

 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???

23-02-2023

TS. Vũ Thanh Nguyên

thông tin?

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

23-02-2023

TS. Vũ Thanh Nguyên

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.

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

 Các ưu điểm của đặc tả hàm không tường minh

 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-

tâm

 Ít xem xét tới đặc tả thuật toán  Dự kiến cho tên của kết quả

23-02-2023

TS. Vũ Thanh Nguyên

condition

Đặc tả hàm không tường minh

(s: ℕ-set) r: ℕ

 Ví dụ: max_of_set s  {} pre (r  s) post  (n  s  n  r)

 Ví dụ: abs pre post

23-02-2023

TS. Vũ Thanh Nguyên

(z: ℤ) r: ℕ true ((r = z)  (z  0))  ((r = -z)  (z < 0))

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

23-02-2023

TS. Vũ Thanh Nguyên

¬ sN1  is-common-divisor (i,j,s)  s>r

Đặ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:ℕ x ≥ 1 pre (z2 ≤ x)  (x < (z+1)2) post

23-02-2023

TS. Vũ Thanh Nguyên

 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 post (x > 0)  (y > 0) dZ (y=dx+m)  (0≤m)  (m

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

23-02-2023

TS. Vũ Thanh Nguyên

 Thảo luận:?

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

true

23-02-2023

TS. Vũ Thanh Nguyên

Phiên bản 1’: issubstr (s: String, t: String) r: B pre post r = ( p, f  String  t = p ⃕ s ⃕ f )

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

23-02-2023

TS. Vũ Thanh Nguyên

is-prefix (p, s, t)  q  String  ( is-prefix (q, s, t)  len q  len p)

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

23-02-2023

TS. Vũ Thanh Nguyên

 (r = 0)

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

 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ù

 Lưu ý:

23-02-2023

TS. Vũ Thanh Nguyên

hợp với yêu cầu của hàm

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

23-02-2023

TS. Vũ Thanh Nguyên

Ở đó chứa đựng tham số, hằng số, hàm, vị từ, hàm xác định bởi người sử dụng

Đặc tả hàm tường minh

 Trong đặc tả dạng tường minh không đặt tên cho biến kết

 Lưu ý:

 Giá trị của kết quả trả về là giá trị được xác định thông qua

quả trả về.

 Các tham số đầu vào (ở dòng 2 của đặc tả) có kiểu tương

đặc tả dạng giải thuật

ứng với các tập nguồn ở dòng 1

23-02-2023

TS. Vũ Thanh Nguyên

 Ví dụ: add : ℝ  ℝ  ℝ add (x, y) ≜ x  y

Mối Quan Hệ Giữa Hàm Tường Minh Và Không Tường Minh

23-02-2023

TS. Vũ Thanh Nguyên

Cấu trúc điều khiển if-then-else

 Cú pháp:

if then else Biểu-thức-điều-kiện giá-trị1 giá-trị2

23-02-2023

TS. Vũ Thanh Nguyên

 Cấu trúc if-then-else có thể lồng nhau

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

23-02-2023

TS. Vũ Thanh Nguyên

factorial : N → N factorial(n) ≜ if n ≥ 1 then n  factorial(n-1) else 1

Cấu trúc điều khiển if-then-else

 Ví dụ:

Đặc tả dạng tường minh

(z: ℤ) r: ℕ

abs : ℤ  ℕ abs (z) ≜

Đặc tả dạng không tường minh abs pre post ((r = z)  (z  0)) if (z<0) then –z else

z  ((r = -z)  (z < 0))

(a: ℤ, b: ℤ) r: ℤ

max : ℤ  ℤ  ℤ max (a, b) ≜

max pre post ((r = a)  (a  b)) if (a  b) then a else

23-02-2023

TS. Vũ Thanh Nguyên

b  ((r = b)  (a < b))

Cấu trúc cases

 Cú pháp: cases index:

(

 result1, value1, value2 value3, value4, value5  result2, … valuen  resultm

23-02-2023

TS. Vũ Thanh Nguyên

)

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,  30, 4, 6, 9, 11  28 2

23-02-2023

TS. Vũ Thanh Nguyên

)

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,  30, 4, 6, 9, 11  if là-năm-nhuận(nm) 2

then 29 else 28

23-02-2023

TS. Vũ Thanh Nguyên

)

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

23-02-2023

TS. Vũ Thanh Nguyên

mk-Farenheit(v)  mk-Celsius ((v-32)*5/9), mk- Celsius(v)  t end

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) )

23-02-2023

TS. Vũ Thanh Nguyên

chia-hết (x : ℕ1, y : ℕ1) r : B pre post r =  k ℕ1  x = y*k

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) ≜

23-02-2023

TS. Vũ Thanh Nguyên

 k ℕ1  x = y * k

Đặc tả đệ quy

 Ví dụ: Đặc tả hàm tính độ dài mảng

Đặc tả dạng không tường minh Đặc tả dạng tường minh

(s: T*) r: ℕ

len: T *  ℕ len (s) ≜

len pre post ((r = 0)  (s =[]))

 ((r = 1+len( tl s))  (s 

23-02-2023

TS. Vũ Thanh Nguyên

[])) if s = [] then 0 else 1 + len (tl s)

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

r: ℤ

maxnum (s: ℤ *) s  [] pre ( r  elems s )  (x  elems s  x  r ) post

r: ℤ

23-02-2023

TS. Vũ Thanh Nguyên

maxnum (s: ℤ *) s  [] pre ( ( r = hd s)  (len s = 1) ) post ( ( r = hd s)  ( r  maxnum (tl s)) )  ( ( r > hd s)  ( r = maxnum (tl s)) ) 

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

23-02-2023

TS. Vũ Thanh Nguyên

if hd s  maxnum (tl s) then hd s else maxnum (tl s)

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

 Xác định giá trị của Biểu-thức1 và gán vào “biến tạm” đinh

 Ý nghĩa:

 Thay thế những vị trí xuất hiện của định danh trong Biểu-

danh

thức2 bằng giá trị của biến tạm định danh

 Cho biểu thức

 Ví dụ:

cos (sin(x) – 1) / (sin(x) – 1) Ta có thể đặt biến tạm y và viết lại như sau:

23-02-2023

TS. Vũ Thanh Nguyên

let y = sin(x) – 1 in cos (y) / y

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:

23-02-2023

TS. Vũ Thanh Nguyên

absprod : ℤ × ℤ   absprod (i,j) ≜ let k = i*j in if k<0 then –k else k

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) ≜

23-02-2023

TS. Vũ Thanh Nguyên

let mk-Datec(d,y) = dt in is-leapyr(y))  d ≤ 365

Ký pháp let-in

 Ví dụ: Đặc tả hàm dùng chuyển đổi từ nhiệt độ F (Farenheit)

23-02-2023

TS. Vũ Thanh Nguyên

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