Bài giảng Đặc tả ngôn ngữ lập trình - Ngữ nghĩa tác vụ

ĐẶC TẢ NGÔN NGỮ LẬP TRÌNH
Ngữ Nghĩa Tác Vụ
TS. Nguyễn Hứa Phùng
Khoa CNTT-ĐHBK TPHCM
2007
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM2
GIỚI THIỆU
z Đặc tả ngữ nghĩa hình thức cho phép:
– Chứng minh tính đúng đắn của chương trình
– Kiểm tra tính đúng đắn của chương trình dịch
z Các phương pháp đặc tả:
– Ngữ nghĩa tác vụ (operational semantics)
– Ngữ nghĩa biểu thị (denotational semantics)
– Ngữ nghĩa tiên đề (axiomatic semantics)
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM3
YÊU CẦU
z Đầy đủ
Mọi chương trình đúng và dừng thì phải có ngữ
nghĩa phù hợp được cho bởi các luật
z Nhất quán
Cùng một chương trình không thể cho nhiều ngữ
nghĩa khác nhau và mâu thuẫn
z Không phụ thuộc 
Không có luật nào có thể dẫn xuất từ một luật khác
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM4
NGÔN NGỮ MẪU
expr → expr ‘+’ term | expr ‘-’ term | term
term → term ‘*’ factor | factor
factor → ‘(‘ expr ‘)’ | number
number → number digit | digit
digit → ‘0’ | ‘1’ | ‘2’ | ‘3’ | ‘4’ | ‘5’ | ‘6’ | ‘7’ | ‘8’ | ’9’
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM5
CÚ PHÁP TRỪU TƯỢNG
E → E1 ‘+’ E2 | E1 ‘-’ E2 | E1 ‘*’ E2 | ‘(’ E1 ‘)’ | N
N → N1D | D
D → ‘0’ | ‘1’ | … | ‘9’
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM6
NGỮ NGHĨA TÁC VỤ
z Dựa vào một máy ảo mà tập các tác vụ của 
nó đã được định nghĩa chính xác
z Ngữ nghĩa của mỗi phần tử chương trình 
được đặc tả bằng 1 tập các tác vụ của máy 
ảo
Chương trình Điều khiển Bộ lưu trữ
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM7
MÁY RÚT GỌN
(reduction machine)
z Bộ điều khiển rút gọn một chương trình 
thành giá trị ngữ nghĩa của nó.
( 3 + 4 ) * 5 ⇒ (7) * 5
⇒ 7 * 5
⇒ 35
z Luật rút gọn
z Tiên đề
Điều kiện
Kết quảa+b=c
b+a=c
a →b,b →c
a →c
Kết quả a + 0 = a
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM8
LUẬT RÚT GỌN CHO BIỂU THỨC
z E → E1 ‘+’ E2 | E1 ‘-’ E2 | E1 ‘*’ E2 | ‘(‘ E1’)’
N → N1D | D
D → ‘0’ | ‘1’ | … | ‘9’
1) ‘0’⇒ 0
‘1’⇒ 1
…
‘9’⇒ 9
2) V‘0’⇒ 10 * V
V‘1’⇒ 10 * V + 1
…
V‘9’⇒ 10 * V + 9
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM9
LUẬT CHO BIỂU THỨC (tt)
10)
E ⇒ E1
V ‘+’ E⇒ V ‘+’ E1
3) V1 ‘+’ V2⇒ V1 + V2
4) V1 ‘–’ V2⇒ V1 – V2
5) V1 ‘*’ V2⇒ V1 * V2
6) ‘(’ V ‘)’⇒ V 11)
E ⇒ E1
V ‘–’ E⇒ V ‘–’ E1
12)
E ⇒ E1
V ‘*’ E⇒ V ‘*’ E17)
E ⇒ E1
E ‘+’ E2 ⇒ E1 ‘+’ E2
13)
E ⇒ E1
‘(’ E ‘)’⇒ ‘(’ E1 ‘)’8)
E ⇒ E1
E ‘–’ E2 ⇒ E1 ‘–’ E2
9)
E ⇒ E1
E ‘*’ E2 ⇒ E1 ‘*’ E2
14)
E ⇒ E1, E1⇒ E2
E ⇒ E2
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM10
VÍ DỤ
‘2’ ‘*’ ‘(’ ‘3’ ‘+’ ‘4’ ‘)’
‘3’ ‘+’ ‘4’⇒ 3 ‘+’ ‘4’
⇒ 3 ‘+’ 4 
⇒ 3 + 4 = 7 
‘3’ ‘+’ ‘4’⇒ 7 
‘(’ ‘3’ ‘+’ ‘4’ ‘)’⇒ ‘(’ 7 ‘)’
⇒ 7 
‘2’ ‘*’ ‘(’ ‘3’ ‘+’ ‘4’ ‘)’⇒ 2 ‘*’ ‘(’ ‘3’ ‘+’ ‘4’ ‘)’
⇒ 2 ‘*’ 7 
⇒ 2 * 7 = 14
(luật 1 và 7)
(luật 1 và 10)
(luật 3)
(luật 14)
(luật 13)
(luật 6)
(luật 1 và 9)
(luật 12)
(luật 5)
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM11
NGÔN NGỮ MẪU MỞ RỘNG
expr → expr ‘+’ term | expr ‘-’ term | term
term → term ‘*’ factor | factor
factor → ‘(‘ expr ‘)’ | number
number → number digit | digit
digit → ‘0’ | ‘1’ | ‘2’ | ‘3’ | ‘4’ | ‘5’ | ‘6’ | ‘7’ | ‘8’ | ’9’
factor → ‘(‘ expr ‘)’ | number | identifier 
program → stmt-list
stmt-list → stmt ‘;’ stmt-list | stmt
stmt → identifier ‘:=’ expr
identifier → identifier letter | letter
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM12
CÚ PHÁP TRỪU TƯỢNG
P → L
L → L1 ‘;’ L2 | S
S → I ‘:=’ E 
E → E1 ‘+’ E2 | E1 ‘-’ E2 | E1 ‘*’ E2 | ‘(’ E1 ‘)’ | N | I
N → N1D | D
D → ‘0’ | ‘1’ | … | ‘9’
I → I1A | A
A → ‘a’ | ‘b’ | … | ‘z’
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM13
MÔI TRƯỜNG
z Env: Identifier → Integer ∪ {undef}
z Env0(I) = undef for all I
z VD: a := 5;
b := a * 4;
a := b – 5;
z Env&{I = n} : thêm 1 ràng buộc mới vào môi trường
15 if I = a
Env(I) = 20 if I = b
undef otherwise
(Env&{I=n})(J) =
n if J = I
Env(J) otherwise
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM14
LUẬT CHO BIỂU THỨC 
z : biểu thức E được tính trong môi 
trường Env
z Thay đổi các luật rút gọn dùng dạng biểu 
diễn có chứa môi trường
z Thêm luật cho danh hiệu
7)
E ⇒ E1
E ‘+’ E2 ⇒ E1 ‘+’ E2
7)
 ⇒ 
⇒ 
⇒ 15)
Env(I) = V
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM15
LUẬT CHO CÁC PHÁT BIỂU
16) ⇒ Env & {I = V}
17) ⇒ 
⇒ 
 ⇒ Env118)
⇒ 
19) L ⇒ 
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM16
VÍ DỤ
a := 3 + 4; b := a * 4; a := b – 5
a := 3 + 4; b := a * 4; a := b – 5
⇒ 
 ⇒ ⇒ Env0 & {a = 7} = {a = 7}
 ⇒ 
⇒ 
⇒ 
⇒ {a = 7} & { b = 28} = {a = 7, b = 28}
Luật 19
Luật 3, 17
Luật 16
Luật 18
Luật 15, 9
Luật 1, 10, 5, 17
Luật 16
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM17
VÍ DỤ (tt)
⇒ 
⇒ 
⇒ 
⇒ {a = 7, b = 28} & {a = 23} = {a = 23, b = 28} 
Luật 18
Luật 15, 9
Luật 1, 11, 4
Luật 16
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM18
NGÔN NGỮ MẪU MỞ RỘNG(tt)
stmt → assign-stmt | if-stmt | while-stmt
assign-stmt → identifier ‘:=’ expr
if-stmt → ‘if’ expr ‘then’ stmt-list ‘else’ stmt-list ‘fi’
while-stmt → ‘while’ expr ‘do’ stmt-list ‘od’
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM19
CÚ PHÁP TRỪU TƯỢNG
P → L
L → L1 ‘;’ L2 | S
S → I ‘:=’ E | ‘if’ E ‘then’ L1 ‘else’ L2 ‘fi’ |
‘while’ E ‘do’ L ‘od’
E → E1 ‘+’ E2 | E1 ‘-’ E2 | E1 ‘*’ E2 | ‘(’ E1 ‘)’ | N | I
N → N1D | D
D → ‘0’ | ‘1’ | … | ‘9’
I → I1A | A
A → ‘a’ | ‘b’ | … | ‘z’
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM20
LUẬT CHO IF 
 ⇒ 
 ⇒
20)
V > 0 
 ⇒ 
21)
V ≤ 0 
 ⇒ 
22)
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM21
LUẬT CHO WHILE
 ⇒ , V > 0 
 ⇒ Env23)
 ⇒ , V ≤ 0 
 ⇒ <L; ‘while’ E
‘do’ L ‘od’ | Env>
24)
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM22
VÍ DỤ
n := 0 – 3;
if n then i := n else i := 0 – n fi;
fact := 1;
while i do
fact := fact * i;
i := i – 1;
od 
{n = -3}
{n = -3, i = 3}
{n = -3, i = 3, fact = 1}
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM23
VÍ DỤ
⇒ và 3 > 0, dùng luật 24 cho phát biểu 
while
⇒ 
⇒ 
⇒ {n = -3, i = 3, fact = 3}
⇒ 
⇒ 
⇒ {n = -3, i = 2, fact = 3}
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM24
VÍ DỤ
⇒ và 2 > 0, dùng luật 24 cho phát biểu 
while
⇒ 
⇒ 
⇒ {n = -3, i = 2, fact = 6}
⇒ 
⇒ 
⇒ {n = -3, i = 1, fact = 6}
...
⇒ {n = -3, i = 0, fact = 6}
Dùng luật 23 ⇒ kết thúc
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM25
HIỆN THỰC MÁY RÚT GỌN
z Giả sử các phát biểu và biểu thức được thể hiện ở
dạng tiền tố
c := a + b * 12 ⇒ assigne(c,plus(a, times(b,12)))
z Đơn giản: Không xét đến môi trường
V1 ‘+’ V2⇒ V1 + V2
reduce(plus(V1,V2),R) :- integer(V1), integer(V2), !, 
R is V1 + V2.
reduce(plus(E,E2),plus(E1,E2)) :- reduce(E,E1).
7) E ⇒ E1
E ‘+’ E2 ⇒ E1 ‘+’ E2
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM26
HIỆN THỰC MÁY RÚT GỌN (tt)
reduce(E,E2) :- reduce(E,E1), reduce(E1,E2) ???
reduce_all(V,V) :- integer(V),!.
reduce_all(E,E2) :- reduce(E,E1), reduce_all(E1,E2).
14) E ⇒ E1, E1⇒ E2
E ⇒ E2
Ngữ nghĩa tác vụ Khoa CNTT-DHBK TPHCM27
HIỆN THỰC MÁY RÚT GỌN (tt)
z Chứa môi trường:
Biểu diễn ⇒ config(E,Env)
reduce(config(I,Env),config(V,Env)) :- atom(I), !, lookup(Env,I,V).
reduce(config(assign(I,V),Env),Env1) :-
integer(V), !, update(Env, value(I,V), Env1).
⇒ 15)
Env(I) = V
16) ⇒ Env & {I = V}