Bài giảng Đặc tả hình thức - Chương 5: Đặc tả hàm - Vũ Thanh Nguyên

4/5/2019 PGS.TS. Vũ Thanh Nguyên 1 Chương 5: Đặc tả hàm 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.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) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.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) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 8 Các phép tổng quát trên ngôn ngữ VDM CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.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) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.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):  Đặ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). CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 12 Đặc tả hàm không tường minh  Đặc tả hàm không tường minh (implicit definition):  Vấn đề ý nghĩa nhất là có một đặc tả bao trùm từ cài ngắn gọn nhất đến cái được đem mô tả để cài đặt.  Toàn bộ miền này trở nên rõ ràng hơn khi đối tượng dữ liệu được áp dụng trong đặc tả.  Một trong những thuận lợi của tìm kiếm một đặc tả là nó có thể mô tả đầy đủ miền giá trị bao trùm cho cài đặt.  Đặc tả không tường minh là cách lưu trữ lại yêu cầu chức năng mà không cần bận tâm đến phương thức cụ thể của tính toán. Tính chất khác của đặc tả là nó có thể mô tả các thuộc tính của kết quả cần thiết sao cho người dùng dễ hiểu nhất. CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 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):  Đặ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ả. CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 14 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 15 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 16 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 17 Đặ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??? CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 18 Đặ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. CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 19 Đặ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ả CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 20 Đặ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)) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 21 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 22 Đặ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<x) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.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 ?  Thảo luận:? CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 24 Đặ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 ) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 25 Đặ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) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 26 Đặ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) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 27 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 28 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 29 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 30 Mối Quan Hệ Giữa Hàm Tường Minh Và Không Tường Minh CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 31 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 32 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 33 Cấu trúc điều khiển if-then-else  Ví dụ: Đặc tả dạng không tường minh Đặc tả dạng tường minh abs (z: ℤ) r: ℕ pre post ((r = z) (z 0)) ((r = -z) (z < 0)) abs : ℤ ℕ abs (z) ≜ if (z<0) then –z else z max (a: ℤ, b: ℤ) r: ℤ pre post ((r = a) (a b)) ((r = b) (a < b)) max : ℤ ℤ ℤ max (a, b) ≜ if (a b) then a else b CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 34 Cấu trúc cases  Cú pháp: cases index: ( value1, value2 result1, value3, value4, value5 result2, valuen resultm )  Cấu trúc case được sử dụng khi chúng ta cấn xét nhiều trường hợp mà viết đặc tả ngắn gọn hơn thay vì sử dụng cấu trúc if- then-else. CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 35 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 th: ( 1, 3, 5, 7, 8, 10, 12 31, 4, 6, 9, 11 30, 2 28 ) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 36 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 th: ( 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 ) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 37 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 38 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 39 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 40 Đặc tả đệ quy  Đối với đặc tả hàm tường minh thì kỹ thuật đặc tả đệ quy cũng được áp dụng. Đối với kỹ thuật này chúng ta cần xác định được điều kiện dừng cho hàm cục bộ. Kỹ thuật này cũng được áp dụng đối với đặc tả hàm không tường minh. CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 41 Đặ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 len (s: T*) r: ℕ pre post ((r = 0) (s =[])) ((r = 1+len( tl s)) (s [])) len: T * ℕ len (s) ≜ if s = [] then 0 else 1 + len (tl s) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 42 Đặ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)) ) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 43 Đặ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) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 44 Khai báo biến tạm bằng let-in  Trong quá trình đặc tả các hàm cục bộ, chúng ta có thể sử dụng giá trị của một biểu thức lặp đi lặp lại nhiều lần. Trong đặc tả hàm đa số các ngôn ngữ đều hỗ trợ ký pháp let in để đặc tả một biến tạm và biến này được xem như là một định danh để thay thế giá trị của biểu thức được sử dụng trong hàm cục bộ. CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 45 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 46 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 47 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 48 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 49 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 50 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 51 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} ) CuuDuongThanCong.com https://fb.com/tailieudientucntt