Bài giảng Đặc tả hình thức Chương 4 của 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

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

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ố

Kiểu Số

 Các phép toán trên số

Kiểu Số

 Các phép toán trên số

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

 Hàm successor (succ) trả lại giá trị của số tiếp theo của số

n:Z  n  0  abs n = -n  n  0  abs n = 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∼

tự nhiên

Kiểu Số

 Miền xác định giữa 2 số a, b: Z được xác định như sau:

 Miền xác định của số

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}

Kiểu Số

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

 Cardinality

Vậy nó tương ứng là 1 2 3 … b-a 1+b-a ↧ ↧ ↧ … ↧ ↧ a a+1 a+2 … b-1 b

Kiểu mảng

 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

 Mảng (sequence):

Kiểu mảng

 Mảng chỉ chứa một phần tử s = {1 ↦ x} có #s=1 và được

 Mảng:

 Tổng quát một mảng

viết là [x] còn gọi là mảng đơn

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

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

 Ví dụ:

Word = Char* Smallstring = {‘a’, ‘b’, ‘c’}* Smallstring = { [], [‘a’], [‘b’], [‘c’], [‘a’, ‘a’], [‘a’, ‘b’], …,

[‘a’,’a’, ‘c’], … }

Paragraph = Word* Chapter = Paragraph*

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*

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

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

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

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”

 Ví dụ: [1, 2, 3, 4] (3) †11 = [1, 2, 11, 4]

 Cập nhật phần tử trong mảng †

 Một số quy tắc  []⃕s=s⃕[]=s  r⃕(s⃕t) = (r⃕s)⃕t  (r⃕s = r⃕t)  s = t

 Nếu s,tT*, st  r:T*  s⃕r = t

 Lưu ý

Các hàm và thao tác trên mảng/chuỗi

 (st  ts)  s = t  (rs  st)  rt  (rt  st)  (rs  sr)

 Lưu ý (ứng dụng cho tiếp đầu ngữ (prefix) của mảng):

Các hàm và thao tác trên mảng/chuỗi

 ⃕/[] = []  ⃕/[a,b,…,n] = a⃕b⃕ … ⃕n  ⃕/([a]⃕s) = [a]⃕(⃕/s)  ⃕/(s⃕[a]) = (⃕/s)⃕[a]

 Phép toán phân bố (ngôn ngữ Z)

Các hàm và thao tác trên mảng/chuỗi

 Ví dụ:

 Hàm Head (hd) và Tail (tl)

 Hàm head của một mảng không rổng có thể định nghĩa như

hd [‘p’, ‘q’, ‘r’] = ‘p’

sau: hd (s: X*) r:X pre s[] post r = s(1)

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:

 Ví dụ:

tl (s: X*) rs:X pre s[] post s = [hd s]⃕rs  Ví dụ tl [‘p’, ‘q’, ‘r’] tl [42] = [‘q’, ‘r’] = []

hd s1 = b hd s2 = a tl s1 = [b,c] tl s2 = []

Các hàm và thao tác trên mảng/chuỗi

 Chèn 1 phần tử vào đầu mảng (cons)  Ví dụ: cons (6, [2, 3]) = [6, 2, 3]

Các hàm và thao tác trên mảng/chuỗi

 Hàm inds: trả về tập chỉ số của các phần tử trong mảng

 Ví dụ: inds [12, 4, 6, 38, 12] = {1, 2, 3, 4, 5}  inds s = {1,…,len s}  inds s1 = {1,2,3}  inds s2 = {1}  inds [] = {}

inds s = {i | 1  i  len s}

Các hàm và thao tác trên mảng/chuỗi

 Hàm elems: trả về tập hợp các giá trị của các phần tử trong

mảng

 Ví dụ: elems [12, 4, 6, 12, 4, 6, 38, 12] = {4, 6, 12, 38}  elems s2 = {a}  elems s1 = {b,c}  elems [] = {}

elems s = {s(i) | i  inds s}

Các hàm và thao tác trên mảng/chuỗi

 sa = sb  len sa = len sb  iinds sa  sa (i) = sb (i)

 Hai mảng bằng nhau

 Hoặc dùng phép nối ⃕ (người ta thường dùng phép nối

 Các mảng có thể liên kết bởi hàm concat(sa:X* , sb:X*) rs:X* post len rs = len sa + len sb  (iinds sa  rs(i) = sa(i))  (iinds sb  rs(i+len sa) = sb(i))

sa⃕sb hơn là hàm concat(sa,sb).