Chương 4 Số và Kiểu mảng

Giảng viên: PGS. TS. Vũ Thanh Nguyên

Nội Dung

v

Số và mảng là khái niệm quan trọng của Đặc tả hình thức

v

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ố

v

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,…}

v

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

Kiểu Số

v

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

Kiểu Số

v

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

Kiểu Số

v

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

Kiểu Số

v

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}

Kiểu Số

v

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

Kiểu mảng

v

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

Kiểu mảng

v

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

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

v

Cho trước kiểu

T

v

Định nghĩa kiểu mảng mà mỗi phần tử thuộc kiểu

T

T*

v

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

v

Chuỗi có thể xem là 1 mảng các ký tự

v

Ví dụ:

[‘D’, ‘i’, ‘s’, ‘k’, ‘ ‘, ‘f’, ‘u’, ‘l’, ‘l’]

“Disk full”

v

Lưu ý:

‘a’

Î

Char

“hello”

Char

*

“a”

Char

*

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

v

Hàm len

len

[] = 0

len

[1, 2, 3, 4, 1] = 5

Tổng quan

len s = card dom s

v

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

v

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

Î

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

v

Mảng/chuỗi con

[‘a’, ‘a’, ‘d’, ‘c’, ‘a’, ‘b’]

(2, …, 4)

= [‘a’, ‘d’, ‘c’]

“Hello”

(2, …, 2)

= “e”

(1,…,

len

= s

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

v

Phép nối

⃕

⃕

Ví dụ: “Hello”

⃕

“ ”

⃕

“World” = “Hello World”

v

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

†

Ví dụ:

[1, 2,

3

, 4] (3)

†

11 = [1, 2,

11

, 4]

v

Một số quy tắc

[]

⃕

s=s

⃕

[]=s

⃕

⃕

t) = (r

⃕

⃕

⃕

s = r

⃕

Þ

s = t

v

Lưu ý

Nếu s,tT*, st r:T* s

⃕

r = t

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

v

L

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

Í

Ù

Í

Þ

s = t

Í

Ù

Í

Þ

Í

Í

Ù

Í

Þ

Í

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

v

Ph

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

⃕

[] = []

⃕

[a,b,…,n] = a

⃕

⃕

…

⃕

⃕

[a]

⃕

s) = [a]

⃕

⃕

⃕

⃕

[a]) = (

⃕

⃕

[a]

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

v

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

¹

[]

post r = s(1)

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

v

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

¹

[]

post s = [hd s]

⃕

Ví dụ

tl

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

= [‘q’, ‘r’]

tl

[42]

= []

Ví dụ:

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

v

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

v

Hàm

inds

:

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

inds

s = {i | 1

£

len

s}

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

[] = {}

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

v

Hàm

elems

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

elems

s = {s(i) | i

inds

s}

Ví dụ:

elems

[12, 4, 6, 12, 4, 6, 38, 12] = {4, 6, 12, 38}

elems

s2 = {a}

elems

s1 = {b,c}

elems

[] = {}

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

v

Hai mảng bằng nhau

sa = sb

Û

len sa = len sb

Ù

iinds sa

·

sa (i) = sb (i)

v

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

Ù

(iinds sa

·

rs(i) = sa(i))

Ù

"

iinds sb

·

rs(i+len sa) = sb(i))

Hoặc dùng phép nối

⃕

ười ta thường dùng phép nối sa

⃕

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

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

v

Các mảng có thể liên kết nhờ phép liên kết phân bố tất cả các mảng trong một mảng bởi hàm đệ quy sau

:

dconc

: (X*)* → X*

Dconc

≜

if ss = [] then [] else (hd ss)

⃕

dconc

(tl ss)

V

í dụ:

dconc

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

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

v

Xác định độ dài của mảng con của mảng đã cho có kích thước từ i tới j

subseq(s:X*, i:N1, j:N) rs:X*

£

j+1ilen s + 1jlen s

post s1,s2

Î

X*

len s1 = i-1

Ù

len s2 = len s – j s= s1

⃕

⃕

s2

Có thể thấy được rằng:

len rs = len s – (i-1 + (len s -j))

= (j – i) + 1

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

v

Thường hàm subseq(i,j,q) được viết là s(i,…,j)

v

Ví dụ:

s1(2,…,2)=[b]

s1(1,…,3)=[b,b,c]

s1(1,…,0)=[]

s1(4,…,3)=[]

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

v

Sơ đồ của các phép toán trên mảng

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

TS. Vũ Thanh Nguyên

Nội dung

v

Tổng quan về hàm

v

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

v

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

v

Đặc tả đệ quy và sử dụng hàm phụ

v

Một số cấu trúc điều khiển

Tổng Quan Về Hàm

v

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:

ê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

Tổng Quan Về Hàm

v

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

≜

*

H

àm xác định giá trị tuyệt đối

abs

: Z → N

abs

≜

if i

Tổng Quan Về Hàm

v

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

Þ

divides

j

Hàm xác định số chẵn

is-even

: N → B

is-even

≜

2

divides

Hàm xác định số lẻ

is-odd

: N → B

is-odd

≜

is-even

Tổng Quan Về Hàm

v

Hàm ước số chung của 2 số

is-common-divisor

: N

´

N

´

N1 → B

is-common-divisor

(i,j,d)

≜

d

divides

Ù

d

divides

j

Hàm xác định giá trị nhỏ hơn 3

less-than-three

: N → B

less-than-three

≜

i<3

Tổng Quan Về Hàm

v

Hàm xác định số nguyên tố

is-prime

: N → B

is-prime

≜

¹

1 dN1 d divides i d=1 d=i

hoặc có thể định nghĩa

is-prime

≜

¹

1 d{2,…,i-1}

¬(d

divides i)

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

Đặc tả hàm

v

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)

Đặc tả hàm

v

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

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

v

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

Vị từ pre-condition

Vị từ post-condition

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

v

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

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

v

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

v

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

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

v

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

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

v

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

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

v

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.

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

v

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ả

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

v

Ví dụ:

max_of_set

(s:

ℕ

-set

r:

ℕ

¹

{}

Î

v

Ví dụ:

abs

(z:

ℤ

r:

ℕ

true

((r = z)

Ù

(z

³

0))

((r = -z)

Ù

(z < 0))

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

v

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)

Ù

¬ sN1

is-common-divisor (i,j,s)

Ù

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

v

Ví dụ: tính căn bật hai của một số nguyên

int_sqr

(x:

ℕ

) z:

ℕ

x

1

(z2 ≤ x)

Ù

(x < (z+1)2)

v

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:

ℕ

(x > 0)

Ù

(y > 0)

$

dZ (y=d

´

x+m)

Ù

(0≤m) (m<x)

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

v

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 ?

v

Thảo luận:?

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

v

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

( (r =

true

( p, f

String

t = p

⃕

⃕

f ) )

( (r =

false

( p, f

String

t = p

⃕

⃕

f ) )

Phiên bản 1’:

issubstr

(s:

String

, t:

String

) r:

B

true

r = ( p, f

String

t = p

⃕

⃕

f )

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

v

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

r = ( f

String

t = p

⃕

⃕

f )

v

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

is-prefix

(p, s, t)

Ù

q

String

is-prefix

(q, s, t)

len

q

len

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

v

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:

ℕ

¹

[]

Ù

cx []

$

String

·

is-shortes-prefix

(p, pt, cx) r = (1 +

len

(r = 0)

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

v

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

v

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

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

v

function_name :

input_type → output_type

function_name

(input_parameter)

≜

expression

hay

v

tên-hàm :

Tập-nguồn

1

´

Tập-nguồn

2

…

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

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

v

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

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

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

v

Cú pháp:

if

Biểu-thức-điều-kiện

then

giá-trị1

else

giá-trị2

v

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

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

v

Ví dụ: hàm tính giai thừa bằng phương pháp tường minh

factorial

: N → N

factorial

≜

if n

≥ 1

then n

´

fact

orial

(n-1)

else 1

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

v

Ví dụ:

Cấu trúc cases

v

Cú pháp:

cases

index:

(value1, value2

result1,

value3, value4, value5

result2,

…

valuen

resultm

Cấu trúc cases

v

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

Sử dụng hàm phụ

v

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

then

29

else

28

Sử dụng hàm phụ

v

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

≜

cases

of

mk-Farenheit(v)

mk-Celsius ((v-32)*5/9),

mk- Celsius(v)

end

Sử dụng hàm phụ

v

Ví dụ: Hàm tính USCLN của 2 số nguyên dương

uscln

(x :

ℕ

1

, y :

ℕ

1

r :

ℕ

1

là-usc

(r, x, y)

Ù

ℕ

1

·

là-usc

(n, x, y) n r )

là-usc

( z:

ℕ

1

,

x

:

ℕ

1

, y :

ℕ

1

r :

B

r =

chia-hết

(x, z)

Ù

chia-hết

(y, z) )

chia-hết

(x :

ℕ

1

, y :

ℕ

1

r :

B

r =

$

k

Î

ℕ

1

·

x

= y*k

Sử dụng hàm phụ

v

Ví dụ: Hàm tính USCLN của 2 số nguyên dương

uscln

(x :

ℕ

1

, y :

ℕ

1

r :

ℕ

1

là-usc

(r, x, y)

Ù

ℕ

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

Đặc tả đệ quy

v

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

Đặc tả đệ quy

v

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:

ℤ

¹

[]

Î

elems

s ) (x

elems

·

x

£

maxnum

(s:

ℤ

*

) r:

ℤ

¹

[]

( ( r =

hd

len

s = 1) )

( ( r =

hd

maxnum

tl

hd

s) ( r =

maxnum

tl

Đặc tả đệ quy

v

Ví dụ: Đặc tả hàm trả về giá trị của phần tử lớn nhất trong mảng

maxnum

:

ℤ

*

ℤ

maxnum

≜

if

len

s = 1

then

hd

else

if

hd

maxnum

tl

then

hd

else

maxnum

tl

Khai báo biến tạm bằng let-in

v

Cú pháp 1:

let

định danh (identifier) = Biểu-thức1

Biểu-thức2

v

Ý 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

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

cos (y) / y

Ký pháp let-in

v

Ví dụ: Đặc tả hàm tính giá trị tuyệt

đối

của tích 2 số nguyên nh

ư

sau:

absprod

:

ℤ

ℤ

N

absprod

(i,j)

≜

let

k = i*j

if

k

then

–k

else

k

Ký pháp let-in

v

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

Ký pháp let-in

v

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

≜

if

Î

Farenheit

then let

mk-Farenheit(v) = t

mk-Celsius ((v-32)*5/9)

else

Ký pháp let-in

v

Ví dụ: Đặc tả hàm trả về giá trị của phần tử lớn nhất trong mảng

maxnum

:

ℤ

*

ℤ

maxnum

≜

if

len

s = 1

then

hd

else

let

max-in-tail

=

maxnum

tl

if

hd

max-in-tail

then

hd

else

max-in-tail

Khai báo biến tạm bằng let-in

v

Cú pháp 2a:

let

định danh

Î

Biểu-thức-tập-hợp

Biểu-thức

v

Cú pháp 2b:

let

định danh

Î

Biểu-thức-tập-hợp

s.t.

Điều-kiện

Biểu-thức

v

Ý 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

Khai báo biến tạm bằng let-in

v

Ví dụ: Đặc tả hàm tính tổng các phần tử trong 1 tập hợp

sumset

:

ℝ

-set

ℝ

sumset

≜

if

= {}

then

0

else

let

x

x

+

sum-set

( s – {x} )