Chương 2 : Cú pháp và ngữ nghĩa

Khoa KTMT - UIT TS. Vũ Đức Lung 1 TRÌNH BIÊN DỊCH (COMPILER) Khoa Kỹ thuật máy tính  TS. Vũ Đức Lung  Email: lungvd@uit.edu.vn Khoa KTMT - UIT TS. Vũ Đức Lung 2 Chương 2 : Cú pháp và ngữ nghĩa Nội dung: Các khái niệm cơ bản Đặc tả hình thức (Formal description) Đặc tả từ vựng Biểu thức chính quy Đặc tả cú pháp hình thức Khoa KTMT - UIT TS. Vũ Đức Lung 3 Các khái niệm cơ bản  NNLT = Ký hiệu + qui tắc kết hợp  Cú pháp: sự kết hợp của các ký hiệu (dạng của biểu thức, các phát biểu, các đơn vị nhỏ trong chương trình)  Ngữ nghĩa: ý nghĩa của các kết hợp  Ngữ dụng: Mối quan hệ của L (cú pháp+ngữ nghĩa) với thế giới bên ngoài  Ví dụ 1: – BT1 = 4 BT2 = 1 + 3 BT3 = 1 + 1 + 1 +1  VD 2: vòng lặp WHILE và REPEAT trong Pascal  VD 3: Số lượng tối đa các phần tử mảng array phụ thuộc – Kích thước kiểu dữ liệu – Dung lượng bộ nhớ Khoa KTMT - UIT TS. Vũ Đức Lung 4 Đặc tả hình thức (Formal description)  Đặc tả hình thức cung cấp một mô tả chính xác về một ngôn ngữ lập trình(nnlt) Chương trình Bộ dịch Đặc tả NNLT Khoa KTMT - UIT TS. Vũ Đức Lung 5 Đặc tả hình thức  Đặc tả hình thức cho phép: – Người học có thể tiếp thu nnlt dễ dàng – Bộ dịch có thể sinh mã đúng đắn – Bộ dịch có thể kiểm tra lỗi tự động – Có thể chứng minh được tính đúng đắn của chương trình  Đặc tả hình thức: – Từ vựng – Văn phạm (cú pháp) – Ngữ nghĩa Khoa KTMT - UIT TS. Vũ Đức Lung 6 Đặc tả từ vựng  Ngôn ngữ là tập hợp chuỗi các ký tự từ alphabet (A…Z, a…z, $ @ 0 …9, + - = ….  Sự kết hợp một số ký tự trong alphabet  từ vựng – VD: BEGIN  Token là một dạng của lexeme – VD: index = 2*count + 17; Lexemes Tokens Index Identifier = Equal_sign 2 Int_literal * Mult_op Count Identifier + Plus_op 17 Int_literal ; semicolon Tokens tương tự như loại từ trong ngôn ngữ học. Tương tự như danh từ hay tính từ, động từ, tokens sẽ được định nghĩa gồm từ khóa (keyword), định danh (identifier), số nguyên, số chấm động tùy theo đặc điểm của trình biên dịch Khoa KTMT - UIT TS. Vũ Đức Lung 7 Ngôn ngữ  Chuỗi và ngôn ngữ – Tập hợp các ký tự Σ – Một chuỗi S trên Σ là 1 dãy hữu hạn các ký tự thuộc Σ – Chuỗi rỗng ∈ – Một ngôn ngữ L trên Σ là tập hợp các chuỗi trên Σ  Tác vụ trên ngôn ngữ – Hợp: L1  L2 – Kết nối: L1 L2 Khoa KTMT - UIT TS. Vũ Đức Lung 8 Ví dụ: L = {A, B, ..., Z, a, b, ..., z } và D = { 0, 1, , ..., 9 } 1. L  D là tập hợp các chữ cái và chữ số 2. LD là tập hợp các xâu bao gồm một chữ cái và một chữ số 3. L4 là tập hợp tất cả các xâu 4 chữ cái 4. L * là tâp hợp tất cả các xâu của các chữ cái bao gồm cả chuỗi rỗng 5. L(L  D)* là tập hợp tất cả các xâu mở đầu bằng một chữ cái theo sau là chữ cái hay chữ số 6. D+ là tập hợp tất cả các xâu gồm một hoặc nhiều chữ số Ngôn ngữ Khoa KTMT - UIT TS. Vũ Đức Lung 9 Biểu thức chính quy (regular expression) Một chuỗi miêu tả một bộ các chuỗi khác, theo những quy tắc cú pháp nhất định  Có thể hiểu như là 1 ngôn ngữ nhỏ dùng cho mục đích : để tìm chuỗi con trong biểu thức chuỗi lớn Microsoft cho nó vào Windows trong namespace .NET : System.Text.RegularExpressions VD: email – /^(?:\w+\.?)*\w+@(?:\w+\.)+\w+$/ – Tìm hiểu các biểu thức chính qui trong RegularExpressionValidator trong Validation Control trong ASP.NET? Khoa KTMT - UIT TS. Vũ Đức Lung 10 Định nghĩa chính qui (regular definition)  Để thuận tiện về mặt kí hiệu, ta dùng định nghĩa chính qui (ĐNCQ) để đặt tên cho các BTCQ Một ĐNCQ là một dãy các định nghĩa có dạng d1  r1 d2  r2 ......... dn  rn Trong đó di là các tên, ri là các BTCQ trên tập các kí hiệu {d1, d2, ....di-1} Khoa KTMT - UIT TS. Vũ Đức Lung 11 Biểu thức chính quy  Để biểu diễn các tokens, người ta dùng biểu thức chính quy a : có xuất hiện ký tự 'a' ab : có xuất hiện ký tự 'b' theo sau ký tự 'a' (theo đúng thứ tự) a|b : có 'a' hoặc có 'b' a* : xuất hiện nhiều hoặc không xuất hiện ký tự 'a' a+ : xuất hiện nhiều hoặc ít nhất là một ký tự 'a' (a)+ == a(a)* a3 : xuất hiện 3 ký tự a a? : xuất hiện a hoặc không xuất hiện (a)? = a | ∈  VD: biểu diễn số nguyên: digits = '0' | '1' | '2' | '3' | '4 | '5' | '6' | '7' | '8' | '9' integer = '−'?(digits)+ Khoa KTMT - UIT TS. Vũ Đức Lung 12  Ví dụ: ĐNCQ cho tập số không dấu được viết lại như sau digit  0 | 1 |...| 9 digits  digit + optional_fraction  (. digits) ? optional_exponent  ( E ( + | - ) ? digits) ? num  digits optional_fraction optional_exponent  Sử dụng các tập kí tự [abc]=a | b | c, [a-z]=a | b |..z ta có thể đặc tả các định danh bởi BTCQ [A - Z a - z] [A - Z a - z 0 - 9]* Biểu thức chính quy Khoa KTMT - UIT TS. Vũ Đức Lung 13 Biểu thức chính quy  Biểu thức chính qui r diễn tả ngôn ngữ L(r) – ∈⇒ {∈} – a ∈ Σ ⇒ {a}  Giả sử r và s lần lượt diễn tả ngôn ngữ L(r) và L(s) thì – (r) | (s) ⇒ L(r) ∪ L(s) – (r)(s) ⇒ L(r)L(s) – (r)* ⇒ (L(r))* – (r) ⇒ L(r) Khoa KTMT - UIT TS. Vũ Đức Lung 14 Ví dụ: Cho = { a, b}. 1. BTCQ a | b đặc tả {a, b} 2. BTCQ (a | b) (a | b) đặc tả {aa, ab, ba, bb}.Tập hợp này có thể được đặc tả bởi BTCQ tương đương sau: aa | ab | ba | bb 3. BTCQ a* đặc tả {, a, aa, aaa, ... } 4. BTCQ (a | b)* đặc tả {a, b, aa,bb, ...}. Tập hợp này có thể đặc tả bởi (a*b* )* 5. BTCQ a | a* b đặc tả {a, b, ab, aab,... } Biểu thức chính quy Khoa KTMT - UIT TS. Vũ Đức Lung 15 Ví dụ: ĐNCQ của các định danh trong pascal là letter  A | B | ...| Z | a | b |...| z digit  0 | 1 | ...| 9 id  letter (letter | digit)* Ví dụ: ĐNCQ của các số không dấu trong pascal như 3254, 23.243E5,16.264E-3... là digit  0 | 1 |...| 9 digits  digit digit* optional_fraction  (. digits)? optional_exponent  ( E ( + | - )? digits)? num  digits optional_fraction optional_exponent Khoa KTMT - UIT TS. Vũ Đức Lung 16 Đặc tả cú pháp hình thức (Formal methods of Describing Syntax)  Cú pháp trừu tượng (Abstract syntax)  Cú pháp cụ thể (concrete syntax) – Văn phạm phi ngữ cảnh (context-free grammar) – BNF (Backus-Naur Form)  Sơ đồ cú pháp (Syntax diagrams)  Chuỗi dẫn xuất và Cây phân tích (Derivations and parse trees)  Sự nhập nhằng (Ambiguity)  Tính kết hợp của toán tử (Associativity of Operator)  BNF mở rộng (Extended BNF) Khoa KTMT - UIT TS. Vũ Đức Lung 17 Cú pháp trừu tượng  Phân các yếu tố ngôn ngữ thành các lớp văn phạm (Syntactic class)  Liệt kê tất cả các dạng (Syntactic form) của mỗi lớp  Ví dụ: – Lớp cú pháp: C Hằng (constant) I Định danh (Identifier) O Toán tử (operator) E Biểu thức (expression) – Dạng cú pháp: E ::= I | C | E O E | ( E ) Khoa KTMT - UIT TS. Vũ Đức Lung 18 Cú pháp trừu tượng • Ưu điểm: đơn giản • Khuyết điểm: Không có định nghĩa ký tự kết thúc Có thể xảy ra hiện tượng nhập nhằng Khoa KTMT - UIT TS. Vũ Đức Lung 19 Đặc tả cú pháp hình thức (Formal methods of Describing Syntax)  Cú pháp trừu tượng (Abstract syntax)  Cú pháp cụ thể (concrete syntax) – Văn phạm phi ngữ cảnh (context-free grammar) – BNF (Backus-Naur Form)  Sơ đồ cú pháp (Syntax diagrams)  Chuỗi dẫn xuất và Cây phân tích (Derivations and parse trees)  Sự nhập nhằng (Ambiguity)  Tính kết hợp của toán tử (Associativity of Operator)  BNF mở rộng (Extended BNF) Khoa KTMT - UIT TS. Vũ Đức Lung 20 Văn phạm phi ngữ cảnh Context-Free Grammars  1956-1959, Chomsky  Là một bộ gồm 4 thành phần: Ký hiệu bắt đầu S  N(Start symbol) Tập các ký hiệu không kết thúc N (Non-terminals) Tập các ký hiệu kết thúc  (Terminals) Tập các luật sinh (Production) có dạng: A  a Với A  N và a là chuỗi các ký hiệu kết thúc và không kết thúc Khoa KTMT - UIT TS. Vũ Đức Lung 21 Ví dụ số nguyên không dấu (Unsigned Integers) • Ký hiệu bắt đầu • Ký hiệu không kết thúc , • Ký hiệu kết thúc 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 • Luật  | Khoa KTMT - UIT TS. Vũ Đức Lung 22 BNF (Backus-Naur Form)  1959, John Backus giới thiệu ALGOL 58 thuộc nhóm ACM-GAMM  1960 Peter Naur cho ra phiên bản mới ALGOL 60  BNF là một ký hiệu tự nhiên mô tả cú pháp, là một siêu ngôn ngữ mô tả ngôn ngữ khác  Rất gần với văn phạm phi ngữ cảnh VD: ::= | Khoa KTMT - UIT TS. Vũ Đức Lung 23 BNF (Backus-Naur Form)  left-hand side (LHS)  right-hand side (RHS)  Có thể có nhiều RHS VD: -> | begin end  Danh sách cú pháp ( Syntactic lists) dùng đệ qui -> ident | ident, Khoa KTMT - UIT TS. Vũ Đức Lung 24 Ví vụ một biểu thức  Start symbol  Non-terminals , , , , ,  Terminals 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, +, -, *, /  Productions:  |  |  | ()  + | -  * | / Khoa KTMT - UIT TS. Vũ Đức Lung 25 Đặc tả cú pháp hình thức (Formal methods of Describing Syntax)  Cú pháp trừu tượng (Abstract syntax)  Cú pháp cụ thể (concrete syntax) – Văn phạm phi ngữ cảnh (context-free grammar) – BNF (Backus-Naur Form)  Sơ đồ cú pháp (Syntax diagrams)  Chuỗi dẫn xuất và Cây phân tích (Derivations and parse trees)  Sự nhập nhằng (Ambiguity)  Tính kết hợp của toán tử (Associativity of Operator)  BNF mở rộng (Extended BNF) Khoa KTMT - UIT TS. Vũ Đức Lung 26 Sơ đồ cú pháp (Syntax Diagrams) term exp term_op term exp Sơ đồ cú pháp của biểu thức Khoa KTMT - UIT TS. Vũ Đức Lung 27 Đặc tả cú pháp hình thức (Formal methods of Describing Syntax)  Cú pháp trừu tượng (Abstract syntax)  Cú pháp cụ thể (concrete syntax) – Văn phạm phi ngữ cảnh (context-free grammar) – BNF (Backus-Naur Form)  Sơ đồ cú pháp (Syntax diagrams)  Chuỗi dẫn xuất và Cây phân tích (Derivations and parse trees)  Sự nhập nhằng (Ambiguity)  Tính kết hợp của toán tử (Associativity of Operator)  BNF mở rộng (Extended BNF) Khoa KTMT - UIT TS. Vũ Đức Lung 28 Chuỗi dẫn xuất (Derivations)   +  +  * + 4  * 5 + 8  32 * 5 + 8 Chuỗi dẫn xuất của biểu thức Khoa KTMT - UIT TS. Vũ Đức Lung 29 Cây phân tích cú pháp (Parse Trees) + 32 5 8 * Khoa KTMT - UIT TS. Vũ Đức Lung 30 Cây cú pháp (Parse Trees) + 12 3 4 * Cây cú pháp Khoa KTMT - UIT TS. Vũ Đức Lung 31 Đặc tả cú pháp hình thức (Formal methods of Describing Syntax)  Cú pháp trừu tượng (Abstract syntax)  Cú pháp cụ thể (concrete syntax) – Văn phạm phi ngữ cảnh (context-free grammar) – BNF (Backus-Naur Form)  Sơ đồ cú pháp (Syntax diagrams)  Chuỗi dẫn xuất và Cây phân tích (Derivations and parse trees)  Sự nhập nhằng (Ambiguity)  Tính kết hợp của toán tử (Associativity of Operator)  BNF mở rộng (Extended BNF) Khoa KTMT - UIT TS. Vũ Đức Lung 32 Sự nhập nhằng (Ambiguity)  Văn phạm cho câu lệnh gán đơn giản  =  A|B|C  + | * | () |  VD biểu thức gán: A = B * (A + C) có chuỗi dẫn xuất cực tả: Khoa KTMT - UIT TS. Vũ Đức Lung 33 Sự nhập nhằng (Ambiguity)  Văn phạm cho câu lệnh gán đơn giản (mở rộng VD trước)  =  A|B|C  + | * | () |  Là một văn phạm nhập nhằng vì A = B + C * A có 2 cây cú pháp Khoa KTMT - UIT TS. Vũ Đức Lung 34 Sự nhập nhằng (Ambiguity) Khoa KTMT - UIT TS. Vũ Đức Lung 35 Sự nhập nhằng (Ambiguity)  Văn phạm không nhập nhằng cho câu lệnh gán đơn giản  =  A|B|C  + | term  * | factor  () |  Sử dụng toán tử ưu tiên (operator precedence)  VD tìm chuỗi dẫn xuất và cây cú pháp cho biểu thức : A = B + C * A Khoa KTMT - UIT TS. Vũ Đức Lung 36 Đặc tả cú pháp hình thức (Formal methods of Describing Syntax)  Cú pháp trừu tượng (Abstract syntax)  Cú pháp cụ thể (concrete syntax) – Văn phạm phi ngữ cảnh (context-free grammar) – BNF (Backus-Naur Form)  Sơ đồ cú pháp (Syntax diagrams)  Chuỗi dẫn xuất và Cây phân tích (Derivations and parse trees)  Sự nhập nhằng (Ambiguity)  Tính kết hợp của toán tử (Associativity of Operator)  BNF mở rộng (Extended BNF) Khoa KTMT - UIT TS. Vũ Đức Lung 37 Tính kết hợp của toán tử (Associativity of Operator)  Đối với các toán tử có cùng mức độ ưu tiên  VD: A = B + C + A – Biến là số nguyên: không có sự khác biệt – Biến là số chấm động: có khác biệt, ví dụ số chấm động dùng độ chính xác 7 bit (1 bit trước dấu phẩy và 6 bit sau dấu phẩy) 107 + 1 + … + 1 = ? 10 – (107 + 1) + 1 + … = ? – 1 + 1 + … + 107 = ? Khoa KTMT - UIT TS. Vũ Đức Lung 38 Đặc tả cú pháp hình thức (Formal methods of Describing Syntax)  Cú pháp trừu tượng (Abstract syntax)  Cú pháp cụ thể (concrete syntax) – Văn phạm phi ngữ cảnh (context-free grammar) – BNF (Backus-Naur Form)  Sơ đồ cú pháp (Syntax diagrams)  Chuỗi dẫn xuất và Cây phân tích (Derivations and parse trees)  Sự nhập nhằng (Ambiguity)  Tính kết hợp của toán tử (Associativity of Operator)  BNF mở rộng (Extended BNF) Khoa KTMT - UIT TS. Vũ Đức Lung 39 BNF mở rộng (Extended BNF)  Không làm tăng khả năng đặc tả của BNF, chỉ là cách biểu diễn gọn hơn 1. Phần lựa chọn được đặt vào trong dấu [] -> if () [else )] 2. Đặt những phần tương tự trong RHS vào trong () và ngăn cách bởi | -> (+ | -) const 3. Đặt những phần lập lại trong {} -> letter {letter | digit}  Khoa KTMT - UIT TS. Vũ Đức Lung 40 BNF vs EBNF BNF: -> + | - | -> * | / | EBNF: -> {(+ | -) } -> {(* | /) } Khoa KTMT - UIT TS. Vũ Đức Lung 41 BÀI TẬP Khoa KTMT - UIT TS. Vũ Đức Lung 42 Ngữ nghĩa hình thức (Formal Semantics)  Đặ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  Các phương pháp đặc tả: Ngữ nghĩa tác vụ (Operational semantics) Ngữ nghĩa tiên đề (Axiomatic semantics) Ngữ nghĩa biểu thị (Denotational semantics) Khoa KTMT - UIT TS. Vũ Đức Lung 43 Yêu cầu  Đầ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  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  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 Khoa KTMT - UIT TS. Vũ Đức Lung 44 Ngữ nghĩa hình thức (Formal Semantics)  Đặ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  Các phương pháp đặc tả: Ngữ nghĩa tác vụ (Operational semantics) Ngữ nghĩa tiên đề (Axiomatic semantics) Ngữ nghĩa biểu thị (Denotational semantics) Khoa KTMT - UIT TS. Vũ Đức Lung 45 Ngữ nghĩa tác vụ (Operational Semantics)  Ý tưởng: đặc tả ý nghĩa một chương trình khi thực thi từng câu lệnh trên máy tính (máy thật hoặc mô phỏng)  Sự thay đổi trạng thái của máy tính cho ta ý nghĩa của câu lệnh  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  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 Khoa KTMT - UIT TS. Vũ Đức Lung 46 Ngữ nghĩa tác vụ  Dùng ngữ nghĩa tác vụ để đặc tả ngữ nghĩa một ngôn ngữ lập trình L cần: – Bộ chuyển đổi (translator) đổi L thành ngôn ngữ cấp thấp – Máy ảo cho ngôn ngữ cấp thấp  VD: Ngôn ngữ C: for ( expr1; expr2; expr3 ) { } Ngữ nghĩa tác vụ: expr1; Loop: if expr2 == 0 goto out … Expr3; goto Loop; out:… Khoa KTMT - UIT TS. Vũ Đức Lung 47 Ngữ nghĩa hình thức (Formal Semantics)  Đặ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  Các phương pháp đặc tả: Ngữ nghĩa tác vụ (Operational semantics) Ngữ nghĩa tiên đề (Axiomatic semantics) Ngữ nghĩa biểu thị (Denotational semantics) Khoa KTMT - UIT TS. Vũ Đức Lung 48 Ngữ nghĩa tiên đề (Axiomatic semantics) • Ý nghĩa của chương trình được xác định bởi tập hợp các quy tắc làm thay đổi dữ liệu sau khi thực hiện một phép toán nào đó của ngôn ngữ lập trình. • NNTĐ dùng để chứng minh các tính chất của chương trình • Tác dụng của một phát biểu (statement) được định nghĩa thông qua tiền diều kiện (precondition) và hậu điều kiện (postcondition). • Tập hợp các tiên đề và luật cho định nghĩa tác dụng của chương trình. Khoa KTMT - UIT TS. Vũ Đức Lung 49 Ngữ nghĩa tiên đề  Nếu P đúng thì sau khi S đươc thực thi xong thì Q đúng  Tiền điều kiện yếu nhất (weakest precondition)p(S,Q) là tiền điều kiện yếu nhất có thể thỏa mãn VD: a := b + 1 {a > 1} một tiền đk có thể: {b > 10} Tiền đk yếu nhất: {b > 0}  p(S,Q) với Q là biến số có thể xem là ngữ nghĩa chính xác của S {P} S {Q} Tiền ĐK Phát biểu Hậu ĐK Khoa KTMT - UIT TS. Vũ Đức Lung 50 Ngữ nghĩa tiên đề {PxE} x := E {P}  Ký hiệu NNTĐ thông thường: {P} S {Q} • x = E, Q – hậu đk • Tiên đề: P = QxE • VD: a = b/2 – 1 {a P={b<22}  Phát biểu gán: {QxE} x := E {Q}  Nhiều sách ghi:  VD: x = 2*y – 3 {x>25} => {y>14} Khoa KTMT - UIT TS. Vũ Đức Lung 51 Ngữ nghĩa tiên đề Chứng minh tính đúng của chương trình VD: {x  3} x := x - 3 {x  0} E = x - 3 Q = x > 0 QxE = x - 3 > 0 = x > 3 Trong trường hợp {x  5} x := x - 3 {x  0} ? Khoa KTMT - UIT TS. Vũ Đức Lung 52 Ngữ nghĩa tiên đề  HỆ LUẬT HOARE L1: Nếu {P} S {Q}  (Q  R) thì {P} S {R} L2: Nếu {P} S {Q}  (R  P) thì {R} S {Q} L3: {QxE} x := E {Q} VD1: CM tính đúng: {x  5} x := x - 3 {x  0} ? VD2: CM tính đúng của đặc tả: {f=i!} i:=i+1 {f*i=i!} VD3: CM tính đúng của đặc tả: {f*i=i!} f:=f*i {f=i!} Khoa KTMT - UIT TS. Vũ Đức Lung 53 Ngữ nghĩa tiên đề L4: luật phát biểu ghép (sequences) if ({P} S1 {Q})  ({Q} S2 {R}) then {P} S1 ; S2 {R} VD4: CM tính đúng của đặc tả: {f=i!} i:=i+1, f = f*i {f = i!} CM: theo vd 2 & 3  HỆ LUẬT HOARE Khoa KTMT - UIT TS. Vũ Đức Lung 54 Ngữ nghĩa tiên đề Với ¬B = NOT B VD4: CM tính đúng của đặc tả: {xyy then max:=x else max:=y {max>0} CM: theo L3 & L2  HỆ LUẬT HOARE Khoa KTMT - UIT TS. Vũ Đức Lung 55 Ngữ nghĩa tiên đề VD4: CM tính đúng của đặc tả: {f=i!} while i # n do begin i:=i+1; f:=f*I end {f=n!} CM:  HỆ LUẬT HOARE Khoa KTMT - UIT TS. Vũ Đức Lung 56 Chứng minh chương trình (Program Proofs)  VD: Chứng minh tính đúng của chương trình { x = A AND y = B} t = x; x = y; y = t; {x = B AND y = A} Khoa KTMT - UIT TS. Vũ Đức Lung 57 Ngữ nghĩa hình thức (Formal Semantics)  Đặ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  Các phương pháp đặc tả: Ngữ nghĩa tác vụ (Operational semantics) Ngữ nghĩa tiên đề (Axiomatic semantics) Ngữ nghĩa biểu thị (Denotational semantics) Khoa KTMT - UIT TS. Vũ Đức Lung 58 Ngữ nghĩa biểu thị (Denotational semantics)  Trên cơ sở lý thuyết hàm đệ qui  Phương pháp đặc tả ngữ nghĩa trừ tượng nhất  Phiên bản gốc được phát triển bởi Scott và Strachey (1970)  Tiến trình xây dựng đặc tính biểu thị cho một ngôn ngữ: 1. định nghĩa các đối tượng toán học cho mỗi thực thể ngôn ngữ 2. Định nghĩa hàm ánh xạ mỗi thể hiện của thực thể đến thể hiện của đối tượng toán học tương ứng  Mỗi cấu trúc chương trình là một hàm ánh xạ đầu vào đến đầu ra  Một chương trình là sự hợp thành của nhiều hàm  Sự khác nhau giữa ngữ nghĩa tác vụ và ngữ nghĩa biểu thị: Trong NN tác vụ trạng thái thay đổi bởi thuật toán, còn trong NN biểu thị NN được định nghĩa là các hàm toán học chính xác Khoa KTMT - UIT TS. Vũ Đức Lung 59 Ngữ nghĩa biểu thị  VD cấu trúc ngôn ngữ số nhị phân. – Cú pháp:  0 | 1 | 0 | 1 – Để biểu thị ý nghĩa của số nhị phân sử dụng ngữ nghĩa biểu thị và cú pháp trên sử dụng hàm ngữ nghĩa: • Mbin(‘0’) = 0 • Mbin(‘1’) = 1 • Mbin( ‘0’) = 2* Mbin() • Mbin( ‘1’) = 2* Mbin() + 1 Cây phân tích số 110 và ngữ nghĩa biểu thị của nó? Khoa KTMT - UIT TS. Vũ Đức Lung 60 Ngữ nghĩa biểu thị  Ngữ nghĩa biểu thị của các ký tự số thập phân  0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | (0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9) Mdec('0') = 0, Mdec ('1') = 1, …, Mdec ('9') = 9 Mdec ( '0') = 10 * Mdec () Mdec ( '1’) = 10 * Mdec () + 1 … Mdec ( '9') = 10 * Mdec () + 9 Khoa KTMT - UIT TS. Vũ Đức Lung 61 BÀI TẬP