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

Bài giảng Đặc tả hình thức: Chương 4 Số và kiểu mảng, cung cấp cho người đọc những kiến thức như: Số và mảng; ngôn ngữ Z mô tả các dạng số; các hàm và thao tác trên mảng/chuỗi. Mời các bạn cùng tham khảo!
Nội dung trích xuất từ tài liệu:
Bài giảng Đặc tả hình thức: Chương 4 - 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 4 Số và Kiểu mảng Giảng viên: PGS. TS. Vũ Thanh Nguyên 1 Nội Dung Số và mảng là khái niệm quan trọng của Đặc tả hình thức Ngôn ngữ Z mô tả các dạng số - đặc biệt là số tự nhiên dùng tương ứng với mảng 2 Kiểu Số Tập số nguyên Z = {…, -2,-1,0,1,2,…} Tập số tự nhiên N = {n:Z|n0} = {0,1,2,…}  Các phép toán trên số 3 Kiểu Số  Các phép toán trên số 4 Kiểu Số  Các phép toán trên số 5 Kiểu Số  Ví dụ về hàm trả lại giá trị tuyệt đối của một số nguyên sử dụng sự miêu tả rỏ ràng như sau:  abs Z Z n:Z  n  0  abs n = -n  n  0  abs n = n  Hàm successor (succ) trả lại giá trị của số tiếp theo của số tự nhiên  Succ = { 0 ↦ 1, 1 ↦ 2, 2 ↦ 3,…}  Hàm predecessor (pred) trả lại giá trị của số phía trước  pred == succ∼ 6 Kiểu Số  Miền xác định của số  Miền xác định giữa 2 số a, b: Z được xác định như sau: a..b = {a, a+1, a+2,…, b-2, b-1, b} Hoặc a..b = {n:Z| a n b} Nếu a > b khi đó a..b = ∅ và a..a = {a} 7 Kiểu Số  Cardinality  Số phần tử của tập (số nguyên)  Xác định là card hay # (ngôn ngữ z)  Ví dụ: #∅ = 0, #{a} = 1  Đối với miền xác định a..b #a..b = 1+b-a nếu a  b = 0 nếu a > b #a..b = max {0, 1+b-a} Vậy nó tương ứng là 1 2 3 … b-a 1+b-a ↧ ↧ ↧ … ↧ ↧ a a+1 a+2 … b-1 b 8 Kiểu mảng  Mảng (sequence):  Gồm hữu hạn phần tử (0 hay nhiều phần tử)  Có thứ tự  Một phần tử có thể xuất hiện nhiều lần trong mảng  Có cùng kiểu dữ liệu 9 Kiểu mảng  Mảng:  Mảng chỉ chứa một phần tử s = {1 ↦ x} có #s=1 và được viết là [x] còn gọi là mảng đơn  Tổng quát một mảng {1 ↦ x1, 2 ↦ x2, …,n ↦ xn} được viết ngắn gọn [x1, x2,…,xn]  Ví dụ: [4, 2, 7, 1, 5, 6, 3] [7, 2, 1, 4, 3, 6, 5] [‘C’, ‘O’, ‘N’] [42.0, 343.0, 42.0] [] (không giống tập mảng rổng xác định một kiểu dữ liệu) 10 Mảng  Cho trước kiểu T  Định nghĩa kiểu mảng mà mỗi phần tử thuộc kiểu T T*  Ví dụ: Word = Char* Smallstring = {‘a’, ‘b’, ‘c’}* Smallstring = { [], [‘a’], [‘b’], [‘c’], [‘a’, ‘a’], [‘a’, ‘b’], …, [‘a’,’a’, ‘c’], … } Paragraph = Word* Chapter = Paragraph* 11 Chuỗi  Chuỗi có thể xem là 1 mảng các ký tự  Ví dụ: [‘D’, ‘i’, ‘s’, ‘k’, ‘ ‘, ‘f’, ‘u’, ‘l’, ‘l’] “Disk full”  Lưu ý: ‘a’  Char “hello”  Char* “a”  Char* 12 Các hàm và thao tác trên mảng/chuỗi  Hàm len len [] = 0 len [1, 2, 3, 4, 1] = 5 Tổng quan len s = card dom s  Một số ví dụ về mảng  [a,b]  [b,a]  [a,b]  [a,b,b]  Giả sử s1= [b,b,c] s2= [a] Khi đó len s1= 3, len s2= 1 13 Các hàm và thao tác trên mảng/chuỗi  Truy xuất phần tử trong mảng theo chỉ số (tính từ 1) sq = [2, 19, 13, 5, 17] sq(1) = 2 sq(4) = 5 Tổng quát s  X*  1  i  len s  s(i)  X  s1(1) = s1(2) = b 14 Các hàm và thao tác trên mảng/chuỗi  Mảng/chuỗi con [‘a’, ‘a’, ‘d’, ‘c’, ‘a’, ‘b’] (2, …, 4) = [‘a’, ‘d’, ‘c’] “Hello” (2, …, 2) = “e” s(1,…, len s) = s 15 Các hàm và thao tác trên mảng/chuỗi  Phép nối ⃕  s ⃕ t  Ví dụ: “Hello” ⃕ “ ” ⃕ “World” = “Hello World”  Cập nhật phần tử trong mảng †  Ví dụ: [1, 2, 3, 4] (3) †11 = [1, 2, 11, 4]  Một số quy tắc  []⃕s=s⃕[]=s  r⃕(s⃕t) = (r⃕s)⃕t  (r⃕s = r⃕t)  s = t  Lưu ý * *  Nếu s,tT , st  r:T  s⃕r = t 16 Các hàm và thao tác trên mảng/chuỗi  Lưu ý (ứng dụng cho tiếp đầu ngữ (prefix) của mảng):  (st  ts)  s = t  (rs  st)  rt  (rt  st)  (rs  sr) 17 Các hàm và thao tác trên mảng/chuỗi  Phép toán phân bố (ngôn ngữ Z)  ⃕/[] = []  ⃕/[a,b,…,n] = a⃕b⃕ … ⃕n  ⃕/([a]⃕s) = [a]⃕(⃕/s)  ⃕/(s⃕[a]) = (⃕/s)⃕[a] 18 Các hàm và thao tác trên mảng/chuỗi  Hàm Head (hd) và Tail (tl)  Ví dụ: hd [‘p’, ‘q’, ‘r’] = ‘p’  Hàm head của một mảng không rổng có thể định nghĩa như sau: hd (s: X*) r:X pre s[] post r = s(1) 19 Các hàm và thao tác trên mảng/chuỗi  Hàm tail của một mảng không rổng có thể định nghĩa như sau: tl (s: X*) rs:X pre s[] post s = [hd s] ...