Chương 1: Tổng quan về đề tài Chương 2: Các kiến thức nền tảng Chương 3: Hệ thống sinh test-case hoàn chỉnh Chương 4: Các giải pháp cho hệ thống sinh test-case Chương 5: Hiện thực hệ thống sinh test-case hoàn chỉnh Chương 6: Kết quả thực nghiệm và Đánh giá Chương 7: Kết luận và hướng phát triển Phân tích MUST-MAY để kiểm tra chương trình 17 Chƣơng 2 Các kiến thức nền tảng 2.1 Tổng quan về separation logic Separation logic [12][13] là logic mở rộng của Hoare logic [14], được dùng để suy diễn cho chương trình sử dụng cấu trúc dữ liệu chia sẻ (mutable data structure). Cấu trúc dữ liệu chia sẻ, tức cấu trúc mà một thuộc tính của nó có thể được tham khảo từ nhiều hơn một con trỏ, thường xảy ra vấn đề bí danh. Đây là một vấn đề gây khó khăn trong việc kiểm tra tính đúng đắn của chương trình. Chúng ta không thể sử dụng Hoare logic để kiểm tra chương trình có chứa các con trỏ vì có thể xảy ra vấn đề bí danh.
Vì vậy, Peter O'Hearn-Đại học London và John Reynolds-Đại học Carnegie Mello đã phát triển separation logic từ Hoare logic bằng cách thêm 2 toán tử mới: spatial conjunction (*) và spatial implication (-*) và một số tiên đề trên separation logic giúp cho việc chứng minh những chương trình có chứa con trỏ.2 Ngữ nghĩa của separation logic 2.1 Mô hình biểu diễn của separation logic Đối với Hoare logic, trạng thái của chương trình được biểu diễn bằng một ánh xạ đi từ tên biến đến miền giá trị Integer (biểu diễn giá trị của biến đó) và được gọi là Store. StoresV V Integers trong đó: + V: tập các biến + Integers: tập các số nguyên biểu diễn giá trị của biến Tuy nhiên, đối với các chương trình có chứa con trỏ, với cách biểu diễn này ta không thể biểu diễn được trường hợp bí danh (tức 2 con trỏ cùng trỏ đến một địa chỉ Phân tích MUST-MAY để kiểm tra chương trình 18 bộ nhớ). Vì vậy, separation logic đề xuất thêm thành phần thứ 2 là heap. Mô hình của separtion logic sẽ có 2 thành phần: store và heap.
Khái niệm store tương tự như khái niệm của stack trong ngôn ngữ lập trình, chức năng của nó là ánh xạ từ các biến đến miền giá trị số nguyên (miền số nguyên này biểu diễn địa chỉ mà biến đó trỏ đến). Heap là ánh xạ đi từ miền địa chỉ ô nhớ (miền này là tập con của miền số nguyên) đến miền số nguyên (biểu diễn giá trị của ô nhớ). Trạng thái của chương trình lúc này sẽ được biểu diễn bằng 2 thành phần (Store x Heap).1 : Mô hình của separation logic (nguồn [12]) • Ints là miền các số nguyên • Variables là miền các biến trong chương trình • Atoms và Locations là tập con của Ints. • Stores là hàm ánh xạ từ biến sang Ints • Heap là ánh xạ từ Location sang Ints.
• States: biểu diễn trạng thái của chương trình được xác định bởi các cặp (Stores x Heaps). Với mô hình này, separation logic có thể biểu diễn các lệnh như cấp phát bộ nhớ, truy xuất, thay đổi giá trị ô nhớ, cũng như hủy bộ nhớ trong các chương trình có chứa con trỏ.1: Trạng thái của chương trình có thể được biểu diễn bằng separation logic qua các lệnh cấp phát, truy xuất, thay đổi giá trị ô nhớ và hủy ô nhớ. Phân tích MUST-MAY để kiểm tra chương trình 19 Hình 2.2: Minh họa trạng thái chương trình qua các lệnh (nguồn [12]) Ký hiệu [E] biểu diễn giá trị tại ô nhớ E.2, giả sử chương trình ban đầu có 2 biến x và y trỏ đến 2 ô nhớ có địa chỉ tương ứng là 3 và 4. - Lệnh x := cons(1,2) khai báo biến x trỏ đến ô nhớ trong heap có giá trị là 1, và ô nhớ tiếp theo ô nhớ này trong heap có giá trị là 2.
- Lệnh y := [x] gán biến y trỏ đến ô nhớ có địa chỉ là nội dung của biến x - Lệnh [x+1] := 3; thay đổi giá trị của ô nhớ tại địa chỉ x + 1 - Lệnh dispose(x+1): hủy ô nhớ tại địa chỉ x+1 Ví dụ 2.2: Minh họa việc dùng separation logic để có thể phát hiện lỗi trong chương trình, ở ví dụ này là lỗi truy xuất đến con trỏ null. Phân tích MUST-MAY để kiểm tra chương trình 20 Hình 2.3: Minh họa dùng separation logic để phát hiện lỗi chương trình (nguồn [12]) 2.2Các toán tử của separation logic Bên cạnh các toán tử được sử dụng trong Hoare logic, separation logic cung cấp thêm một số toán tử sau để thuận tiện trong việc biểu diễn heap. emp: biểu diễn một heap rỗng e e’: heap chứa một ô nhớ duy nhất, tại địa chỉ e và có giá trị là e’. p1 * p2 : heap được chia thành 2 phần heap không giao nhau là p1 và p2 p1 - * p2: Như ta đã biết, Hoare logic chỉ có thể biểu diễn trạng thái của chương trình thông qua ánh xạ từ tên biến đến giá trị của biến đó trong các chương trình không chứa con trỏ.
Đối với các chương trình có chứa con trỏ, để biểu diễn trạng thái của chương trình, Hoare logic không thể biểu diễn trường hợp một con trỏ đang trỏ đến một ô nhớ nào đó, như trong ví dụ 2. Separation logic đã đề xuất toán tử , e e’ biểu diễn cho con trỏ e đang trỏ đến một ô nhớ có giá trị e’.3: int * p = new int(); *p = 3; Thứ hai là vấn đề bí danh, Hoare logic không thể biểu diễn được trường hợp các Phân tích MUST-MAY để kiểm tra chương trình 21 con trỏ có trỏ đến cùng một địa chỉ bộ nhớ hay không. Separation logic đã đề xuất toán tử *, p1 * p2 biểu diễn 2 vùng nhớ heap là không giao nhau, lúc này sẽ không xảy ra vấn đề bí danh.4: Minh họa cho trường hợp p và q trỏ đến 2 vùng nhớ khác nhau int * p = new int(); int * q = new int(); *p = 3; *q = 2; Sau đây là một số ví dụ dùng separation logic để biểu diễn trạng thái của chương trình Ví dụ 2.5: x 3, y : biểu diễn x trỏ đến 2 ô nhớ liên tục trong heap. Ô nhớ x trỏ đến có giá trị là 3, ô nhớ kế tiếp có giá trị là y (tức là, store ánh xạ x đến giá trị α và y đến giá trị β, α là một địa chỉ, khi đó heap ánh xạ α đến giá trị là 3 và ánh xạ địa chỉ α + 1 đến giá trị β) Tương tự cho trường hợp Ví dụ 2.6: x 3, y y 3, x : công thức này có nghĩa là: 2 phần heap không giao nhau, phần thứ nhất chứa 2 ô nhớ liên tục có giá trị lần lượt là 3 và y, và được trỏ đến bởi x, phần thứ hai chứa 2 ô nhớ liên tục là 3 và x, và được trỏ đến bởi y.
Phân tích MUST-MAY để kiểm tra chương trình 22 Ví dụ 2.7: x 3, y y 3, x: biểu diễn 2 heap giao nhau, tức x và y trỏ đến cùng một ô nhớ Bên cạnh đó, separation logic còn rất hữu dụng trong việc mô tả các cấu trúc dữ liệu phức tạp. Để đặc tả chương trình một cách đầy đủ, cần phải mô tả nhiều hơn về các hình thức cấu trúc của nó và mối quan hệ giữa các trạng thái của chương trình đối với các giá trị trừu tượng mà chúng biểu thị. Cho ví dụ, để biểu diễn cấu trúc danh sách trong separation logic, chúng ta có các định nghĩa sau, với α và β là những chuỗi: • ε là chuỗi rỗng • [x] là một chuỗi một phần tử duy nhất chứa x • α.β là một chuỗi tạo ra bằng cách thêm β vào α • α + là một dạng nghịch đảo (reflection) của α • # α là độ dài của α • αi là phần tử thứ i trong chuỗi α • list α(i, j) là một danh sách từ i tới j biểu diễn cho chuỗi α Ví dụ 2.8: minh họa danh sách liên kết đơn Chúng ta có thể định nghĩa bằng phương pháp quy nạp cho danh sách theo cấu trúc Phân tích MUST-MAY để kiểm tra chương trình 23 của α như sau: def list (i,j) emp i=j def list a (i, j ) j.9: minh họa xóa phần tử đầu tiên của một danh sách { list a (i, k ) } { j. i 1 j list ( j , k ) } j:=[i+1]; { i a i 1 j list ( j , k ) } dispose i; {i 1 j list ( j , k )} dispose i+1; {list ( j , k )} i:=j {list (i, k )} Ngoài ra, separation logic còn dung cho những chương trình phức tạp hơn như đảo các phần tử của một danh sách Ví dụ 2.10: minh họa chương trình đảo các phần tử của một danh sách (nguồn [12]) Phân tích MUST-MAY để kiểm tra chương trình 24 Ví dụ 2.11: Biểu diễn danh sách liên kết đôi (doubly-linked list) (nguồn [12]) dlist α(i, i’, j, j’) biểu diễn danh sách liên kết đôi cho chuỗi α từ i đến j, và từ j’ ngược về i’ Định nghĩa quy nạp cho danh sách liên kết đôi như sau: def dlist (i, i’, j, j’) emp i=j i’=j’ def dlist a (i, i’, k, k’) j.
dlist i, i ' , j , j ' dlist j, j ' , k , k ' dlist b i, i ' , k , k ' j ' .3 Các tiên đề Phần này trình bày thêm các tiên đề cho phép suy luận trên separation logic dựa vào tiền điều kiện và hậu điều kiện, ngoài các tiền đề đã được giới thiệu trong Hoare logic. E E : F EF E dispose E emp x m x : cons E1 ,.4 : Các tiên đề áp dụng trên separation logic (nguồn [12]) x: = E là một phép gán bình thường giống như trong Hoare logic. • Tiên đề đầu tiên phát biểu rằng nếu E trỏ vào một ô nhớ có giá trị bất kỳ thì sau đó khi gán nội dung của ô nhớ mà E trỏ đến cho F, thì cuối cùng ta sẽ có nội dung tại ô nhớ E là F. Ý nghĩa của tiên đề này là một con trỏ chỉ trỏ tới một ô nhớ.
• Tiên đề thứ hai phát biểu rằng nếu chúng ta sử dụng hàm dispose(E), thì ô nhớ được trỏ bởi E sẽ được trả lại cho hệ thống. • Tiên đề thứ ba phát biểu rằng ban đầu, x được gán cho giá trị m trong store, tức x trỏ đến ô nhớ có địa chỉ m. Sau đó, x được gán cho k giá trị liền kề E1, .,Ek trong heap và x trỏ tới giá trị đầu tiên E1.
