Báo cáo Phương pháp kiểm chứng tính đúng đắn của một chương trình Java đa luồng thông qua sử dụng logic Hoare

- 1 - TRƯỜNG …………………. KHOA………………………. ---------- Báo cáo tốt nghiệp Đề tài: Phương pháp kiểm chứng tính đúng đắn của một chương trình Java đa luồng thông qua sử dụng logic Hoare - 2 - TÓM TẮT KHÓA LUẬN Có rất nhiều phương pháp để kiểm chứng tính đúng đắn của một chương trình Java đa luồng. Một trong các phương pháp đó là sử dụng logic Hoare. Kiểm chứng tính đúng đắn của một chương trình Java đa luồng sử dụng logic Hoare yêu cầu ta cần phải chứng minh một chương trình được bổ sung và chú thích dưới sự thi hành của các lệnh phải thỏa mãn: Nếu bước tính toán thi hành một phép gán, thì ta sử dụng các điều kiện tính đúng đắn cục bộ để chứng minh tính quy nạp của sự thi hành các thuộc tính của cấu hình cục bộ, và kiểm tra tính không có can thiệp đối với tất cả các cấu hình cục bộ khác và các bất biến lớp khác. Đối với giao tiếp, tính bất biến đối với thi hành các đối tác và bất biến toàn cục được chứng tỏ thông qua kiểm tra sự hợp tác đối với giao tiếp. Giao tiếp với chính nó không ảnh hưởng trạng thái toàn cục; tính bất biến của các thuộc tính còn lại dưới các quan sát tương ứng được chứng tỏ thông qua kiểm tra tính không có can thiệp. Cuối cùng, đối với tạo đối tượng, tính bất biến đối với bất biến toàn cục, tạo cấu hình cục bộ, bất biến lớp của đối tượng được tạo được đảm bảo các điều kiện của kiểm tra hợp tác đối với tạo đối tượng; tất cả các thuộc tính khác được chứng tỏ là bất biến thông qua sử dụng kiểm tra tính không có can thiệp. - 3 - MỤC LỤC TÓM TẮT KHÓA LUẬN................................................................................................- 1 - MỞ ĐẦU ..........................................................................................................................- 4 - CHƯƠNG 1. LOGIC HOARE ........................................................................................- 6 - 1.1. Logic vị từ ..................................................................................................................- 6 - 1.2. Các tiên đề của Logic Hoare .....................................................................................- 9 - 1.2.1. Các công thức đúng cú pháp cho chứng minh chương trình................................- 9 - 1.2.2. Tiên đề của phép gán............................................................................................- 10 - 1.2.3. Các quy tắc bổ sung..............................................................................................- 10 - CHƯƠNG 2. NGÔN NGỮ TUẦN TỰ ..........................................................................- 12 - 2.1. Cú pháp ...................................................................................................................- 13 - 2.2. Ngữ nghĩa ................................................................................................................- 16 - 2.2.1. Trạng thái và các cấu hình...................................................................................- 16 - 2.2.2. Các ngữ nghĩa toán tử ..........................................................................................- 18 - 2.3. Ngôn ngữ khẳng định..............................................................................................- 20 - 2.3.1. Cú pháp ................................................................................................................- 20 - 2.3.2. Ngữ nghĩa..............................................................................................................- 21 - 2.4. Hệ chứng minh ........................................................................................................- 25 - 2.4.1. Phác thảo chứng minh..........................................................................................- 26 - 2.4.2. Kiểm chứng các điều kiện ....................................................................................- 31 - CHƯƠNG 3. NGÔN NGỮ TƯƠNG TRANH .................... Error! Bookmark not defined. 3.1. Cú pháp ...................................................................................................................- 42 - 3.2. Ngữ nghĩa ................................................................................................................- 42 - 3.3. Hệ chứng minh ........................................................................................................- 43 - 3.3.1. Phác thảo chứng minh..........................................................................................- 43 - 3.3.2. Kiểm chứng các điều kiện ....................................................................................- 43 - CHƯƠNG 4. BỘ ĐIỀU PHỐI LẶP LẠI............................. Error! Bookmark not defined. 4.1. Cú pháp ...................................................................................................................- 47 - 4.2. Ngữ nghĩa ................................................................................................................- 47 - 4.3. Hệ chứng minh……………………………………………………………………….- 48- 4.3.1. Phác thảo chứng minh..........................................................................................- 49 - 4.3.2. Kiểm chứng các điều kiện ....................................................................................- 51 - CHƯƠNG 5. PHÉP TOÁN ĐIỀU KIỆN TRƯỚC YẾU NHẤT ..................................- 53 - 5.1. Các phép toán thay thế............................................................................................- 54 - 5.2. Kiểm chứng các điều kiện…………………………………………………………...- 54- CHƯƠNG 6. TÍNH ĐÚNG ĐẮN......................................... Error! Bookmark not defined. 6.1. Tính đúng đắn .........................................................................................................- 59 - KẾT LUẬN………………………………………………………………………………..- 62- TÀI LIỆU THAM KHẢO………………………………………………………………..- 63- - 4 - MỞ ĐẦU Yêu cầu của người dùng đối với một phần mềm ngày nay là không những nó phải có giao diện đẹp, tốc độ xử lý dữ liệu nhanh, tốc độ phản ứng của chương trình với người dùng cũng là một yêu cầu không thể bỏ qua. Một chương trình yêu cầu vừa có giao diện đẹp, vừa xử lý nhanh chạy trên một máy cấu hình bình thường thì cần có một cơ chế để quản lý cấp phát tài nguyên của máy một cách phù hợp. Và cơ chế quản lý đa luồng chính là một giải pháp cho các yêu cầu trên. Ngôn ngữ lập trình Java là một ngôn ngữ lập trình bậc cao hỗ trợ rất mạnh cho lập trình đa luồng, được sử dụng nhiều trong các hệ thống lớn cũng như trong các phần mềm có quy mô vừa và nhỏ. Trong các hệ thống lớn, chỉ một lỗi rất nhỏ cũng có thể dẫn tới những kết quả tai hại, hoặc thậm chí là phá hủy hệ thống. Do đó ta thấy được tính quan trọng đối với việc kiểm chứng tính đúng đắn của một chương trình. Việc kiểm chứng tính đúng đắn của một chương trình Java đa luồng là không thể thiếu được trong việc phát triển hệ thống. Ta cần có một phương pháp kiểm chứng tính đúng đắn của một chương trình Java đa luồng. Đó chính là phương pháp thông qua sử dụng logic Hoare. Logic Hoare là một hệ thống hình thức được phát triển bởi các nhà khoa học máy tính Anh C.A.R.Hoare, và về sau được cải tiến bởi Hoare và các nhà nghiên cứu khác. Mục đích của hệ thống này là cung cấp một tập các quy tắc logic để lý luận về tính đúng đắn của các chương trình máy tính với tính chính xác của các logic toán học. Logic Hoare là cơ sở để định nghĩa tính đúng đắn của hệ thống. Trong khóa luận tốt nghiệp này em sẽ trình bày về phương pháp kiểm chứng tính đúng đắn của một chương trình Java đa luồng thông qua sử dụng logic Hoare. Khóa luận sẽ có sáu chương với nội dung chính như sau:  Chương 1: Logic Hoare  Chương 2: Ngôn ngữ tuần tự - 5 -  Chương 3: Ngôn ngữ tương tranh  Chương 4: Bộ điều phối lặp lại  Chương 5: Phép toán trước yếu nhất  Chương 6: Tính đúng đắn Tuy nhiên do còn nhiều hạn chế về thời gian cũng như kiến thức của bản thân, khóa luận này không thể tránh khỏi những thiếu sót. Em rất mong nhận được sự quan tâm góp ý của các thầy, cô giáo cũng như các anh, chị và các bạn, những người quan tâm đến vấn đề này. Em xin chân thành cảm ơn thầy giáo, tiến sỹ Đặng Văn Hưng, người đã hướng dẫn trực tiếp, động viên và giúp đỡ em rất nhiều để hoàn thành khóa luận này. Cuối cùng, em xin bày tỏ lòng biết ơn sâu sắc tới gia đình, bạn bè, các thầy cô giáo, những người đã quan tâm, giúp đỡ em rất nhiều trong suốt những năm ngồi trên ghế nhà trường. Hà Nội, tháng 5 năm 2009 Sinh viên LÊ VĂN VIỄN - 6 - CHƯƠNG 1. LOGIC HOARE 1.1. Logic vị từ Định nghĩa: Vị từ là một hàm nhận một giá trị Bool. Một vị từ thực sự là một giá trị logic được biểu hiện bằng tham số. Nó có thể đúng với một số đối số, và sai với một số đối số khác. Chẳng hạn x > 0 là một vị từ với một đối số, ta có thể đặt tên nó là gt0(x). Do vậy mà gt0(5) là đúng và gt0(0) là sai. Định nghĩa: Các thành phần của logic vị từ wffs gồm có các thành phần sau: • Các định danh biến – một tập (thường là vô hạn) của các tên biến, thường là ...,,,...,,,, 2121 yyyxxx • Các định danh hằng – một tập (hữu hạn, vô hạn, hoặc rỗng) của các tên hằng, thường là ...,,...,,,, 2121 bbbaaa • Các định danh vị từ – một tập (không rỗng) của các tên vị từ, thường là ...,,...,,,, 2121 qqqppp • Các định danh hàm – một tập các tên hàm, thường là ...,,,...,,,, 2121 gggfff Mỗi định danh hàm và định vị từ có một số cố định của các đối số mà nó chấp nhận là arity. Định nghĩa: Các toán hạng của logic vị từ được định nghĩa một cách đệ quy như sau: (i) các tên biến và các tên hằng là toán hạng, và (ii) nếu ktt ,...,1 là các toán hạng và f là một tên hàm có số các đối số cố định là k, thì  ktttf ...,,, 21 là một toán hạng - 7 - Một toán hạng không chứa các biến được gọi là toán hạng cơ sở. Định nghĩa: nếu ktt ,...,1 là các toán hạng và vị từ p có số của các đối số cố định là k, thì  ktttp ...,,, 21 là một công thức nguyên tử của logic vị từ. Các phép toán logic thêm vào trong logic vị từ là lượng hóa phổ biến  x đọc là với mọi x, và lượng hóa tồn tại, x đọc là tồn tại x. Trong sơ đồ ưu tiên để tránh các dấu ngoặc trong các công thức,  có độ ưu tiên thấp nhất trong các liên kết. Định nghĩa: Các công thức đúng ngữ pháp (wffs) của logic vị từ được định nghĩa đệ quy như sau: (i) mỗi công thức nguyên tử là một công thức đúng ngữ pháp wff, và (ii) nếu  và  là wffs và x là một tên biến, thì mỗi công thức sau đây cũng là một công thức đúng ngữ pháp: • (  ) •    • ( .x ) •    •  .x •    •    Hai phép toán lượng hóa cung cấp một ngữ nghĩa không thể thiếu được để biểu diễn các khẳng định về các kết quả chân lý của các vị từ. Sự thể hiện của mỗi phép toán trong các phép toán logic phụ thuộc vào hiểu biết về không gian từ đó các giá trị của các biến có thể được đưa ra. Nếu không gian này là hữu hạn, nói rằng  kccc ...,,, 21 , thì những phép toán logic mới này có thể được biểu thị bằng cách sử dụng các quan hệ logic mệnh đề. Một công thức  .x thì tương đương với sự kết hợp của các công thức đúng ngữ pháp đạt được bằng sự thay thế x bởi mỗi phần tử của các phần tử trong không gian (ví dụ,        ycpycpycpyxpx k ,...,,,. 21  ). Tương tự như vậy một công thức .x tương đương với sự tách rời của các công thức wffs đạt được bởi thay thế x bằng mỗi phần tử của các phần tử của không gian (ví dụ        ycpycpycpyxpx k ,...,,,. 21  ). Các phép toán lượng hóa này yêu cầu ta phân biệt cách sử dụng của các biến. Chẳng hạn, công thức p(x) có một tham biến x, và nó có thể đúng với một số giá trị và sai với một số giá trị khác. Tuy nhiên, công thức )(. xpx thực sự không có tham biến - 8 - và thể hiện một giá trị duy nhất – giá trị x được gọi là biên trong trường hợp trước và tự do trong trường hợp sau. Nó minh họa hai vai trò khác nhau đối với các biến trong biểu thức đúng khuôn dạng logic mệnh đề do đó phải phân biệt cẩn thận. Định nghĩa: Các xuất hiện bị chặn của các biến trong .x là các xuất hiện bị chặn của các biến trong  , cộng thêm tất các xuất hiện của x trong  ,  được gọi là phạm vi của lượng hóa. Tất cả các xuất hiện của biến mà không bị chặn là các biến tự do. Tương tự định nghĩa áp dụng cho  .x . Một công thức đúng ngữ pháp wff được gọi là đóng nếu nó không có các xuất hiện của biến tự do. Định nghĩa: Một thể hiện i gồm có (i) Một tập D không rỗng – miền (hoặc không gian của các giá trị) (ii) Một phép gán  của • mỗi tên vị từ n đối số thành một quan hệ n vị trí trong D, • mỗi tên hàm n đối số thành một hàm n vị trí trong D, • mỗi định danh hằng thành một phần tử của D. Ta viết i =  ,D Một thể hiện là một toán hạng thể hiện nếu D là tất cả các toán hạng, và các phép gán đối với mỗi tên hàm là toán hạng khởi tạo tương ứng,     kk ttfttf ,...,,..., 11  . Định nghĩa: Một thể hiện được cho i =  ,D , một biến gán (hoặc trạng thái)  là hàm trong tập các biến V,  : V  D. Phép gán được mở rộng một cách đệ quy để mang một giá trị cho tất cả các toán hạng và các công thức, (i) đối với các toán hạng • với biến x,  xxval  )( , và đối với hằng c,  ccval  )( , • với một toán hạng phức hợp ))(),...,()(()),...,(( 11 kk tvaltvalfttfval   (ii) đối với các công thức • đối với một công thức nguyên tử ))(),...,()((),...,(( 11 kk tvaltvalpttpval   • đối với các công thức phức hợp )()(   valval  - 9 - )()()(   valvalval  )()()(   valvalval  )()()(   valvalval  )()()(   valvalval      .xval true nếu   trueval  ' đối với mỗi ' trong đó    yy  ' đối với xy  , false nếu ngược lại.     .xval true nếu   trueval  ' đối với mỗi ' trong đó    yy  ' đối với xy  , = false nếu ngược lại. Hai định nghĩa cuối cùng này biểu thị rằng, cho một thể hiện và một trạng thái, chỉ có một giá trị duy nhất được quyết định cho mỗi toán hạng và mỗi công thức bởi việc ước lượng mỗi phép toán logic. Điều này cung cấp các giá trị đúng ta sử dụng phân loại các công thức. Định nghĩa: Cho  là một biểu thức hợp khuân dạng wff, i là một thể hiện, và  là một trạng thái. Thì thỏa mãn  dưới i, i | nếu )(val = true. Biểu thức hợp khuân dạng  là đúng trên i, |i , nếu mọi trạng thái thỏa mãn  dưới i, và i được gọi là mô hình của  ,  là sai trên i nếu không có trạng thái nào thỏa mãn  dưới i. Một thể hiện được gọi là mô hình của một tập các biểu thức hợp khuân dạng nếu nó là mô hình của từng biểu thức hợp khuân dạng wff trong tập, và nếu nó là một thể hiện toán hạng, thì nó được gọi là một mô hình toán hạng. Định nghĩa: Một công thức đúng ngữ pháp wff là đúng logic (công thức hằng đúng) nếu nó đúng trên mọi thể hiện, có thể thỏa mãn nếu tồn tại một thể hiện và trạng thái thỏa mãn nó, và ngược lại nếu nó là không thể thỏa mãn. Định nghĩa: Một công thức đúng ngữ pháp wff là một hệ quả logic của một tập các công thức đúng ngữ pháp  ,  | , nếu mọi thể hiện và trạng thái thỏa mãn mỗi  ,  và  là tương đương logic,   nếu với mọi thể hiện và trạng thái  , )()(   valval  1.2. Các tiên đề của Logic Hoare 1.2.1. Các công thức đúng cú pháp cho chứng minh chương trình - 10 - Các công thức ta viết sẽ xác nhận các thuộc tính của các chương trình (các đoạn chương trình thực sự). Do vậy, các công thức phải bao gồm các xác nhận và chương trình tới công thức mà nó gắn liền. Các xác nhận chương trình (wffs) có dạng     P gồm 3 thành phần: • P là một đoạn chương trình - một lệnh (có thể phức hợp), và •  và  là các công thức logic vị từ sử dụng các tên biến và hàm/thao tác của chương trình, các ký hiệu {, } là các siêu ký hiệu được sử dụng để biểu thị bắt đầu và kết thúc của các công thức logic vị từ, và không nên hiểu như là các ký hiệu trong ngôn ngữ lập trình. Công thức logic  được gọi là điều kiện trước, và  được gọi là điều kiện sau. 1.2.2. Tiên đề của phép gán Ta giả thiết rằng :X biểu thị một lệnh gán, trong đó X là một biến và  là một biểu thức thích hợp. Tiên đề của phép gán nằm dưới hệ thống logic để chứng minh các chương trình không điều kiện. Tiên đề của phép gán:     PXXP   :| trong đó P là một công thức logic vị từ, X là một biến,  là một biểu thức, và  XP là công thức P với mỗi lần xuất hiện của X được thay thế bởi  . Một bước chứng minh được xác nhận bởi việc chứng minh cú pháp công thức tương ứng. Tuy nhiên ta không phân biệt các công thức mà chúng tương đương logic. Độ mạnh của các công thức đúng ngữ pháp Nếu P và Q là các công thức đúng ngữ pháp mà QP  , thì ta nói rằng P là một xác nhận mạnh hơn Q, và Q thì yếu hơn P. Một điều kiện mạnh hơn là một điều kiện mà nhiều – ít hơn các giá trị thỏa mãn một điều kiện mạnh hơn. 1.2.3. Các quy tắc bổ sung Tiên đề Skip    PskipP| với P là một công thức logic mệnh đề bất kỳ. Bằng trực giác, vì skip không làm gì, nên cái gì đúng sau sự thực hiện của nó thì cũng như là cái đã đúng trước đó. - 11 - Các quy tắc bổ trợ Độ mạnh của điều kiện trước Đó là quy tắc đầu tiên của các quy tắc suy luận trong hệ chứng minh chương trình. Ý kiến một cách trực quan là nếu một xác nhận chương trình có thể được chứng minh, thì điều kiện trước có thể được thay thế bởi bất kỳ công thức nào kéo theo nó.        RP QPRQ    |,|  là một đoạn chương trình bất kỳ. Độ yếu của điều kiện sau Đó là quy tắc tiếp theo của các quy tắc suy luận trong hệ thống chứng minh chương trình. Ý kiến một cách trực quan là nếu một xác nhận chương trình có thể được chứng minh, thì điều kiện sau có thể được thay thế bởi bất kỳ công thức nào nó kéo theo.        RP RQQP     | |,|  là một đoạn chương trình bất kỳ. Quy tắc tuần tự            RCCP RCQQCP 21 21 ;| |,|   Quy tắc điều kiện            RCelseCthenBifP RCBPRCBP 21 21 | |,|   Quy tắc while        BPCdoBwhileP PCBP   | | - 12 - Tính đúng đắn: nếu    QSP có thể được chứng minh, thì điều tất nhiên là thực hiện S từ một trạng thái thỏa mãn P sẽ chỉ kết thúc trong các trạng thái thỏa mãn Q. Để mô tả rõ ràng về hệ chứng minh, ta trình bày hệ chứng minh tăng dần trong các mức: Ta bắt đầu với một hệ chứng minh đối với ngôn ngữ con tuần tự của Java, cho phép tạo đối tượng và thi hành phương thức động. Ở cấp này biểu thị cách để quản lý các hoạt động của một luồng duy nhất. Trong mức thứ hai, ta cho phép thêm vào tạo đối tượng động, dẫn tới sự thi hành đa luồng. Hệ chứng minh tương ứng mở rộng hệ chứng minh trong ngôn ngữ seqJava với các điều kiện quản lý tạo luồng động và theo các khía cạnh chen ngang vào. Cuối cùng, ta tích hợp kỹ thuật quản lý đồng bộ hóa của Java. Quản lý đồng bộ hóa cho phép thi hành các loại trừ lẫn nhau trên đối tượng. - 13 - CHƯƠNG 2. NGÔN NGỮ TUẦN TỰ 2.1. Cú pháp Đối với mỗi kiểu, miền giá trị tương ứng được trang bị với một tập hợp chuẩn các toán tử với phần tử điển hình f. Mỗi toán tử f có một kiểu duy nhất ttt n 1 và một thể hiện cố định của f, trong đó các hằng là các toán tử không có tham biến. Đối với các biến, ta phân biệt định nghĩa giữa các biến thể hiện và các biến cục bộ (tạm thời). Các biến thể hiện giữ trạng thái của một đối tượng và tồn tại suốt vòng đời của đối tượng. Các biến cục bộ được cấp phát trong bộ nhớ Stack; chúng thể hiện vai trò của các tham biến hình thức và các biến của các định nghĩa phương thức và chỉ tồn tại trong sự thi hành của phương thức chứa chúng. Ta định nghĩa IVar là tập các biến thể hiện với các phần tử x, và TVar là tập các biến cục bộ với các phần tử u, u’, v, … Cho Var = IVarTVar với phần tử điển hình y là tập các biến của chương trình., trong đó  là toán tử tập hợp tách rời nhau. Cú pháp trừu tượng: e ::= x | u | this | null | f (e, …, e) ::rete  | e stm ::= x := e | u:= e | u:= cnew | u := e.m (e, …,e) | e.m (e, …,e) | | stm; stm | if e then stm else stm fi | while e do stm od … meth ::= m (u, …, u) { stm; return rete } runmeth ::= run () { stm; return} class ::= class c { meth … meth} mainclass ::= class c { meth … meth runmeth } prog ::= class … class mainclass - 14 - Bên cạnh việc sử dụng biến cục bộ và biến thể hiện, các biểu thức Expe  được xây dựng từ biến tham chiếu đến chính nó this, tham chiếu rỗng là null, và từ các biểu thức con sử dụng các toán tử được cho. Để hỗ trợ một giao diện rõ ràng giữa hành vi bên trong và hành vi bên ngoài đối tượng, seqJava không cho phép các tham chiếu hạn chế tới các biến thể hiện. Chú ý rằng tất cả các biểu thức của ngôn ngữ không có ảnh hưởng, có nghĩa là, sự ước lượng của chúng không thay đổi trạng thái chương trình. Chỉ có sự thi hành của các lệnh có ảnh hưởng tới trạng thái chương trình. Các câu lệnh Stmstm  , cho phép các phép gán, tạo đối tượng, thi hành các phương thức, và các cấu trúc điều khiển chuẩn như là dãy các lệnh hợp thành, các lệnh điều kiện, và vòng lặp. Viết cho câu lệnh rỗng. Định nghĩa phương thức    retn ereturnstmuum ;...,,1 bao gồm một phương thức tên m, một danh sách các tham biến hình thức nuu ...,,1 , và thân phương thức của dạng stm; return rete , có nghĩa là, ta yêu cầu rằng các thân của phương thức được kết thúc bởi một câu lệnh trả về duy nhất có dạng return hoặc là return e, trả về sự điều khiển và có thể trả về một giá trị. Nhiều khi ta bỏ qua các câu lệnh trả về mà không có giá trị trả về trong các phương thức. Tập hợp cMeth chứa các phương thức của lớp c. Ta ký hiệu thân của phương thức m của lớp c là cmbody , . Thỉnh thoảng ta đề cập rõ ràng đến các kiểu của giá trị trả về và các tham số hình thức theo kiểu Java t  nn ututm ...,,11 Một lớp được định nghĩa bằng tên c của nó và các phương thức, trong đó tên của các phương thức được đảm bảo khác nhau. Một chương trình là một tập hợp của các định nghĩa lớp có các tên lớp khác nhau, trong đó một lớp chính mainclass định nghĩa bằng phương thức run của nó. Ta gọi thân của phương thức run của lớp chính là câu lệnh chính của chương trình. Phương thức run không thể bị gọi. Tập các biến thể hiện cIVar của một lớp c được cho một cách rõ ràng bởi các biến thể hiện xuất hiện trong lớp; khai báo tập các biến cục bộ của phương thức cũng được đưa ra một cách tương tự. Trong các ví dụ ta nhiều khi định nghĩa một cách rõ ràng biến thể hiện và biến cục bộ theo kiểu Java: khai báo t y; trong các lớp bên ngoài các định nghĩa phương thức khai báo y là một biến thể hiện của kiểu t của lớp, trong khi đó nếu khai báo bên trong của một phương thức chỉ rõ y là một biến cục bộ. Bên cạnh các rút gọn của các kiểu đã được đề cập, do các nguyên nhân kỹ thuật đã dẫn tới các giới hạn sau: Ta yêu cầu các lệnh thi hành phương thức chỉ chứa các biến cục bộ, nghĩa là, không có các biểu thức nee ...,,0 trong một lời gọi hàm - 15 -  neeme ...,,. 10 chứa các biến thể hiện. Ngoài ra, các tham biến hình thức phải không xuất hiện bên phía trái của các phép gán. Các giới hạn này kéo theo trong suốt quá trình thi hành của một phương thức các giá trị của các tham biến thực sự và hình thức không bị thay đổi. Cuối cùng, kết quả của việc tạo các đối tượng và thi hành các phương thức có thể không bị gán cho các biến thể hiện. Hạn chế này cho phép một hệ chứng minh với kiểm chứng các điều kiện riêng biệt cho tính không có can thiệp và tính hợp tác. class C { int x1; void m1 (C o) { x1 := o.m2 (x1); return } int m2 (int u) { return u + 1 } } Sự biến đổi sau đây thỏa mãn các yêu cầu, nhưng chèn thêm các điểm điều khiển trước và sau khi gọi phương thức trong m1: class C { int x1; void m1 (C o) { int u, v; u := x1; - 16 - v := o.m2 (u); x1 := v; return } int m2 (Int u) { return u + 1 } } 2.2. Ngữ nghĩa 2.2.1. Trạng thái và các cấu hình Cho tVal là các miền rời nhau với các kiểu khác nhau t. Đối với lớp có tên là c, các tập rời nhau cVal với các phần tử điển hình là ...,, biểu thị các tập vô hạn của các định danh đối tượng. Giá trị của null trong kiểu c là cc Valnull  . Nói chung ta chỉ viết null, khi c là rõ ràng từ ngữ cảnh. Ta đinh nghĩa nullcVal là  cc nullVal  , và tương ứng đối với các kiểu hợp thành. Tập tất cả các giá trị có thể không null tt Val được viết là Val, và nullVal biểu thị nulltt Val . Cho Init : nullValVar  là một hàm gán một giá trị khởi tạo cho mỗi biến Vary  , nghĩa là, null, false, và 0, cho lớp, giá trị kiểu logic, và các kiểu số nguyên, và tương ứng cho các kiểu hợp thành. Ta định nghĩa biến this Var , là một tham chiếu tới chính nó không phải trong miền của Init. Cấu hình của một chương trình bao gồm tập hợp của các đối tượng đang tồn tại cùng với giá trị của các biến thể hiện của chúng, và cấu hình của luồng đang thi hành. Trước khi hình thức hóa các cấu hình toàn cục của một chương trình, ta định nghĩa các trạng thái cục bộ và các cấu hình cục bộ. Một trạng thái cục bộ  loc của sự thi hành một phương thức giữ giá trị của các biến cục bộ của phương thức và được mô hình hóa như là một hàm bộ phận của kiểu nullValTVar  . Ta tham chiếu tới các trạng thái cục bộ của phương thức m của lớp c bởi cm, . Trạng thái cục bộ ban đầu initcm, gán cho mỗi biến cục bộ u từ miền của nó giá trị Init(u). Một cấu hình cục bộ  stm,, của một phương thức của đối tượng - 17 - null chỉ rõ, thêm vào trạng thái cục bộ  , điểm thi hành của nó được biểu diễn bởi câu lệnh stm. Một cấu hình luồng  là một ngăn xếp của các cấu hình cục bộ  000 ,, stm  111 ,, stm …  nnn stm,,  , mô tả dãy của các sự thi hành phương thức của luồng được cho. Ta viết  stmo ,, có nghĩa là đẩy một cấu hình cục bộ mới vào trong ngăn xếp. Các đối tượng được mô tả đặc điểm bởi các trạng thái thể hiện  instinst của kiểu   nullValthisIVar  sao cho nó ở trong miền  instdom  của inst . Ta viết instc để ký hiệu các trạng thái của các thể hiện của lớp c. Các ngữ nghĩa sẽ duy trì   cinstc Valthis  bất biến. Trạng thái thể hiện ban đầu initc inst , gán một giá trị từ cVal tới this, và tới mỗi biến thể hiện x còn lại của nó giá trị Init(x). Một trạng thái toàn cục  của kiểu  instcc Val lưu trữ đối với mỗi đối tượng đang tồn tại hiện thời, nghĩa là, một đối tượng đang thuộc về miền của , trạng thái thể hiện của đối tượng. Tập các đối tượng đang tồn tại của kiểu c trong một trạng thái  được cho bởi  cVal , và        ccnullc nullValVal  . Đối với các kiểu còn lại,  tVal và  tnullVal được định nghĩa tương ứng. Ta tham chiếu tới tập  tt Val bởi  Val ;  nullVal biểu thị   t nullt Val . Trạng thái thể hiện của một đối tượng   cVal được cho bởi   với thuộc tính bất biến   this . Ta yêu cầu rằng, một trạng thái toàn cục được cho, không có biến thể hiện nào trong bất kỳ các đối tượng đang tồn tại nào tham chiếu tới một đối tượng không tồn tại, nghĩa là,      nullValx  cho tất cả các lớp c và các đối tượng   cVal . Một cấu hình toàn cục ,T mô tả các đối tượng hiện thời qua trạng thái toàn cục  , tập T chứa cấu hình của luồng đang thi hành. Đối với các ngôn ngữ tương tranh của các phần sau, T sẽ là một tập các cấu hình của tất cả các luồng đang thi hành hiện thời. Tương ứng với giới hạn trong các trạng thái toàn cục, ta yêu cầu rằng các cấu hình cục bộ  stm,, trong ,T chỉ tham chiếu tới các định danh đối tượng đang tồn tại, nghĩa là,   Val và   nullValu )( đối với tất cả các u từ miền của  . Trong phần tiếp theo, ta viết   Tstm ,, nếu tồn tại một cấu hình cục bộ  stm,, trong một ngăn xếp của các ngăn xếp thi hành của T. - 18 - Hàm ngữ nghĩa      nulllocinst ValExp :_ _,_ ước lượng trong ngữ cảnh của một trạng thái thể hiện cục bộ   ,inst các biểu thức đang chứa các biến từ     domdom inst  , dom (f) biểu thị miền của hàm f. Các biến thể hiện x và các biến cục bộ u được ước lượng lần lượt là  xinst và  u , biến this ước lượng là  thisinst , và null có tham chiếu null như giá trị.    xx instinst  ,    uu inst  ,    thisthis instinst  ,   nullnull inst  ,         ,,1,1 ...,,...,, instinstinst nn eefeef  Ta biểu diễn bằng  vu  trạng thái cục bộ gán giá trị v cho u;  vxinst  được định nghĩa một cách tương tự, trong đó  vxinst . cho kết quả từ  bằng cách gán v cho biến thể hiện x của đối tượng   Val . Ta sử dụng những toán tử này một cách tương tự cho các vector của các biến. Ta cũng sử dụng  vy  cho các dãy biến bất kỳ;  vyinst . và  vy . được định nghĩa tương tự. Cuối cùng, đối với các trạng thái toàn cục,  inst  bằng với  trừ đi  ; trong trường hợp   Val , toán tử mở rộng tập các đối tượng đang tồn tại bởi  , có trạng thái thể hiện của nó được khởi tạo cho inst . 2.2.2. Các ngữ nghĩa toán tử Trước khi có một cái nhìn chặt chẽ về các quy tắc ngữ nghĩa cho phép biến đổi quan hệ  , ta bắt đầu bằng định nghĩa về điểm vào của một chương trình. Cấu hình ban đầu 00 , T của một chương trình thỏa mãn         thisdom initcinst ,00 ,  , và   cruncruninit bodyT ,,0 ,,  , trong đó c là lớp chính, và cVal là đối tượng ban đầu. - 19 - Ta gọi một cấu hình ,T của một chương trình là có thể đạt được nếu tồn tại một tính toán  ,, 00 TT  sao cho 00 ,T là cấu hình ban đầu của chương trình và  là bao đóng bắc cầu phản thân của  . Một cấu hình cục bộ   Tstm ,, được cho phép trong ,T , nếu nó có thể được thi hành, nghĩa là, nếu có một bước tính toán ',',  TT  đang thi hành stm trong trạng thái cục bộ  và đối tượng  .            instASSexstmTstmexT  ,.,,,,;:,,              locASSstmeuTstmeuT   ,,,,;:,, ,               NEWstmuTstmnewuT thisValVal c instinst initc inst c ',,,,;:,, '\ ,          cMethbodyum                   CALLstmemT euVale cminit c        ,;.e:u,, ' 0 ,,, 0        ,,',;u,, bodystmreceiveT             RETURN ereturnstmureceiveT eu retret retret   ,',;,, '' ',         ,,'', stmT        run RETURN TreturnT  ,,,,,,   - 20 - Các phép gán tới các biến thể hiện hoặc các biến cục bộ cập nhật trạng thái thành phần tương ứng, có nghĩa là, cả trạng thái thể hiện và trạng thái cục bộ (quy tắc instASS và quy tắc locASS ). Tạo đối tượng bằng lệnh cnewu : tạo một đối tượng mới của kiểu c với một định danh mới được lưu trữ trong biến cục bộ u, và khởi tạo các biến thể hiện của đối tượng mới. Thi hành một phương thức mở rộng lời gọi dãy bằng một cấu hình cục bộ mới (quy tắc CALL). Ta sử một câu lệnh phụ trợ receive u để nhớ biến mà trong đó kết quả của phương thức được gọi sẽ được lưu trữ lúc trả về. Sau khi khởi tạo trạng thái cục bộ và truyền các tham biến, luồng bắt đầu thi hành các lệnh trong thân của phương thức. Khi trả về từ một lời gọi phương thức, phương thức được gọi ước lượng biểu thức trả về và chuyển nó cho phương thức gọi, sau đó phương thức gọi cập nhật trạng thái cục bộ của nó. Thân phương thức kết thúc sự thi hành của nó và phương thức gọi có thể tiếp tục. Luồng đang thi hành kết thúc vòng đời của nó thông qua sự trả về từ phương thức run của đối tượng ban đầu (quy tắc runRETURN ). 2.3. Ngôn ngữ khẳng định Logic khẳng định bao gồm một ngôn ngữ con cục bộ và một ngôn ngữ con toàn cục. Các khẳng định cục bộ mô tả các trạng thái thể hiện cục bộ, và được sử dụng để chú thích các phương thức trong các toán hạng của các biến cục bộ và của các biến thể hiện của lớp mà chúng thuộc về. Các khẳng định toàn cục mô tả trạng thái toàn cục, nghĩa là, toàn bộ một hệ thống của các đối tượng và các cấu trúc giao tiếp của nó. 2.3.1. Cú pháp Trong ngôn ngữ của các khẳng định, ta giới thiệu một tập vô hạn LVar của các biến logic với phần tử điển hình là z , trong đó ta giả thiết rằng các biến thể hiện, các biến cục bộ và con trỏ this không nằm trong LVar. Ta sử dụng tLVar cho tập các biến logic của kiểu t. Các biến logic được sử dụng để lượng hóa trong cả ngôn ngữ cục bộ và ngôn ngữ toàn cục. Bên cạnh đó, chúng còn được sử dụng như là các biến tự do để biểu diễn các biến cục bộ trong ngôn ngữ khẳng định toàn cục: Để biểu diễn một thuộc tính cục bộ trong mức toàn cục, mỗi biến cục bộ trong một khẳng định cục bộ được cho sẽ được thay thế bởi một biến logic mới. Các biểu thức cục bộ LExpe  là các biểu thức của ngôn ngữ lập trình có thể chứa các biến logic. Tập các biểu thức cục bộ của kiểu t được ký hiệu bởi tLExp . Một cách lạm dụng ký hiệu, ta sử dụng e, e’, … không những cho các biểu thức chương trình mà còn cho các phần tử điển hình của các biểu thức cục bộ. Các khẳng định cục bộ LAssqpp ...,,,', là các công thức logic chuẩn thông qua các biểu thức logic cục - 21 - bộ. Ta cho phép ba dạng của lượng hóa thông qua các biến logic: Lượng hóa tồn tại pz. chỉ được cho phép đối với các miền không có các tham chiếu đối tượng, nghĩa là, kiểu của z được yêu cầu là các kiểu Int, Bool, hoặc là một kiểu hợp thành được xây dựng từ các kiểu này. Đối với các kiểu tham chiếu c, dạng này của lượng hóa không được cho phép, do vậy đối với các kiểu tham chiếu, sự tồn tại của một giá trị phụ thuộc động vào trạng thái toàn cục. Không cho phép lượng hóa tồn tại đối với các kiểu đối tượng đảm bảo rằng giá trị của một khẳng định cục bộ thực sự chỉ phụ thuộc vào các giá trị của các biến thể hiện và các biến cục bộ, mà không phụ thuộc vào trạng thái toàn cục. Tuy nhiên, một dạng lượng hóa có thể khẳng định sự tồn tại của các đối tượng trong mức cục bộ thỏa mãn một vị từ, dạng được cung cấp là rõ ràng về tập các đối tượng. Do vậy, các lượng hóa tồn tại pez . và pez . khẳng định sự tồn tại của một phần tử, theo thứ tự, sự tồn tại của một dãy con của một dãy được cho e, sao cho với một thuộc tính mà p đúng. Các biểu thức toàn cục GExpEE ...,', được xây dựng từ các biến logic, null, các biểu thức toán tử, và các tham chiếu hạn chế E.x tới các biến thể hiện x của các đối tượng E. Ta viết tGExp đối với tập các biểu thức toàn cục của kiểu t. Các khẳng định toàn cục GAssQP ...,, là các công thức logic thông qua các biểu thức logic toàn cục. Không giống như ngôn ngữ cục bộ, ngữ nghĩa của một biểu thức toàn cục được định nghĩa trong ngữ cảnh của một trạng thái toàn cục. Do vậy lượng hóa tồn tại được cho phép đối với tất cả các kiểu và được thể hiện cho các dãy thông qua tập các giá trị đang tồn tại và null, nghĩa là, tập các giá trị  nullVal  trong một cấu hình toàn cục ,T Nhiều khi ta viết lượng hóa thông qua các giá trị kiểu t trong dạng   ptz .: tạo sự rõ ràng cho miền lượng hóa; ta cũng sử dụng cùng ký hiệu trong ngôn ngữ toàn cục. Sử dụng pz . thay cho pz  . . 2.3.2. Ngữ nghĩa Các biến logic được thể hiện tương đối tới môi trường logic  , đó là, một hàm cục bộ của kiểu nullValLVar , gán các giá trị cho các biến logic. Ta ký hiệu bằng  vz  môi trường logic gán các giá trị v cho các biến z . Tương tự như vậy đối với các cập nhật trạng thái cục bộ và trạng thái thể hiện, ta cũng sử dụng  vy cho các dãy biến tùy y để biểu diễn môi trường logic gán cho mỗi biến logic trong y giá trị - 22 - tương ứng trong v . Đối với một môi trường logic  và một trạng thái toàn cục  , ta nói rằng  chỉ tham chiếu tới các giá trị đang tồn tại trong  , nếu     nullValz  đối với tất cả  domz . Thuộc tính này phù hợp với định nghĩa của lượng hóa trong đó các dãy chỉ thông qua các giá trị đang tồn tại và null, và trong thực tế, trong các cấu hình cục bộ có thể đạt tới được các biến chỉ có thể tham chiếu tới các giá trị đang tồn tại hoặc là null. Hàm ngữ nghĩa     ,,_ L của kiểu    nulllocinst ValLAssLExp     ước lượng các biểu thức cục bộ và các khẳng định cục bộ trong ngữ cảnh của một môi trường logic  và một trạng thái thể hiện cục bộ   ,inst . Hàm ước lượng được định nghĩa cho các biểu thức và các khẳng định chỉ chứa các biến từ       domdomdom inst  . Trạng thái thể hiện cục bộ cung cấp ngữ cảnh đối với ngữ nghĩa cho các biểu thức ngôn ngữ lập trình do vậy được định nghĩa bởi hàm ngữ nghĩa     ,,_  ; môi trường logic ước lượng các biến logic. Một lượng hóa tồn tại pz . với tLVarz ước lượng là đúng trong môi trường logic  và trạng thái thể hiện cục bộ   ,inst khi và chỉ khi tồn tại một giá trị tValv sao cho p đúng trong môi trường logic  vz và trạng thái thể hiện cục bộ   ,inst , trong đó đối với kiểu t của z chỉ có kiểu Int, Bool, hoặc các kiểu hợp thành được xây dựng từ hai kiểu này là được cho phép. Sự ước lượng của một lượng hóa tồn tại pez . với tLVarz và tlistLExpe được định nghĩa tương tự, trong đó sự tồn tại của một phần tử trong dãy được yêu cầu. Một khẳng định pez . với tlistLVarz và tlistLExpe chỉ rõ sự tồn tại của một dãy con của e sao cho p đúng. Trong phần sau ta cũng viết    truepchop instLLinst   ,,|,, (L thỏa mãn vị từ p dưới thể hiện i(  ,, inst )). pL| ta phát biểu rằng pLinst |,,  đúng đối với các môi trường logic bất kỳ, các trạng thái thể hiện bất kỳ, và các trạng thái cục bộ bất kỳ.     zz instL  ,,     xx instL inst  ,,     uu instL  ,,     thisthis instL inst  ,, - 23 -    nullnull instL  ,,            ,,,,1,,1 ...,,...,, instinstinst LnLLn eefeef     truep instL   ,, khi và chỉ khi    falsep instL  ,,    truepp instL   ,,21 khi và chỉ khi    truep instL  ,,1 và    truep instL  ,,2    truepz instL   ,,. khi và chỉ khi      truep instvzL  ,, với nullValv    truepez instL   ,,. khi và chỉ khi      truepez instvzL   ,, với nullValv    truepez instL   ,,. khi và chỉ khi      truepez instvzL   ,, với nullValv Bởi vì các khẳng định toàn cục không chứa các biến cục bộ và các tham chiếu không hạn chế tới các biến thể hiện, nên các ngữ nghĩa của các khẳng định toàn cục không tham chiếu tới các trạng thái thể hiện cục bộ nhưng tới các trạng thái toàn cục. Hàm ngữ nghĩa     ,,G của kiểu    nullValGAssGExp    , cho các biểu thức toàn cục và các khẳng định toàn cục ngữ nghĩa trong ngữ cảnh của một môi trường logic  và một trạng thái toàn cục  . Để đúng theo định nghĩa,  được yêu cầu chỉ tham chiếu tới các giá trị đang tồn tại trong miền của  , và theo thứ tự biểu thức và khẳng định chỉ có thể chứa các biến tự do từ miền của  . Các biến logic, null, và các biểu thức toán tử được ước lượng tương tự như các khẳng định cục bộ. một biểu thức toàn cục E.x được cho bởi giá trị của biến thể hiện x của đối tượng được tham chiếu tới bởi biểu thức E. Sự ước lượng của một biểu thức E.x chỉ được định nghĩa nếu E tham chiếu tới một đối tượng đang tồn tại trong  . Chú ý rằng khi E và E’ tham chiếu tới cùng một đối tượng, đó là, E và E’ là các bí danh, thì E.x và E’.x biểu diễn cùng một biến. Các ngữ nghĩa của phép phủ định và phép hội là chuẩn. Một lượng hóa Pz . với tLValz  ước lượng đúng trong ngữ cảnh của  và  nếu P ước lượng đúng trong ngữ cảnh của  vz  và  , đối với giá trị  nulltValv  . Chú ý rằng lượng hóa chỉ thông qua các dãy các đối tượng thông qua tập của các đối tượng đang tồn tại và null.     zz G  ,    nullnull G  , - 24 -            ,,1,1 ...,,...,, GnGGn EEfEEf          xExE GG   ,,.         falsePkhichivàkhitrueP GG   ,,            truePvàtruePkhichivàkhitruePP GGG   ,2,1,21           nullGG ValvvoitruePkhichivàkhitruePz  ,,. Đối với một trạng thái toàn cục  và một môi trường logic  đang tham chiếu chỉ tới các giá trị đang tồn tại trong  ta viết PG|, khi P là đúng trong ngữ cảnh của  và  . Ta viết PG| nếu P đúng đối với các trạng thái toàn cục và các môi trường logic  bất kỳ đang tham chiếu chỉ tới các giá trị đang tồn tại trong  . Để biểu thị một thuộc tính cục bộ p trong ngôn ngữ khẳng định toàn cục, ta định nghĩa sự thay thế nâng lên  thiszp / bởi thay thế đồng thời trong p tất cả các lần xuất hiện của tham chiếu tới chính nó – con trỏ this bằng biến logic z, được đảm bảo không xuất hiện trong p, và biến đổi tất cả các lần xuất hiện của các biến thể hiện x trong các tham chiếu hạn chế z.x. Để thuận tiện cho việc ký hiệu ta xem các biến cục bộ đang xuất hiện trong khẳng định toàn cục  thiszp / như là các biến logic. Các biến cục bộ này được thay thế bởi các biến logic mới. Đối với các lượng hóa tồn tại   thiszpz /.' sự thay thế áp dụng cho khẳng định p. Các lượng hóa tồn tại cục bộ được biến đổi trong các lượng hóa tồn tại toàn cục trong đó các quan hệ  và  được biểu thị ở mức toàn cục như là các toán tử.   zthiszthis /   xzthiszx ./    uthiszu /     thiszpzthiszpz /.'/.'         thiszpthiszezzthiszpez //'.'/.'         thiszpthiszezzthiszpez //'.'/.'  trong đó z là biến mới. Ta viết P (z) đối với  thiszp / , và tương tự cho các biểu thức. Sự thay thế này sẽ được sử dụng để kết hợp các thuộc tính của các trạng thái thể hiện cục bộ trong mức toàn cục. Sự thay thế bảo toàn ngữ nghĩa của các khẳng định - 25 - cục bộ, ngữ nghĩa của các biến cục bộ đã được cung cấp được biểu diễn trùng khớp bởi môi trường logic: Bổ đề 2.3.1. (Sự thay thế nâng lên) Cho  là một trạng thái toàn cục,  và  một môi trường logic và trạng thái cục bộ, cả hai đang tham chiếu chỉ tới các giá trị đang tồn tại trong  . Hơn nữa cho p là một khẳng định cục bộ đang chứa các biến cục bộ u . Nếu    uu   và z là một biến logic mới, thì  thiszpG /|,  khi và chỉ khi    pz L|,,  2.4. Hệ chứng minh Chứng minh tính đúng đắn của một thuộc tính của chương trình gồm có ba bước. Đầu tiên, thuộc tính được yêu cầu phải được chỉ rõ bởi sự bổ sung và chú thích chương trình, nghĩa là, bằng sự bổ sung chương trình với các biến phụ trợ không ảnh hưởng đến luồng điều khiển của chương trình gốc, và bằng sự đính kèm các vị từ cho các cấu trúc chương trình cú pháp. Một chương trình được bổ sung và chú thích được gọi là một phác thảo chứng minh. Thứ hai, phác thảo chứng minh phải được áp dụng đối với phác thảo chứng minh riêng biệt, có kết quả là tập kiểm chứng các điều kiện. Cuối cùng, kiểm chứng các điều kiện phải được chứng minh. Để thuận lợi về mặt kỹ thuật, đầu tiên ta đưa ra kiểm chứng các điều kiện như là các bộ ba Hoare chuẩn của dạng    qstmp , trong đó stm là một phép gán bội hoặc là các thành phần tuần tự của các phép gán bội, đang biểu thị các cập nhật trạng thái. Trong kiểm chứng các điều kiện được đưa ra trong ngôn ngữ khẳng định cục bộ, các phép gán bội trong bộ ba Hoare có thể tham chiếu tới các biến thể hiện và cục bộ. Các phép gán trong các điều kiện toàn cục có thể sử dụng các biến logic và các tham chiếu hạn chế tới các biến thể hiện. Các lệnh trong các điều kiện toàn cục có thể sử dụng các biến logic và các tham chiếu hạn chế tới các biến thể hiện. Các biến cục bộ được biểu thị trong ngôn ngữ toàn cục bởi các biến logic. Ví dụ 2.4.1. Bộ ba logic Hoare    0*:00  xvuxvu , được đưa ra trong ngôn ngữ cục bộ, phát biểu rằng nếu cả hai biến u và v có các giá trị dương, thì sau khi thi hành phép gán x := u * v giá trị của biến x là dương. Bộ ba Hoare    0.*:.00  xzvuxzvu , được đưa ra trong ngôn ngữ toàn cục, phát biểu rằng nếu cả hai biến u và v có giá trị dương thì sau khi thi hành phép gán z.x = u * v, có nghĩa là, sau khi gán giá trị của u * v cho biến thể hiện x của đối tượng z, giá trị của z.x là dương. - 26 - 2.4.1. Phác thảo chứng minh Vì ngôn ngữ khẳng định trình bày rõ ràng về các trạng thái cục bộ và toàn cục, ta phải bổ sung chương trình với các biến phụ trợ mới để biểu diễn thông tin về các điểm điều khiển và các cấu trúc ngăn xếp trong các trạng thái cục bộ và toàn cục. Các thuộc tính bất biến của chương trình được chỉ rõ bởi chú thích. Một chương trình được bổ sung và chú thích được gọi là một phác thảo chứng minh hoặc là một chương trình được khẳng định. Ta chăm chú vào sự bổ sung để biểu diễn các động lực của nó. Các ngữ nghĩa toán tử của ngôn ngữ lập trình định nghĩa các quy tắc biến đổi của dạng   TransRule TT TA ',', ,    trong đó A là một vị từ được cho phép thông qua các cấu hình toàn cục. Tính đúng đắn của một hệ chứng minh có nghĩa là kiểm chứng các điều kiện đảm bảo tính quy nạp của chú thích, nghĩa là, tính bất biến của nó dưới các bước tính toán của dạng trên. Nói theo cách khác, trong mỗi cấu hình toàn cục có thể đạt được, các khẳng định kèm được đính kèm cho tất cả các điểm điều khiển hiện tại được yêu cầu là đúng .Chú ý rằng một luồng duy nhất có thể đồng thời ở một vài điểm điều khiển, mỗi điểm đối với mỗi cấu hình cục bộ trong chuỗi lời gọi của nó. Có nghĩa là, ta làm thành mô hình các lời gọi phương thức bằng giao tiếp đồng bộ, ta đòi hỏi rằng với mọi cấu hình cục bộ trong chuỗi của một luồng được kết hợp với khẳng định được thỏa mãn, và không chỉ đối với cấu hình cục bộ trên đỉnh của ngăn xếp. Một hệ chứng minh - đảm bảo rằng chú thích bất biến dưới các bước tính toán bất kỳ - là đúng đắn. Nhưng nó cũng mong muốn đầy đủ (tương đối), nghĩa là, mỗi thuộc tính bất biến là có thể chứng minh. Một hệ chứng minh đúng đắn và đầy đủ yêu cầu rằng chú thích là bất biến dưới các bước tính toán được cho phép thi hành chỉ trong các cấu hình có thể đạt được. Nó có nghĩa là, ta phải có khả năng biểu diễn tính được cho phép của các bước tính toán trong các mệnh đề đứng trước của kiểm chứng các điều kiện và tính có thể đạt được được trong chú thích. Bởi vì các khẳng định chỉ có thể tham chiếu tới các biến, nghĩa là, kiểm chứng các điều kiện chỉ lý luận về các trạng thái trong các cấu hình toàn cục mà không lý luận về các điểm điều khiển và các cấu trúc ngăn xếp, ta giới thiệu các biến phụ trợ sử dụng để mã hóa thông tin điều khiển trong các trạng thái. Với sự trợ giúp của các biến phụ trợ ta có thể định nghĩa một vị từ Aˆ thông qua các trạng thái sao cho các cấu hình có thể đạt được được ˆ,Tˆ - 27 - của chương trình được mở rộng thỏa mãn Aˆ . Chú ý rằng sự mở rộng phải không ảnh hưởng tới hành vi của chương trình gốc, nhưng nó chỉ được sử dụng để tạo các sự quan sát về cách một cấu hình được với tới như thế nào. Sự bổ sung Một sự bổ sung mở rộng một chương trình bằng thi hành nguyên tử các phép gán bội ey : cho các biến phụ trợ khác nhau, được gọi là các quan sát. Đối với việc tạo đối tượng – được trình bày theo cú pháp bởi sự bổ sung new c eynewu  :: đính kèm sự quan sát cho lệnh tạo đối tượng. Các quan sát 11 : ey  của một lời gọi phương thức và các quan sát 44 : ey  của sự thu nhận tương ứng của một giá trị trả về được biểu thị bằng:   retcall eyeyemeu ?44 ! 110 ::.:  . Sự bổ sung ret ret call eyereturnstmey ! 33 ? 22 :;:  của các thân phương thức chỉ rõ 22 : ey  là quan sát của sự thu nhận của lời gọi phương thức và 33 : ey  là quan sát được đính kèm cho câu lệnh return. Các phép gán có thể được quan sát bằng cách sử dụng ass eyey ':':  . Một quan sát đứng một mình không được đính kèm cho bất kỳ câu lệnh nào được viết là ey : . Nó có thể được chèn vào bất kỳ điềm nào trong chương trình. Chú ý rằng ta cũng có thể sử dụng cùng một cú pháp cho tất cả các kiểu của quan sát. Tuy nhiên, một ký hiệu như vậy sẽ bất tiện cho các bổ sung bộ phận, nghĩa là, đối với sự chỉ rõ của các bổ sung trong đó tất cả các câu lệnh không được quan sát. Ví dụ, sử dụng ký hiệu được giới thiệu ở trước, sự bổ sung   stmeme .0 chỉ rõ duy nhất stm là một quan sát đứng một mình theo sau một lời gọi phương thức không được quan sát, sử dụng cùng cú pháp bổ sung stm cho tất cả các kiểu của quan sát, ta phải viết   stmeme .0 để chỉ rõ cùng thiết lập. Sự bổ sung không ảnh hưởng tới luồng điều khiển của chương trình nhưng ép buộc một chính sách lịch trình chi tiết của các quan sát. Một lệnh gán và quan sát của nó được thi hành đồng thời. Tạo đối tượng và quan sát của nó được thi hành trong một bước tính toán duy nhất, trong thứ tự này. Đối với các quan sát của lời gọi phương thức, giao tiếp, gửi, nhận được thi hành trong một bước tính toán duy nhất, theo thứ tự này. Chú ý rằng thứ tự của các quan sát chỉ giữ vai trò đối với các lời gọi chính nó, - 28 - nghĩa là, đối với các lời gọi phương thức trong đó đối tượng gọi và đối tượng được gọi là như nhau. Các điểm giữa một câu lệnh và quan sát của nó là các điểm không có điều khiển, bởi vì lệnh và quan sát của nó được thi hành trong một bước tính toán duy nhất; ta gọi chúng là các điểm phụ trợ. Chú ý rằng các điểm điều khiển là các điểm chen vào, có nghĩa là, trong khi điều khiển ở các điểm này, các luồng khác có thể thực thi tương tranh; các điểm phụ trợ không có các điểm chen vào. Để loại trừ khả năng hai quan sát được thi hành trong bước tính toán duy nhất cả hai cùng sửa đổi trạng thái thể hiện của cùng một đối tượng, ta yêu cầu quan sát gọi trong một giao tiếp với chính nó không thể thay đổi các giá trị của các biến thể hiện. Trong phần sau ta cũng gọi các lệnh gán với các quan sát của nó là các phép gán bội, bởi vì chúng được thi hành đồng thời. Tương tự các biến chương trình, nhiều khi ta định nghĩa rõ ràng các biến ;yt xuất hiện trong một lớp bên ngoài các định nghĩa phương thức khai báo y là một biến phụ trợ của kiểu t. Cùng định nghĩa bên trong của một phương thức khai báo y là một biến phụ trợ cục bộ của kiểu t. Ví dụ 2.4.2. Mở rộng một phép gán x:= e tới assxuex  :: lưu trữ giá trị của x trước khi thi hành x := e trong biến phụ trợ u. Mở rộng nó tới x := e lưu trữ giá trị của x trong u sau khi thi hành x := e. Ví dụ 2.4.3. Ta có thể lưu trữ số lượng của các đối tượng đã được tạo bằng một thể hiện của một lớp c bằng cách sử dụng một biến thể hiện n kiểu nguyên với giá trị khởi tạo là 0, và mở rộng mỗi lệnh tạo đối tượng ': cnewu  trong c tới newc nnnewu 1:: '  Ví dụ 2.4.4. Ta mở rộng ví dụ 2.4.3 bởi thêm vào quan sát mỗi lời gọi  emeu .: 0 trong c bởi   retcall knknkemeu ?!0 ::.:  . Thì giá trị của biến phụ trợ cục bộ k kiểu nguyên sau lời gọi phương thức và quan sát của nó lưu trữ số lượng của các đối tượng được tạo nhưng trước khi trả về lời gọi phương thức. Sau khi trả về, nó lưu trữ số lượng các đối tượng được tạo ra trong suốt quá trình ước lượng phương thức. Ví dụ 2.4.5 Cho l là một biến thể hiện nguyên phụ trợ của một lớp c. Ta có thể đếm số lượng của các cấu hình cục bộ đang thực thi trong một thể hiện của lớp c bằng cách bổ sung vào thân stm; retereturn của mỗi phương thức trong lớp c kết quả là ret ret call llereturnstmll !? 1:;1:  - 29 - Các ví dụ trên biểu diễn cách đếm các đối tượng, các cấu hình cục bộ trong một đối tượng. Nhưng thông tin này là không đủ cho một hệ chứng minh đầy đủ: ta phải có khả năng nhận dạng những cấu hình này. Ta nhận dạng một cấu hình cục bộ bởi đối tượng trong đó nó thi hành cùng với giá trị của các biến cục bộ phụ trợ conf được tích hợp lưu trữ một định danh duy nhất bên trong đối tượng. Tính duy nhất được đảm bảo bởi biến phụ trợ counter, được tăng cho mỗi hình cục bộ trong đối tượng. Phương thức được gọi nhận địa chỉ trả về như một tham biến phụ trợ hình thức caller của kiểu IntObject  , lưu trữ các định danh của đối tượng gọi và lời gọi cấu hình cục bộ. Phương thức run của đối tượng khởi tạo được thi hành với tham biến caller có giá trị (null, 0). Mỗi khai báo phương thức   retereturnstmum ; được mở rộng bởi tích hợp sự bổ sung tới   retcall ereturncountercountercounterconfcallerum ;1,:,, ? . Tương tự cho lời gọi phương thức  emeu .: 0 , danh sách tham biến thực sự được mở rộng, kết quả là   confthisemeu ,,.: 0 . Chú thích Để chỉ rõ các thuộc tính bất biến của hệ thống, các chương trình bổ sung được chú thích bởi đính kèm các khẳng định cho mỗi điểm điều khiển và các điểm phụ trợ. Ta sử dụng ký hiệu bộ ba Hoare    qstmp và viết pre(stm) và post(stm) để tham chiếu tới điều kiện trước và điều kiện sau của một lệnh. Đối với các khẳng định ở các điểm phụ trợ ta sử dụng ký hiệu sau: Chú thích      210 :: peypnewup newnewc  của một lệnh tạo đối tượng chỉ rõ 0p và 2p là các điều kiện trước và sau, trong khi đó 1p tại điểm phụ trợ là đúng trực tiếp sau khi tạo đối tượng nhưng trước sự điều phối của nó. Chú thích            4 ? 44 ? 32 ! 11 ! 100 ::.: peyppeypemeup retretwaitcallcall  gán 0p và 4p là các điều kiện trước và điểu kiện sau cho lệnh thi hành công thức; 1p được đảm bảo là đúng trực tiếp sau khi gọi phương thức, nhưng đứng trước sự quan sát của nó; 2p mô tả điểm điều khiển của phương thức gọi sau lời gọi phương thức và quan sát của nó nhưng trước khi trả về; cuối cùng, 3p chỉ rõ trạng thái trực tiếp sau khi - 30 - trả về nhưng trước quan sát của nó. Chú thích của thân phương thức retereturnstm; được định nghĩa như sau:          4 ! 33 ! 321 ? 22 ? 0 :;: peypereturnpstmpeyp retret ret callcall  Điều kiện sau của phương thức được gọi là 1p ; các điều kiện trước và điều kiện sau đối với câu lệnh trả vê là 2p và 4p . Các khẳng định 0p và 3p theo thứ tự chỉ rõ các trạng thái của phương thức được gọi giữa lời gọi phương thức, theo thứ tự, trả về và quan sát của nó. Bên cạnh các điều kiện trước và điều kiện sau, đối với mỗi lớp c, chú thích định nghĩa một khẳng định cục bộ cI gọi là bất biến lớp, chỉ rõ các thuộc tính bất biến trong các toán hạng của c trong điều kiện trước và sau của biến thể hiện của nó. Ta yêu cầu đối với mỗi phương thức của lớp, bất biến lớp là điều kiện trước của thân phương thức. Cuối cùng, một khẳng định toàn cục GI được gọi là bất biến toàn cục chỉ rõ các thuộc tính của giao tiếp giữa các đối tượng. Khẳng định toàn cục là bất biến dưới sự tính toán bên trong của đối tượng. Với lý do này, ta yêu cầu tất cả các tham chiếu hạn chế E.x trong GI với biểu thức E của kiểu c, tất cả các phép gán tới x trong lớp c xuất hiện trong các quan sát của truyền thông hoặc tạo đối tượng. Trong phần sau ta sẽ sử dụng các lệnh được chú thích bộ phận; các khẳng định không được chỉ rõ bằng định nghĩa đúng. Ví dụ 2.4.6. Chú thích (bộ phận)  thisunewu c : của một lệnh tạo đối tượng trong lớp c’ phát biểu rằng định danh của đối tượng mới khác với định danh của đối tượng tạo ra. Tính bất biến của chú thích này có thể được biển diễn bởi chứng minh kiểm chứng các điều kiện được sinh ra cho lệnh tạo đối tượng ở trên. Tuy nhiên, tính đúng đắn của khẳng định không phụ thuộc vào các phần còn lại của chương trình, bởi vì chỉ biến được chia sẻ trong khẳng định là tham chiếu tới chính nó, không thể được gán tới. Thuộc tính giống nhau có thể được phát biểu bằng sử dụng bất biến lớp. Bởi vì bất biến lớp chỉ có thể tham chiếu tới các biến thể hiện, ta phải lưu trữ định danh của đối tượng mới trong biến thể hiện phụ trợ x để tham chiếu tới nó trong bất biến lớp. Ta định nghĩa chú thích  uxuxnewu newc  :: và bất biến lớp bởi thisx  . Trong trường hợp này, tính bất biến của các khẳng định được cho cũng phụ thuộc vào các phần còn lại của định nghĩa lớp: một quan sát x := this được thi hành trong cùng đối - 31 - tượng tất nhiên sẽ vi phạm tính bất biến lớp. Chú thích này rất hữu ích, nếu các khẳng định khác nhau trong cùng lớp tham chiếu tới x, và đặc biệt nếu thông tin được phát biểu bởi bất biến lớp được đòi hỏi biểu diễn các thuộc tính của các lời gọi phương thức đến. Bất biến toàn cục có thể được sử dụng để phát biểu thuộc tính trên: Đảm bảo  uxuxnewu newc  :: và cho bất biến toàn cục được định nghĩa bởi   zxzcz  ..': . 2.4.2. Kiểm chứng các điều kiện Hệ chứng minh hình thức hóa một số kiểm chứng các điều kiện, đảm bảo quy nạp rằng đối với mỗi cấu hình có thể đạt được, các khẳng định cục bộ được đính kèm với các điểm điều khiển hiện tại trong cấu hình luồng là đúng, cũng như là các bất biến lớp và bất biến toàn cục là đúng. Các điều kiện thường được nhóm lại thành các điều kiện ban đầu, và đối với bước quy nạp trong tính đúng đắn cục bộ và các kiểm tra đối với tính không có sự can thiệp và kiểm tra sự hợp tác. Các điều kiện của tính đúng đắn ban đầu bao hàm sự thỏa mãn của các thuộc tính trong cấu hình chương trình ban đầu. Sự thi hành của duy nhất một thân phương thức được nắm giữ bởi các điều kiện đúng đắn cục bộ chuẩn, bằng cách sử dụng ngôn ngữ khẳng định cục bộ. Sự can thiệp giữa các thi hành phương thức tương tranh được bao hàm trong kiểm tra tính không có can thiệp, cũng được đề ra trong ngôn ngữ cục bộ. Các kết quả của giao tiếp và tạo đối tượng được giải quyết trong kiểm tra sự hợp tác. Bởi vì giao tiếp có thể diễn ra trong một đối tượng duy nhất hoặc giữa các đối tượng khác nhau, kiểm tra tính hợp tác được đưa ra trong ngôn ngữ khẳng định toàn cục. Kiểm chứng các điều kiện đảm bảo tính bất biến của chú thích như các phần sau: Thỏa mãn ban đầu của chú thích được đảm bảo bởi các điều kiện ban đầu. Nếu một bước tính toán thi hành một phép gán, thì các điều kiện đúng đắn cục bộ đảm bảo quy nạp của việc thi hành các thuộc tính của cấu hình cục bộ; kiểm tra tính không có sự can thiệp đảm bảo tính bất biến dưới sự thi hành của phép gán cho các thuộc tính của tất cả các cấu hình cục bộ và các bất biến lớp khác. Đối với sự giao tiếp, tính bất biến đối với sự thi hành các phần và bất biến toàn cục được đảm bảo bởi kiểm tra sự hợp tác cho giao tiếp. Giao tiếp với chính nó không ảnh hưởng đến trạng thái toàn cục; tính bất biến của các thuộc tính còn lại dưới các quan sát tương ứng được đảm bảo bởi kiểm tra tính không có can thiệp. - 32 - Trước khi chỉ rõ kiểm chứng các điều kiện, ta giới thiệu một vài ký hiệu. Cho Init là một toán tử cú pháp với thể hiện Init. Cho cIVar là tập hợp các biến thể hiện của lớp c không có tham chiếu tới chính nó, và z là một biến logic của kiểu c, cho InitState(z) là khẳng định toàn cục  xInitxznullz cIVarx   . , phát biểu rằng đối tượng được biểu thị bởi z trong trạng thái thể hiện ban đầu của nó. Tính đúng đắn ban đầu Một phác thảo chứng minh của một chương trình là đúng đắn ban đầu, nếu điều kiện trước của lệnh chính, bất biến lớp của đối tượng ban đầu, và bất biến toàn cục được thỏa mãn ban đầu, nghĩa là, trong cấu hình toàn cục ban đầu sau sự thi hành của quan sát được gọi ở phần bắt đầu của lệnh chính. Hơn nữa điều kiện trước của quan sát nên được thỏa mãn trước sự thi hành của nó. Định nghĩa 2.4.7. (Tính đúng đắn ban đầu) Cho thân của phương thức run của lớp chính c là     returnstmpeyp call ;: 322 ? 2  với các biến cục bộ v không có các tham biến hình thức, cLVarz và ObjectLVarz ' . Một phác thảo chứng minh là đúng đắn ban đầu, nếu G|   '''. zznullzzzInitState     0,,:, nullvInitcallerv    zP2 , và G|   '''. zznullzzzInitState     0,,:, nullvInitcallerv  ;  zEyz 22 :.      zIzPGI c 3 . Khẳng định   '''. zznullzzzInitState  phát biểu rằng trạng thái toàn cục ban đầu định nghĩa một đối tượng đang tồn tại z trong trạng thái thể hiện ban đầu. Sự khởi tạo của cấu hình cục bộ được biểu diễn bởi lệnh gán    0,,:, nullvInitcallerv  . Quan sát 22 : ey  tại phần bắt đầu của phương thức run của đối tượng ban đầu z được biểu diễn bởi lệnh gán  zEyz 22 :.  . Ví dụ 2.4.8. Giả thiết phác thảo chứng minh sau:     212211 .:.: zznullzInitialznullzInitialz  // bất biến toàn cục - 33 - class Initial { Int x; {started} // bất biến lớp Void run () { Int v; ;uInt   callxvu ?000  //điều kiện trước của quan sát   callu ?1: // quan sát của lời gọi  001  xvu // điều kiện sau của quan sát … } } Chú ý rằng bổ sung được được tích hợp mở rộng quan sát   callu ?1: thành   calltruestartedu ?,1:,  . Điều kiện ban đầu   ''.:'0.| zznullzObjectzxznullzG   0,,0,0:,, nullcalleruv   0.00  xzvu đảm bảo rằng điều kiện trước của quan sát là đúng sau khi khởi tạo nhưng trước sự thi hành của nó. Điều kiện thứ hai   ''.:'0.| zznullzObjectzxznullzG    truestartedzunullcalleruv ,1:.,;0,,0,0:,,      startedzxvuGI .001  - 34 - đảm bảo rằng bất biến toàn cục, điều kiện sau của quan sát, và bất biến lớp là đúng sau quan sát. Sự thỏa mãn của bất biến toàn cục có thể được biểu diễn bằng sự tạo đối tượng với z. Tính đúng đắn cục bộ Một phác thảo chứng minh là đúng đắn cục bộ, nếu các thuộc tính của các thể hiện phương thức được chỉ rõ bởi chú thích là bất biến dưới sự thi hành của các phương thức. Ví dụ, điều kiện trước của một lệnh gán phải kéo theo điều kiện sau của nó sau sự thì hành của nó. Bên cạnh các điều kiện cho các phép gán, tính đúng đắn cục bộ định nghĩa thêm các điều kiện bổ sung cho các cấu trúc điều khiển như các vòng lặp và các lệnh điều kiện. Định nghĩa 2.4.9. (Tính đúng đắn cục bộ: Phép gán) Một phác thảo chứng minh là đúng đắn cục bộ với khía cạnh các phép gán, nếu với tất cả các phép gán    21 : peyp  trong lớp c, các phép gán không phải là quan sát của tạo đối tượng hoặc là giao tiếp,    21 :| peyIp cL  . Ví dụ 2.4.10. Giả thiết phương thức được bổ sung và chú thích sau tính toán giai thừa u! đối với tham biến u của nó: Int fac (Int u) { Int result; {u > 0} result := 1;  01  uresult v := u  00!*!  vuvresultu while (v > 1) do  10!*!  vuvresultu result := result * v;   10!1*!  vuvresultu v := v – 1;  00!*!  vuvresultu od;  resultu ! return result; } Phác thảo chứng minh trên thỏa mãn các điều kiện của tính đúng đắn cục bộ. Có 7 điều kiện của tính đúng đắn cục bộ (không có các điều kiện của tính đúng đắn ban - 35 - đầu, tính không có can thiệp, và kiểm tra sự hợp tác cho ví dụ này). Đối với ví dụ này, tính đúng đắn cục bộ của phép gán result := result * v định nghĩa kiểm chứng điều kiện  10!*!|  vuvresultuL result := result * v   10!1*!  vuvresultu Kiểm tra tính không có can thiệp Sự can thiệp giữa các sự thi hành của phương thức tương tranh được bao hàm bởi kiểm tra tính không có can thiệp. Bởi vì ta đang giải quyết với một ngôn ngữ tuần tự, ta chỉ phải biểu diễn tính bất biến của các khẳng định được đính kèm với các điểm điều khiển đang chờ trả về trong một dãy các lời gọi dưới sự thi hành của cấu hình cục bộ ở trên đỉnh của ngăn xếp. Tính không có can thiệp cũng bao hàm tính bất biến của các bất biến lớp. Bởi vì seqJava không hỗ trợ các tham chiếu hạn chế tới các biến thể hiện, sự thi hành trong một đối tượng không thể ảnh hưởng đến sự ước lượng của các biểu thức cục bộ trong các đối tượng khác. Điều đó có nghĩa là, ta chỉ phải giải quyết với tính bất biến dưới sự thi hành của cùng một đối tượng. Do đó, các kiểm chứng điều kiện tương ứng được đưa ra trong ngôn ngữ khẳng định cục bộ. Chỉ ảnh hưởng tới các biến cục bộ, giao tiếp đối tượng và tạo đối tượng không thay đổi các trạng thái thể hiện của các đối tượng đang thi hành. Do đó ta chỉ phải bao hàm tính bất biến của các khẳng định ở các điểm điều khiển dưới các phép gán, chứa trong các quan sát của giao tiếp đối tượng và tạo đối tượng. Để phân biệt các biến cục bộ của các cấu hình cục bộ khác nhau, ta viết lại tên của các biến này của khẳng định. Chú ý rằng các khẳng định tại các điểm phụ trợ không phải biểu diễn tính bất biến, bởi vì các điểm phụ trợ là các điểm không chen vào. Cho q là một khẳng định tại một điểm điều khiển và ey : là một phép gán bội trong cùng một lớp c. Bởi vì trong ngôn ngữ tuần tự, q và ey : thuộc về cùng một luồng, các khẳng định bị ảnh hưởng là các khẳng định tại các điểm điều khiển đang chờ trả về trong sự thi hành ngăn xếp hiện tại. Tuy nhiên tính bất biến của một cấu hình cục bộ dưới sự thi hành của nó không cần được để ý và loại bỏ bằng yêu cầu 'confconf  . Với một khẳng định tại một điểm điều khiển đang chờ trả về từ một lời gọi chính nó, sự can thiệp với sự trùng khít câu lệnh trả về cả hai không cần được để ý: - 36 - Các đối tác đang giao tiếp thi hành thời thì chúng thay đổi điểm điều khiển của phương thức gọi. Khẳng định  ', confthiscaller  mô tả thiết lập này: Nó đúng nếu cấu hình cục bộ được mô tả bởi q’ và định danh conf’ là phương thức gọi của cấu hình cấu hình cục bộ mà trong đó biến cục bộ caller thi hành ey : trong cùng đối tượng. Cho caller_obj là thành phần đầu tiên và caller_conf là thành phần thứ hai của caller. Ta định nghĩa  eyqretforwait :,__ bằng: • confconf ' , với các khẳng định  waitq được đính kèm với các điểm điều khiển đang chờ trả về, nếu ey : không phải là quan sát của trả về. •  confcallerconfobjcallerthisconfconf _'_'  , với các khẳng định  waitq , nếu ey : quan sát trả về. • false, ngược lại. Định nghĩa 2.4.11. (Tính không có can thiệp) Một phác thảo chứng minh là không có can thiệp, nếu với tất cả các lớp c và các phép gán ey : với điều kiện trước p trong c,    ccL IeyIp  :| . Hơn nữa, với tất cả các khẳng định q tại các điểm điều khiển trong c,     '::,__'| qeyeyqretforwaitsIqp cL  . Ví dụ 2.4.12. Cho           5?2?43!1!21 . pstmppstmpemthisp retretwaitcallcall là một lệnh gọi phương thức được chú thích trong phương thức m’ của lớp c với một biến phụ trợ kiểu nguyên x, sao cho mỗi khẳng định kéo theo conf = x. Có nghĩa là, định danh của cấu hình cục bộ đang thi hành được lưu trữ trong biến thể hiện x. Chú thích biểu thị rằng không có các cặp của các điểm điều khiển trong m’ của c có thể đạt tới được một cách đồng thời. Các khẳng định 2p và 4p không cần được biểu diễn bất biến, bởi vì chúng được đính kèm cho các điểm phụ trợ. Tính không có can thiệp không yêu cầu đối với cả hai khẳng định 1p và 5p , bởi vì chúng không phải là các điểm điều khiển đang chờ sự trả về, và do vậy các mệnh đề của các điều kiện tương ứng ước lượng là sai. Tính bất biến của 3p dưới sự thi hành của quan sát 1stm với điều kiện trước 2p yêu cầu sự đúng đắn của     311332 ',__'| pstmstmpretforwaitsppL  . Khẳng định - 37 -  1332 ,__' stmpretforwaitspp  kéo theo      confconfxconfxconf  '' , ước lượng sai. Tính bất biến của 3p dưới sự thi hành của 2stm được chứng minh tương tự. Kiểm tra hợp tác Trong khi kiểm tra tính không có can thiệp đảm bảo tính bất biến của các khẳng định dưới các bước trong đó chúng không được tham gia, kiểm tra sự hợp tác giải quyết với các đối tác giao tiếp, đảm bảo rằng bất biến toàn cục, và các điều kiện trước và các bất biến lớp của các lệnh được tham gia kéo theo các điều kiện sau của chúng sau bước kết hợp. Thêm nữa, các điều kiện trước của các quan sát tương ứng phải là đúng sau giao tiếp. Các bất biến toàn cục tham chiếu tới các biến thể hiện phụ trợ, các biến này chỉ có thể được thay đổi bởi các quan sát của giao tiếp. Do đó, bất biến toàn cục là bất biến dưới sự thi hành của các lệnh không phải là giao tiếp. Tuy nhiên, đối với giao tiếp và tạo đối tượng tính bất biến phải được biểu diễn như một phần của kiểm tra sự hợp tác. Để tránh các xung đột tên giữa các biến của các đối tác giao tiếp, ta đặt lại tên các biến của các đối tác được gọi. Bởi vì các đối tượng khác nhau có thể được tham gia, kiểm tra tính hợp tác được đưa ra trong ngôn ngữ khẳng định toàn cục. Các thuộc tính cục bộ được phát biểu trong ngôn ngữ toàn cục thông qua sử dụng sự thay thế nâng lên. Như đã được đề cập, ta sử dụng các biểu tượng tắt  zP và  '' zQ theo thứ tự với  thiszp / và với  thiszq /'' , và tương tự cho các biểu thức. Cho z và z’ là các biến logic mà giá trị của chúng đại diện cho đối tượng gọi và đối tượng được gọi trong một lời gọi phương thức. Ta giả thiết bất biến toàn cục, các bất biến lớp của các đối tác đang giao tiếp, và các điều kiện trước của các lệnh đang giao tiếp là đúng trước giao tiếp. Đối với sự thi hành phương thức, điều kiện trước của phương thức được gọi là bất biến lớp của nó. Hai lệnh đại diện các đối tác đang giao tiếp được nắm giữ bởi khẳng định comm, phụ thuộc vào kiểu của giao tiếp: Với sự thi hành phương thức  me0 , khẳng định   '0 zzE  phát biểu rằng giá trị của z’ nhận dạng đối tượng được gọi. Chú ý rằng sự thi hành phương thức điều khiển thông qua sự trả về địa chỉ như là một tham biến phụ trợ, và các giá trị của các tham biến hình thức còn lại không được thay đổi. Hơn nữa, các tham biến không thể chứa các biến thể hiện, nghĩa là, thể hiện của chúng không thay đổi trong suốt quá trình thi hành phương thức. Bởi vậy, các tham biến hình thức và các tham biến thực sự có thể được sử dụng trong sự trả về từ một phương thức để nhận dạng các đối tác đang trong mối quan hệ caller- - 38 - callee, bằng cách sử dụng các biến phụ trợ. Do đó với trường hợp trả về, comm thêm vào phát biểu  zEu  , trong đó u và e là các biến hình thức và biến thực sự. Sự trả về từ phương thức run kết thúc luồng đang thi hành; phương thức run không có các kết quả với giao tiếp. Các thay đổi trạng thái được biểu thị bởi các phép gán. Ví dụ của sự thi hành một phương thức, giao tiếp được phát biểu bởi các phép gán  zEu : , trong đó sự khởi tạo của các biến cục bộ v được bao hàm bởi  vInitv :' . Các phép gán  zEyz 11 :.  và  '':''. 22 zEyz  đại diện cho các quan sát gọi và quan sát được gọi 11 : ey và 22 : ey , theo thứ tự được thi hành trong z và z’. Định nghĩa 2.4.14. (Kiểm tra sự hợp tác: Sự giao tiếp) Một phác thảo chứng minh thỏa mãn kiểm tra sự hợp tác với giao tiếp, nếu G|         nullznullzcommzIzQzIzPGI cc  '''' '11 commf     ''22 zQzP  và (2.6) G|         nullznullzcommzIzQzIzPGI cc  '''' '11 21;; obsobscomm fff (2.7)     ''33 zQzPGI  là đúng với các biến logic mới khác nhau cLVarz và '' cLVarz  , trong các trường hợp sau: 1.CALL: Với tất cả các lệnh       waitcallcallret peypemeup 3 ! 11 ! 201 :.:  (hoặc là các lệnh này mà không nhận một giá trị) trong lớp c với 0e của kiểu c’, trong đó phương thức m của c’ có thân     ret callcall ereturnstmqeyq ;: 3 ? 22 ? 2  , các tham biến hình thức u , và các biến cục bộ v trừ các tham biến hình thức. Bất biến của lớp được gọi là '1 cIq  . Khẳng định comm được cho bởi   '0 zzE  . Hơn nữa, commf là    vInitzEvu ,:','  , 1obsf là  zEyz 11 :.  , và 2obsf là  '':''. 22 zEyz  . - 39 - 2. RETURN: Với tất cả        3 ? 44 ? 21 ! 0 :.: peyppstmemeu retretwaitcall ret  hoặc không nhận một giá trị đang xuất hiện trong c với 0e của kiểu c’, sao cho phương thức m của c’ có lệnh trả về      3 ! 33 ! 21 : qeyqereturnq retret ret  , và danh sách biến hình thức u , các phương trình trên phải là đúng với comm được cho bởi    zEuzzE  ''0 , và trong đó commf là  '': zEu retret  , 1obsf là  '':''. 33 zEyz  , và 2obsf là  zEyz 44 :.  . 3. runRETURN : Với      3 ! 33 ! 21 : qeyqreturnq retret  đang xuất hiện trong phương thức run của lớp chính, trueppp  321 , truecomm  , và hơn nữa commf và 2obsf là các lệnh rỗng, và 1obsf là  '':''. 33 zEyz  . Bên cạnh các lời gọi phương thức và các trả về phương thức, kiểm tra sự hợp tác cần điều khiển Ví dụ 2.4.15. Ví dụ này minh họa cách chứng minh các thuộc tính của việc truyền tham biến. Cho    evmep ,.0 , với p được cho bằng v > 0, là một lệnh được chú thích trong lớp c với 0e của kiểu c’, và cho phương thức  ,um của c’ có thân của dạng   returnstmq ; trong đó q là u > 0. Tính quy nạp của phác thảo chứng minh yêu cầu rằng nếu p là đúng trước khi gọi (bên cạnh sự đúng đắn của các bất biến toàn cục và bất biến lớp), thì q được thỏa mãn sau sự thi hành. Điều kiện 2.7 của kiểm tra sự hợp tác yêu cầu chứng minh      '':'| zQvuzPG  , khai triển thành    0':'0|  uvuvG . Ví dụ 2.4.16. Ví dụ sau chứng minh cách biểu thị sự phụ thuộc giữa các trạng thái thể hiện trong cấu hình toàn cục và sử dụng thông tin này trong kiểm tra giao tiếp. Cho    emep .0 , với p được cho bằng oex  00 , là một lệnh được chú thích trong lớp c với 0e của kiểu c’, x là một biến thể hiện kiểu nguyên, và o là một biến thể hiện của kiểu c’, và cho phương thức  um của c’ có chú thích thân phương thức   returnstmq ; trong đó q là y > 0 và y là một biến thể hiện kiểu nguyên. Hơn nữa cho cLVarz và cho bất biến toàn cục được cho bằng   0..0...  yozxznulloznullzz . Tính quy nạp yêu cầu rằng nếu p và bất biến toàn cục là đúng trước khi gọi, thì q được thỏa mãn sau sự thi hành. Điều kiện 2.7 của kiểm tra sự hợp tác     0..0...| yozxznulloznullzzG - 40 -      nullznullzzzEozzExz  ''.0. 00  zEu :'  0'. yz tạo đối tượng lượng hóa bằng z, mệnh đề kéo theo ozzyoz .'0..  , có nghĩa là 0'. yz . Bên cạnh các lời gọi phương thức và các sự trả về, kiểm tra sự hợp tác yêu cầu quản lý tạo đối tượng, duy trì các bất biến toàn cục, điều kiện sau của lệnh new và quan sát của nó, và các bất biến lớp của của đối tượng mới. Ta có thể giả thiết rằng điều kiện trước của lệnh tạo đối tượng, bất biến lớp của đối tượng tạo, và bất biến toàn cục là đúng trong cấu hình trước khi tạo đối tượng. Sự mở rộng của trạng thái toàn cục với đối tượng được tạo mới được đưa ra trong điều kiện sau mạnh nhất, có nghĩa là, nó được yêu cầu là đúng ngay sau khi tạo đối tượng. Ta sử dụng lượng hóa tồn tại để tham chiếu tới giá trị cũ: z’ của kiểu listObjectLVar đại diện các đối tượng đang tồn tại trước khi mở rộng. Hơn nữa, định danh đối tượng được tạo ra được lưu trữ trong u là mới và thể hiện mới có thể được khởi tạo được biểu thị bằng khẳng định toàn cục  uzFresh ,' được định nghĩa là     uvzvObjectvzuuInitState  '.:' . Để biểu thị rằng một khẳng định tham chiếu tới tập các đối tượng đang tồn tại trước sự mở rộng của trạng thái toàn cục, ta chỉ cần giới hạn lượng hóa phổ biến trong khẳng định tới dãy thông qua các đối tượng từ z’. Cho P là một khẳng định toàn cục và listObjectLVarz ' là một biến logic không xuất hiện trong P. Thì 'zP  là khẳng định toàn cục với tất cả các lượng hóa '. Pz được thay thế bằng   ''. Pzzobjz  , trong đó obj(v) ký hiệu tập các đối tượng xuất hiện trong giá trị v. Bổ đề 2.4.18. Giả thiết rằng một trạng thái toàn cục  , một sử mở rộng  initcinst ,'   đối với   ValVal c  , , và một môi trường logic  chỉ tham chiếu tới các giá trị đang tồn tại trong  . Cho v là dãy bao gồm tất cả các phần tử của  nullcc Val . Thì đối với tất cả các khẳng định P và các biến logic listObjectLVarz ' không xuất hiện trong P, PG|, khi và chỉ khi   '|',' zPvz G   . Vị từ   '. zPu  được ước lượng ngay sau khi tạo đối tượng cnewu : , biểu thị rằng P đúng trước khi tạo đối tượng mới. - 41 - Định nghĩa 2.4.19. (Kiểm tra sự hợp tác: Tạo đối tượng) Một phác thảo chứng minh thỏa mãn kiểm tra sự hợp tác đối với việc tạo đối tượng, nếu với tất cả các lớp c’ và các lệnh      321 :: peypnewup newnewc  trong c’: G|         '.,''. '1 zzIzPuGIuzFreshzuznullz c     uIzP c 2 và G|          '.,''. '1 zzIzPuGIuzFreshzuznullz c   zEyz :.   zPGI 3 là đúng với 'cLVarz và listObjectLVarz ' mới. - 42 - CHƯƠNG 3. NGÔN NGỮ TƯƠNG TRANH 3.1. Cú pháp  startmethmethmethcclassclass runmeth...:: classclass main :: mainclassclassclassprog ...:: Ta tập trung vào khía cạnh tương tranh, tất cả các lớp là các lớp Thread theo nghĩa của Java: Mỗi lớp chứa một phương thức start được định nghĩa trước có thể được thi hành chỉ một lần đối với mỗi đối tượng, kết quả là tạo ra một luồng mới của sự thi hành. Luồng mới bắt đầu thi hành phương thức run được định nghĩa bởi người dùng của đối tượng được cho trong khi luồng ban đầu tiếp tục sự thi hành của nó. Phương thức run không thể được thi hành trực tiếp. Phương thức start không có tham biến không có giá trị trả về thì không được cài đặt một cách đúng cú pháp. Cú pháp không cho phép các tham chiếu hạn chế tới các biến thể hiện. Như là một hệ quả, các biến chia sẻ tương tranh được tạo ra bởi sự thi hành tương tranh chỉ trên một đối tượng duy nhất, không phải thông qua tập các đối tượng. 3.2. Ngữ nghĩa Các ngữ nghĩa toán tử của concJava mở rộng các ngữ nghĩa của seqJava bởi tạo các luồng động. Các quy tắc thêm:                 start c CALL stmstarteT stmstarteTstartedVale      ,;.,, ,;.,,,        ,,,,,, ,, cruncruninit bodystmT                     skip startCALLstmTstmstarteT stmstarteTstartedVale    ,,,,;.,, ,;.,,,     Sự thi hành phương thức start tạo ra một luồng mới bắt đầu thi hành phương thức run của đối tượng được gọi. Chỉ có lần gọi đầu tiên thi hành phương thức start có hiệu quả (quy tắc skipstartCALL ). Vị từ  ,Tstarted là đúng khi và chỉ khi tồn tại một ngăn - 43 - xếp có dạng  000 ,, stm  111 ,, stm …  nnn stm,,  T sao cho 0  . Một luồng kết thúc vòng đời của nó bằng sự trả về từ một phương thức run. 3.3. Hệ chứng minh 3.3.1. Phác thảo chứng minh Để đạt được một hệ chứng minh đầy đủ, đối với ngôn ngữ tương tranh ta phải có khả năng nhận dạng các luồng. Ta nhận dạng một luồng qua đối tượng mà trong đó nó bắt đầu sự thi hành. Do đó ta sử dụng kiểu Thread như là sự viết tắt cho kiểu Object. Một định danh là duy nhất, bởi vì một luồng của đối tượng chỉ có thể được bắt đầu một lần. Trong suốt một lời gọi phương thức, luồng phương thức được gọi nhận định danh của nó như là tham biến phụ trợ hình thức được tích hợp thread. Ta mở rộng tham biến hình thức phụ trợ caller bằng định danh luồng gọi, nghĩa là, cho caller là kiểu ThreadIntObject  , lưu trữ các định danh của đối tượng của luồng gọi, lời gọi cấu hình cục bộ, và luồng gọi. Chú ý các định danh luồng của đối tượng gọi và đối tượng được gọi là như nhau trong tất cả các trường hợp ngoại trừ đối với sự thi hành của phương thức start. Phương thức run của đối tượng ban đầu được thi hành với các tham biến  callerthread , có các giá trị   nullnull ,0,,0 , trong đó 0 biểu thị đối tượng ban đầu. Giá trị của biến thể hiện phụ trợ được tích hợp vào started nhớ bất kỳ khi nào phương thức start của đối tượng đã được thi hành. Theo cú pháp, mỗi danh sách tham biến hình thức u trong chương trình gốc được mở rộng thành  callerthreadu ,, . Tương ứng với phương thức gọi, mỗi danh sách tham biến thực sự e trong các câu lệnh thi hành một phương thức khác với phương thức start được mở rộng thành   threadconfthisthreade ,,,, . Sự thi hành của phương thức start không có tham biến của đối tượng 0e lấy danh sách tham biến thực sự   threadconfthise ,,,0 . Sự quan sát của phương thức được gọi ở điểm bắt đầu của phương thức run thi hành started := true. Các biến conf và counter cũng được cập nhật. Bởi vì một luồng gọi phương thức start không đợi sự trả về của phương thức start nhưng tiếp tục thi hành, sự bổ sung và chú thích của sự thi hành phương thức start có dạng là        3!!201 . pstmpestartep callcall . 3.3.2. Kiểm chứng các điều kiện Tính đúng đắn ban đầu - 44 - Tính đúng đắn cục bộ chỉ thay đổi ở chỗ các tham biến hình thức thread và caller được gán các giá trị ban đầu  và  nullnull ,0, , trong đó  là đối tượng ban đầu. Định nghĩa 3.3.1. (Tính đúng đắn ban đầu) Cho thân của phương thức run của lớp chính c là     returnstmpeyp callcall ;: 3 ? 22 ? 2  với biến cục bộ v không có các tham biến hình thức, cLVarz , và ObjectLVarz ' . Một phác thảo chứng minh là đúng đắn ban đầu, nếu G|   ''.' zznullzzzInitState     nullnullzvInitcallerthreadv ,0,,,:,,    zP2 , và G|   ''.' zznullzzzInitState       zEyznullnullzvInitcallerthreadv 22 :.;,0,,,:,,      zIzPGI c 3 . Khẳng định   '''. zznullzzzInitState  phát biểu rằng trạng thái toàn cục ban đầu định nghĩa một đối tượng z đang tồn tại trong trạng thái thể hiện ban đầu của nó, và quan sát 22 : ey  ở phần bắt đầu của phương thức run của đối tượng ban đầu z được thể hiện bởi phép gán  zEyz 22 :.  . Sự khác nhau là ở trong sự khởi tạo của cấu hình cục bộ, cấu hình cục bộ bây giờ được biểu diễn bởi phép gán    0,0,,,:,, nullthreadvInitcallerthreadv  . Kiểm tra tính không có can thiệp Sự can thiệp của một luồng duy nhất dưới sự thi hành của nó giống như trong ngôn ngữ tuần tự. Tuy nhiên, ta phải giải quyết với sự bất biến của các thuộc tính của một luồng dưới sự thi hành của một luồng khác. Một khẳng định q tại một điểm điều khiển phải là bất biến dưới một phép gán ey : trong cùng một lớp nếu cấu hình cục bộ được mô tả bởi khẳng định không hoạt động trong bước tính toán đang thi hành phép gán. Để phân biệt các biến cục bộ của các cấu hình cục bộ khác nhau, ta đặt lại tên của các biến cục bộ trong khẳng định mà phải là bất biến, có kết quả là các biến, các biểu thức, và các khẳng định được đánh - 45 - dấu phẩy. Ví dụ, trong các điều kiện ta sử dụng thread để nhận dạng luồng đang thi hành phép gán, và thread’ để nhận dạng luồng được mô tả bởi q. Nếu q và ey : thuộc về cùng một luồng, có nghĩa là , thead’ = thread, thì ta có cùng mệnh đề như đối với ngôn ngữ tuần tự. Nếu khẳng định và phép gán thuộc về các luồng khác nhau, tính không có can thiệp phải được biểu diễn trong tất cả các trường hợp trừ sự thi hành chính nó của phương thức start: Quan sát được gọi của một sự thi hành chính nó của phương thức start không thể can thiệp với điều kiện trước của sự thi hành. Để mô tả sự thiết lập này, ta định nghĩa  eyqstartself :,_ bằng  ',', threadconfthiscaller  khi và chỉ khi q là điều kiện trước của sự thi hành phương thức  estarte .0 và phép gán là quan sát được gọi tại phần bắt đầu của phương thức run, và bằng false nếu ngược lại. Định nghĩa 3.3.2. (Tính không có can thiệp) Một phác thảo chứng minh là không có can thiệp, nếu các điều kiện của định nghĩa 2.4.1 đúng với  eyqretforwaits :,__ được thay thế bằng   defe :yq,interferes thread = thread’   eyqretforwaits :,__  eyqstartselfthreadthread  :,_' Ví dụ 3.3.3. Giả thiết một lệnh gán được chú thích  stmp trong một phương thức, và một khẳng định q tại một điểm điều khiển không đợi sự trả về trong cùng một phương thức, sao cho p và q kéo theo thread = this. Điều này có nghĩa là, phương thức được thì hành chỉ bởi luồng của đối tượng mà phương thức đó thuộc về. Rõ ràng, p và q không thể đồng thời đạt tới được bằng cùng một luồng. Đối với tính bất biến của q dưới phép gán stm, mệnh đề của điều kiện không có can thiệp kéo theo  stmqqp ,interferes' . Từ 'qp  ta kết luận thread = thread’, và do đó bằng định nghĩa của  e:yq,interferes khẳng định q là một điểm điều khiển chờ trả về, nhưng trong trường hợp này thì không đúng, và do đó mệnh đề của điều kiện ước lượng là sai. Kiểm tra sự hợp tác Kiểm tra sự hợp tác đối với tạo đối tượng không bị ảnh hưởng bởi việc thêm vào tính tương tranh. Sự thi hành của các phương thức khác với phương thức start, được thi hành bởi một luồng duy nhất, không bị ảnh hưởng bởi sự có mặt của tính tương tranh. z và z’ là các biến logic mới đại diện cho đối tượng gọi và đối tượng được gọi. Bên - 46 - cạnh điều kiện trước của lời gọi, các bất biến toàn cục, bất biến lớp, ta giả sử rằng sự thi hành được cho phép, có nghĩa là, luồng của đối tượng được gọi chưa được bắt đầu, được định nghĩa bằng startedz'. . Định nghĩa 3.3.5. (Kiểm tra sự hợp tác: Giao tiếp) Một phác thảo chứng minh thỏa mãn kiểm tra sự hợp tác đối với sự giao tiếp, nếu các điều kiện của định nghĩa 2.4.14 đúng đối với các lệnh được liệt kê ở đó với startm  , và thêm vào các trường hợp sau: 1. startCALL : Đối với tất cả các lệnh       3 ! 11 ! 201 :. peypestartep callcall  trong lớp c với 0e của kiểu c’, comm được cho bằng   startedzzzE '.'0  , trong đó     returnstmqeyq callcall ;: 3 ? 22 ? 2  là thân của của phương thức run của c’ có các tham biến hình thức u , và các biến cục bộ v trừ các tham biến hình thức. Bất biến của lớp được gọi là '1 cIq  . Hơn nữa, commf là    vInitzEvu ,:','  , 1obsf là  zEyz 11 :.  , và 2obsf là  '':''. 22 zEyz  . 2. skipstartCALL : Đối với các lệnh phía trên, các phương trình phải đúng với khẳng định comm được cho bằng   trueqqstartedzzzE  320 ,'.' , 1q và 1obsf như phần trên, và commf và 2obsf là lệnh rỗng. - 47 - CHƯƠNG 4. BỘ ĐIỀU PHỐI LẶP LẠI 4.1. Cú pháp Các phương thức được bao bọc bởi một từ bổ nghĩa modif phân biệt giữa các phương thức đồng bộ và không đồng bộ. Trong phần tiếp theo ta tham chiếu tới các lệnh trong thân của một phương thức đã đồng bộ như là đang được đồng bộ. Do vậy, ta xem các phương thức thêm vào được định nghĩa trước là wait, notify, và notifyAll modif ::= nsyn | sync meth ::= modif m (u, …, u) { stm; return retexp } runmeth ::= nsync run () { stm; return} waitmeth ::= nsync wait () { ?signal; getlockreturn } notifymeth ::= nsync notify () {!signal; return } notifyAllmeth ::= nsync notifyAll () { !signal_all; return } predefmeth ::= notifyAllnotifywaitstart methmethmethmeth class ::= class c { meth … meth predefrun methmeth } mainclass ::= class prog ::= class … class mainclass Các định nghĩa của cú pháp sử dụng các câu lệnh bổ trợ !sinal, !signal_all, ?signal, và getlockreturn mô tả ở mức cao của kỹ thuật trừu tượng hóa signal-and- continue dưới các phương thức wait, notify, và notifyAll. 4.2. Ngữ nghĩa Các ngữ nghĩa toán tử mở rộng các ngữ nghĩa của concJava bằng các quy tắc sau, trong đó quy tắc CALL được thay thế. Đối với các lời gọi phương thức được đồng bộ hóa, khóa của đối tượng được gọi phải là tự do hoặc được sở hữu bởi luồng đang thi hành, do vậy được biểu thị bởi vị từ owns, được định nghĩa bên dưới. - 48 - Các quy tắc còn lại quản lý các ngữ nghĩa của các phương thức điều phối wait, notify, và notifyAll. Trong cả ba trường hợp luồng gọi phải sở hữu khóa của đối tượng được gọi (quy tắc monitorCALL ). Một luồng có thể khóa chính nó trong một đối tượng mà nó sở hữu khóa bằng cách thi hành phương thức wait của đối tượng, do đó nó giải phóng khóa và đưa chính nó vào trong tập đợi của đối tượng. Tập đợi  ,Twait của một đối tượng được cho như là một tập của tất cả các ngăn xếp trong T với một phần tử ở đỉnh ngăn xếp có dạng  stmsignal;?,, . Sau khi đóng băng chính nó, luồng đợi thông báo từ luồng thi hành phương thức notify của đối tượng. Câu lệnh !signal trong phương thức notify do đó kích hoạt lại một luồng duy nhất được chọn đang chờ thông báo trong đối tượng được cho (quy tắc SIGNAL). Tương tự như tập chờ, tập được thông báo  ,Tnotified của đối tượng  biểu thị tập tất cả các ngăn xếp trong T với phần tử ở đỉnh ngăn xếp có dạng  getlockreturn,, , nghĩa là, các luồng được thông báo và cố gắng giữ khóa lại. Theo quy tắc waitRETURN , luồng được thông báo chỉ có thể tiếp tục thi hành getlockreturn sau thông báo nếu khóa là tự do. Chú ý rằng luồng thông báo không được bàn giao lại khóa cho một luồng đang được thông báo nhưng tiếp tục sở hữu nó. Hành vi này được biết đến như là quy tắc điều phối signal-and-continue. Các quy tắc:      cMethbodyumnotifyAllnotifywaitrunstartm  modif,,,,               ,,,0 ' euVale cminitc          CALLstmemeuT Towns     ,;.:,, ,syncmodif 0      ,,',;,, bodystmureceiveT   notifyAllnotifywaitm ,,                monitor c CALL stmmeT stmmeownsVale      ,;.,, ,;.,,,        ,,,;,, ,, cmcminit bodystmreceiveT  - 49 -        waitgetlock RETURN returnstmreceiveT Towns     ,,',;,, ,     ,,, stmT        SIGNAL stmsignalstmsignalT  ,';?,',';!,,        ,',',',, stmstmT          skip SIGNAL stmTstmsignalT Twait   ,,,,;!,, ,            SIGNALALL stmTstmallsignalT TsignalT   ,,,',;_!,, ,'    Nếu không có luồng nào đang đợi trong đối tượng, lệnh !signal của luồng thông báo không có kết quả (quy tắc skipSIGNAL ). Phương thức notifyAll tổng quát phương thức notify ở chỗ thông báo tất cả các luồng đang đợi được thông báo qua sự quảng bá !signal_all (quy tắc SIGNALALL). Kết quả của câu lệnh này được cho bởi định nghĩa  ,Tsignal là           ,;?,,|,,,\ TwaitstmsignalstmTwaitT  . Bằng cách sử dụng các tập đợi và tập được thông báo, ta có thể hình thức hóa vị từ owns: Một luồng  sở hữu khóa của đối tượng  khi và chỉ khi  thi hành phương thức đồng bộ của đối tượng  , nhưng không phải phương thức wait của nó. Vị từ owns (T,  ) là đúng khi và chỉ khi tồn tại một luồng T và một cấu hình    stm,, với stm được đồng bộ hóa và     ,, TnotifiedTwait  . 4.3. Hệ chứng minh 4.3.1. Phác thảo chứng minh Để nắm bắt sự loại trừ lẫn nhau và quy tắc điều phối, biến thể hiện được tích hợp thêm lock có kiểu IntThread  lưu trữ định danh của luồng sở hữu khóa, nếu có, cùng với số của các lời gọi đồng bộ trong chuỗi lời gọi của luồng sở hữu khóa. Giá trị ban đầu - 50 - của khóa 0) (null, free  biểu thị rằng khóa tự do. Các biến thể hiện wait và notified của kiểu  IntThread list là tương đương với các tập wait và notified của các ngữ nghĩa và lưu trữ các luồng đang đợi ở một bộ điều phối, theo thứ tự các luồng được thông báo. Bên cạnh định danh luồng, số của các lời gọi đồng bộ cũng được lưu trữ. Nói cách khác, các biến này nhớ giá trị của khóa cũ trước khi tạm thời ngừng, giá trị này được trả lại khi luồng hoạt động trở lại. Tất cả các biến bổ trợ được khởi tạo một cách bình thường. Đối với các giá trị thread của kiểu Thread và wait của kiểu list ( IntThread  ), ta sẽ viết waitthread  thay vì   waitnthread , với các giá trị n. Theo cú pháp, bên cạnh bổ sung được tích hợp của chương trước, quan sát được gọi ở điểm đầu và điểm cuối của mỗi thân phương thức được đồng bộ hóa thi hành theo thứ tự  lockinclock : và  lockdeclock : . Các ngữ nghĩa của sự tăng khóa      ,instlockinc là   1, nthread đối với    nvlockinst , . Chú ý rằng định danh của luồng sở hữu khóa không những trong trường hợp khóa tự do mà còn trong trường hợp nếu có một luồng đang sở hữu khóa. Tuy nhiên, bởi vì những cập nhật này được thi hành trong các phương thức được đồng bộ, nên các ngữ nghĩa đảm bảo cho trường hợp có một luồng đang sở hữu khóa, luồng sở hữu khóa là luồng đang thực thi, nghĩa là, nếu khóa không tự do thì thành phần luồng của khóa không được sửa đổi. Điều này có nghĩa là, tăng giá trị khóa  n, tạo ra  1, n , trong khi đó tăng một khóa tự do  0,null bởi một luồng  có kết quả là  1, . Giảm khóa  lockdec được thực hiện ngược lại:      ,instlockdec với    nlockinst ,  là  1, n nếu n > 1, và tự do nếu ngược lại. Thay vì các câu lệnh phụ trợ của các ngữ nghĩa, thông báo được thể hiện trong hệ chứng minh dựa trên trạng thái bởi các phép gán phụ trợ trong các biến wait và notified: Các câu lệnh phụ trợ !signal và !signal_all được thay thế bởi các phép gán phụ trợ. Các câu lệnh phụ trợ ?signal không được thể hiện. Điều này có nghĩa là, thông báo được thể hiện bởi duy nhất một phép gán phụ trợ được thi hành bởi luồng đưa ra thông báo. Đối với các luồng đang được thông báo, các điểm điều khiển trước và sau thông báo được mô tả bởi duy nhất một khẳng định trong phương thức wait. Các điểm điều khiển khác có thể được phân biệt bởi các giá trị của các biến phụ trợ tích hợp wait và notified. Vào phương thức wait nhận được quan sát   freelockwaitlockwait ,:,  trả về từ phương thức wait quan sát - 51 -     threadnotifiedgetnotifiedthreadnotifiedgetnotifiedlock ,\,,:,  . Đối với một luồng ThreadVal và một danh sách  IntthreadlistValnotified  ,  ,notifiedget lấy giá trị  n, từ danh sách. Các ngữ nghĩa đảm bảo tính duy nhất của sự kết hợp. Câu lệnh signal! của phương thức notify được thay thế bằng lệnh gán bội phụ trợ  notifiedwaitnotifynotifiedwait ,:,  , trong đó giá trị  notifiedwaitnotify , là một cặp của các tập được cho với một phần tử được chọn, được chuyển từ tập tập wait sang tập notified; nếu tập wait là rỗng, nó là định danh hàm. Cuối cùng, câu lệnh allsignal _! của phương thức notifyAll được thay thế bởi phép gán phụ trợ  ,:, waitnotifiedwaitnotified  . 4.3.2. Kiểm chứng các điều kiện Tính đúng đắn cục bộ và tính đúng đắn ban đầu thì như là đối với concJava . Đối với tính đúng đắn cục bộ, chú ý rằng các điều kiện bao hàm thêm vào tính bất biến đối với các luồng đang thi hành thông báo. Tuy nhiên, ta không cần thêm vào các điều kiện cho trường hợp này, bởi vì kết quả của thông báo được giữ lại bởi một phép gán phụ trợ. Đối với các luồng đang được thông báo, các điểm điều khiển trước và sau thông báo được mô tả bởi một khẳng định. Kiểm tra tính không có can thiệp Các phương thức được đồng bộ của một đối tượng duy nhất chỉ có thể được thi hành tương tranh nếu một trong các cấu hình cục bộ tương ứng đang chờ sự trả về: Nếu các luồng đang thi hành là khác nhau, thì một trong các luồng thi hành trong phương thức không được đồng bộ hóa wait của đối tượng; mặt khác, cả hai cấu hình cục bộ đang thi hành là trong cùng một dãy lời gọi. Định nghĩa 4.3.1. (Tính không có can thiệp) Một phác thảo chứng minh là không có can thiệp, nếu các điều kiện của định nghĩa 3.3.2 đúng đối với tất cả các lớp c, tất cả các phép gán bội ey : với điều kiện p trong c, và tất cả các khẳng định q tại các điểm điều khiển trong c, sao cho hoặc là cả hai p và q không xuất hiện trong một phương thức đồng bộ, hoặc là q là một điểm điều khiển đang chờ sự trả về. Chú ý rằng đối với thông báo, ta cũng yêu cầu tính bất biến của các khẳng định của các luồng đang đợi thông báo. Thông báo được mô tả bằng một phép gán phụ trợ được thi hành bởi luồng thông báo. Điều đó có nghĩa là, cả hai tình trạng đang đợi và tình trạng được thông báo của một luồng bị tạm thời ngừng được thay thế bằng một điểm điều khiển duy nhất trong phương thức wait. Hai tình trạng có thể được phân biệt - 52 - bằng các giá trị của các biến wait và biến notified. Tính bất biến của điều kiện trước của lệnh trả về trong phương thức wait dưới phép gán trong phương thức notify biểu thị quá trình thông báo, trong khi đó tính bất biến của khẳng định thông qua các phép gán thay đổi khóa biểu thị kỹ thuật đồng bộ hóa. Thông tin về giá trị khóa được khai báo từ kiểm tra sự hợp tác bởi vì thông tin này phụ thuộc vào hành vi toàn cục. Ví dụ 4.3.2. Ví dụ này biểu diễn cách nhiều nhất một luồng có thể sở hữu khóa của một đối tượng có thể được sử dụng để biểu diễn sự loại trừ lẫn nhau. Ta sử dụng khẳng định  lockthreadowns , đối với   threadlockthreadnullthread  , trong đó  lockthread là thành phần đầu tiên của giá trị khóa. Cho  lockthreadforfree ,_ là   freelocklockthreadownsnullthread  , . Cho q, được cho bởi  lockthreadowns , , là một khẳng định tại một điểm điều khiển và cho   callcall stmp ?? với  lockthreadforfreep def ,_ là quan sát được gọi tại phần bắt đầu của một phương thức được đồng bộ hóa trong cùng lớp. Chú ý rằng quan sát stm thay đổi giá trị khóa. Điều kiện không có can thiệp     ',interferes'| qstmstmqqpL  đảm bảo tính bất biến của q dưới quan sát stm. Các khẳng định p và q’ kéo theo thread = thread’. Các điểm tại p và q chỉ có thể đạt tới được đồng thời bởi cùng một luồng nếu q mô tả một điểm đang chờ trả về. Nhưng điều đó là sai bởi định nghĩa của vị từ interferes: Nếu q không ở một điểm điều khiển đang chờ trả về, thì mệnh đề của điều kiện ước lượng là sai. Mặt khác, sau sự thi hành của lệnh phụ trợ tích hợp  lockinclock : trong stm ta có  lockthreadowns , , có nghĩa là  lockthreadowns ,' . Kiểm tra sự hợp tác Ta mở rộng kiểm tra sự hợp tác cho concJava với kỹ thuật đồng bộ hóa và với sự thi hành của các phương thức điều phối. Trong các ngôn ngữ trước, khẳng định comm phát biểu rằng các lệnh được cho đại diện các đối tác giao tiếp. Trong ngôn ngữ hiện tại với sự đồng bộ hóa điều phối, giao tiếp luôn luôn được cho phép. Do vậy khẳng định comm phải giữ thêm tính được cho phép của giao tiếp: Trong trường hợp thi hành một phương thức được đồng bộ hóa, khóa của đối tượng phải là tự do hoặc thuộc sở hữu của luồng gọi. Điều này được biểu diễn bởi   threadlockzthreadfreelockz  '.'. , trong đó thread là luồng gọi, z’ là đối tượng được gọi, và trong đó  lockzthread '. là thành phần đầu tiên của giá trị khóa, có nghĩa là, luồng đang sở hữu khóa của z’. Đối với sự thi hành của các phương thức điều phối ta yêu cầu rằng luồng đang thi hành - 53 - đang giữ khóa. Sự trả về từ phương thức wait giả thiết rằng luồng được thông báo và khóa của đối tượng được gọi là tự do. Định nghĩa 4.3.3. (Kiểm tra sự hợp tác: Giao tiếp) Một phác thảo chứng minh thỏa mãn kiểm tra sự hợp tác đối với giao tiếp, nếu các điều kiện của định nghĩa 3.3.5 đúng đối với các lệnh được liệt kê ở đó với ngoại lệ của trường hợp quy tắc CALL, và thêm vào các trường hợp sau đây: 1.CALL: Sự thi hành của các phương thức không được đồng bộ hóa m với  notifyAllnotifywaitstartm ,,, được xử lý như trước đó. Đối với tất cả các lệnh       waitcallcallret peypemeup 3 ! 11 ! 201 :.:  (hoặc là các lệnh này mà không nhận một giá trị) trong lớp c với 0e của kiểu c’, trong đó phương thức  notifyAllnotifywaitstartm ,,, của c’ được đồng bộ hóa với thân     ret callcall ereturnstmqeyq ;: 3 ? 22 ? 2  , các biến hình thức u , và các biến cục bộ v ngoại trừ các biến hình thức, các điều kiện 2.6 và 2.7 phải đúng với các định nghía sau: Bất biến của lớp được gọi là '1 : cIq  . Khẳng định comm được cho bằng     threadlockzthreadfreelockzzzE  '.'.'0 . Hơn nữa, commf là    vInitzEvu ,:','  , 1obsf được cho bằng  zEyz 11 :.  , và 2obsf là  '':''. 22 zEyz  . 2. monitorCALL : Đối với  notifyAllnotifywaitm ,, , comm được cho bằng     threadlockzthreadzzE  '.'0 . 3. waitRETURN : Đối với      3 ! 33 ! 21 : qeyqreturnq retret getlock  trong phương thức wait, comm là  