Bài giảng Đặc tả hình thức - Chương 13: Giới thiệu về ESC/Java2-Cảnh báo - Nguyễn Thị Minh Tuyền

LOGO Đặc tả hình thức Nguyễn Thị Minh Tuyền 1 Giới thiệu về ESC/Java2 Cảnh báo Nội dung slide này được dịch từ các slide của David Cok, Joe Kiniry, Eric Poll Đặc tả hình thức Các loại cảnh báo ESC/Java2 v Các cảnh báo ESC/Java2 thường rơi vào các mục sau: §  Cảnh báo về ngoại lệ khi thực thi (runtime exception)(Cast, Null, NegSize, IndexTooBig, IndexNegative, ZeroDiv, ArrayStore). •  Đây là các ngoại lệ khi thực thi phổ biến nhất gây ra bởi các vấn đề khi lập trình. •  Không chứa tất cả các ngoại lệ khi thực thi. 2 Nguyễn Thị Minh Tuyền Đặc tả hình thức Cast warning v Cảnh báo Cast xảy ra khi ESC/Java2 không thể kiểm tra rằng một ClassCastException sẽ không được đưa ra. public class CastWarning { public void m(Object o) { String s = (String)o; } } sinh ra ------------------------------------------------------------------------ CastWarning.java:3: Warning: Possible type cast error (Cast) String s = (String)o; ˆ ------------------------------------------------------------------------ 3 Nguyễn Thị Minh Tuyền Đặc tả hình thức Cast warning Nhưng sẽ OK nếu ta viết: public class CastWarningOK { public void m(Object o) { if (o instanceof String) { String s = (String)o; } } } Với đặc tả JML: public class CastWarningOK2 { //@ requires o instanceof String; public void m(Object o) { String s = (String)o; } } 4 Nguyễn Thị Minh Tuyền Đặc tả hình thức Null warning v  Cảnh báo Null xảy ra khi ESC/Java2 không thể kiểm tra rằng NullPointerException sẽ không được đưa ra. public class NullWarning { public void m(Object o) { int i = o.hashCode(); } } Kết quả: ------------------------------------------------------------------------ NullWarning.java:3: Warning: Possible null dereference (Null) int i = o.hashCode(); ˆ ------------------------------------------------------------------------ Sẽ OK nếu ta viết: public class NullWarningOK { public void m(/*@ non_null */ Object o) { int i = o.hashCode(); } } 5 Nguyễn Thị Minh Tuyền Đặc tả hình thức ArrayStore Warning v  Xảy ra khi ESC/Java không thể kiểm tra việc gán một đối tượng cho một phần tử của mảng không đưa ra ngoại lệ ArrayStoreException. public class ArrayStoreWarning { public void m(Object o) { Object[] s = new String[10]; s[0] = o; } } Kết quả: ------------------------------------------------------------------------ ArrayStoreWarning.java:4: Warning: Type of right-hand side possibly not a subtype of array element type (ArrayStore) s[0] = o; ˆ ------------------------------------------------------------------------ Nhưng sẽ OK nếu ta viết: public class ArrayStoreWarningOK { public void m(Object o) { Object[] s = new String[10]; if (o instanceof String) s[0] = o; } } 6 Nguyễn Thị Minh Tuyền Đặc tả hình thức ZeroDiv, index Warnings v ZeroDiv: xảy ra khi chia số nguyên với mẫu số có thể bằng 0. v NegSize: xảy ra trong một biểu thức cấp phát bộ nhớ: kích thước của một mảng có thể âm. v IndexNegative: xảy ra khi chỉ số index của một mảng có thể âm. v IndexTooBig: xảy ra khi chỉ số index của mảng lơn hơn hoặc bằng kích thước mảng. 7 Nguyễn Thị Minh Tuyền Đặc tả hình thức ZeroDiv, index Warnings v Ví dụ: public class Index { void m() { int i = 0; int j = 8/i; Object[] oo = new Object[i-1]; oo = new Object[10]; i = oo[-1].hashCode(); i = oo[20].hashCode(); } } 8 Nguyễn Thị Minh Tuyền Đặc tả hình thức ZeroDiv, index Warnings v Ví dụ: public class Index { void m() { int i = 0; int j = 8/i; // Causes a ZeroDiv warning Object[] oo = new Object[i-1]; // NegSize warning oo = new Object[10]; i = oo[-1].hashCode(); // IndexNegative warning i = oo[20].hashCode(); // IndexTooBig warning } } _ 9 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các loại cảnh báo ESC/Java2 v Các cảnh báo ESC/Java2 thường rơi vào các mục sau: §  Cảnh báo về ngoại lệ khi thực thi (runtime exception) (Cast, Null, NegSize, IndexTooBig, IndexNegative, ZeroDiv, ArrayStore). §  Cảnh báo về vi phạm đặc tả của phương thức (điều kiện trước, điều kiện sau, các thay đổi). •  Những cảnh báo này xảy ra bởi vi phạm về các đặc tả phương thức do người dùng viết. 10 Nguyễn Thị Minh Tuyền Đặc tả hình thức Pre, Post warnings v  Những cảnh báo này xảy ra để trả lời các điều kiện trước (requires), điều kiện sau (ensures, signals), hay các phát biểu assert. public class PrePost { //@ requires i >= 0; //@ ensures \result == i; public int m(int i){ return i; } //@ ensures \result > 0; public int mm() { int j = m(-1); // Pre warning - argument must be >= 0 return j; } //@ ensures \result > 0; public int mmm() { int j = m(0); return j; } // Post warning - result is 0 and should be > 0 } 11 Nguyễn Thị Minh Tuyền Đặc tả hình thức Frame conditions v  Khi triệu gọi một phương thức, ta phải biết cái gì có thể thay đổi trong phương thức đó. v  Ta sử dụng §  Mệnh đề assignable //@ assignable x, o.x, this.*, o.*, a[*], a[3], a[4..5]; §  Mệnh đề modifies §  Bổ từ pure //@ pure public int getX() { return x; } v  Mệnh đề assignable phát biểu về các trường có thể bị gán giá trị trong một phương thức – đây là tập về cái gì có thể bị thay đổi. Mặc định là assignable \everything; v  Một phương thức pure là assignable \nothing. 12 Nguyễn Thị Minh Tuyền Đặc tả hình thức Frame conditions v  Một cảnh báo Modifies chỉ ra việc cố gắng gán giá trị cho một trường của đối tượng không phải trong một mệnh đề modifies. v  Chú ý: §  Một số vi phạm của mệnh đề modifies có thể được tìm ra tại thời điểm viết đặc tả. 13 Nguyễn Thị Minh Tuyền Đặc tả hình thức Modifies warnings Ví dụ: public class ModifiesWarning { int i; //@ assignable i; void m(/*@ non_null */ ModifiesWarning o) { i = 1; o.i = 2; // Modifies warning } } Ta không biết liệu o có equal với this hay không, vì chỉ có this.i có thể bị gán, vì vậy mà ESC/Java2 sinh ra cảnh báo ------------------------------------------------------------------------ ModifiesWarning.java:7: Warning: Possible violation of modifies clause (Modifies) o.i = 2; // Modifies warning ˆ Associated declaration is "ModifiesWarning.java", line 4, col 6: //@ assignable i; ˆ ------------------------------------------------------------------------ 14 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các loại cảnh báo ESC/Java2 v Các cảnh báo ESC/Java2 thường rơi vào các mục sau: §  Cảnh báo về ngoại lệ khi thực thi (runtime exception) (Cast, Null, NegSize, IndexTooBig, IndexNegative, ZeroDiv, ArrayStore). §  Cảnh báo về vi phạm đặc tả của phương thức (điều kiện trước, điều kiện sau, các thay đổi). §  Các vi phạm non_null (NonNull, NonNullInit) •  Các cảnh báo này liên quan đến các đặc tả tham số hay trường non_null. 15 Nguyễn Thị Minh Tuyền Đặc tả hình thức NonNullInit warning v  Các trường khai báo non_null phải được khởi tạo giá trị để không bị null trong mỗi phương thức khởi tạo, nếu không một cảnh báo NonNullInit được sinh ra. public class NonNullInit { /*@ non_null */ Object o; public NonNullInit() { } } v  Sinh ra ------------------------------------------------------------------------ NonNullInit.java:4: Warning: Field declared non_null possibly not initialized (NonNullInit) public NonNullInit() { } ˆ Associated declaration is "NonNullInit.java", line 2, col 6: /*@ non_null */ Object o; ˆ ------------------------------------------------------------------------ 16 Nguyễn Thị Minh Tuyền Đặc tả hình thức NonNull warning v  Cảnh báo NonNull được sinh ra khi việc gán giá trị được thực hiện cho một trường hay một biến đã được khai báo non_null nhưng ESC/Java2 không thể xác định được giá trị bên phải của biểu thức gán không null. public class NonNull { /*@ non_null */ Object o; public void m(Object oo) { o = oo; } // NonNull warning } v  sinh ra ------------------------------------------------------------------------ NonNull.java:4: Warning: Possible assignment of null to variable declared non_null (NonNull) public void m(Object oo) { o = oo; } // NonNull warning ˆ Associated declaration is "NonNull.java", line 2, col 6: /*@ non_null */ Object o; ˆ ------------------------------------------------------------------------ 17 Nguyễn Thị Minh Tuyền Đặc tả hình thức NonNull warning Nhưng sẽ OK nếu: public class NonNull { /*@ non_null */ Object o; public void m(/*@ non_null */Object oo) { o = oo; } } v  Vì vậy: public class NonNull { /*@ non_null */ Object o; public void m(Object oo) { if (oo != null) o = oo; } } Vì vậy: public class NonNull { /*@ non_null */ Object o; public void m() { o = new Object(); } } _ 18 Nguyễn Thị Minh Tuyền non_null có thể được áp dụng với: •  một trường •  một tham số hình thức •  một giá trị trả về •  một biến cục bộ •  các biến ghost hay hay biến model Đặc tả hình thức Các loại cảnh báo ESC/Java2 v Các cảnh báo ESC/Java2 thường rơi vào các mục sau: §  Cảnh báo về ngoại lệ khi thực thi (runtime exception) (Cast, Null, NegSize, IndexTooBig, IndexNegative, ZeroDiv, ArrayStore). §  Cảnh báo về vi phạm đặc tả của phương thức (điều kiện trước, điều kiện sau, các thay đổi). §  Các vi phạm non null (NonNull, NonNullInit) §  Các đặc tả loop và flow (Assert, Reachable, LoopInv, DecreasesBound). •  Các cảnh báo này được sinh ra bởi các vi phạm về đặc tả trong thân một phương thức. 19 Nguyễn Thị Minh Tuyền Đặc tả hình thức Body assertions v  Assert: cảnh báo xảy ra khi điều kiện trong assert không được thỏa mãn. v  Reachable: không có trong JML, chỉ có trong ESC/Java2, xảy ra với §  //@ unreachable; tương đương §  //@ assert false; v  Ví dụ: public class AssertWarning { //@ requires i >= 0; public void m(int i) { //@ assert i >= 0; // OK --i; //@ assert i >= 0; // FAILS } public void n(int i) { switch (i) { case 0: case 1: case 2: break; default: //@ unreachable; // FAILS } } } 20 Nguyễn Thị Minh Tuyền Đặc tả hình thức Loop assertions v  loop_invariant được đặt trước các lệnh vòng lặp Java (for, while, do ...while), đảm bảo điều kiện trong loop_invariant phải đúng cho mỗi vòng lặp và tại điểm kết thúc của vòng lặp. v  decreases đặt trước các vòng lặp Java để đảm bảo rằng giá trị của biểu thức đặt sau decreases là một một số nguyên không âm và giảm tại mỗi vòng lặp. v  Chú ý: các vòng lặp được kiểm tra bằng cách truy ngược lại vài lần. public class LoopInvWarning { public int max(/*@ non_null */ int[] a) { int m=Integer.MAX_VALUE; //@ loop_invariant (\forall int j; 0<=j && j<i; a[j] <= m); //@ decreases a.length - i - 1; for (int i=0; i<a.length; ++i) { if (m < a[i]) m = a[i]; } return m; } } 21 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các loại cảnh báo ESC/Java2 v Các cảnh báo ESC/Java2 thường rơi vào các mục sau: §  Cảnh báo về ngoại lệ khi thực thi (runtime exception) (Cast, Null, NegSize, IndexTooBig, IndexNegative, ZeroDiv, ArrayStore). §  Cảnh báo về vi phạm đặc tả của phương thức (điều kiện trước, điều kiện sau, các thay đổi). §  Các vi phạm non null (NonNull, NonNullInit) §  Các đặc tả loop và flow (Assert, Reachable, LoopInv, DecreasesBound). §  Các cảnh báo về vi phạm đặc tả lớp có thể xảy ra (Invariant, Constraint, Initially) 22 Nguyễn Thị Minh Tuyền Đặc tả hình thức Class invariant warnings v  Các mệnh đề invariant và constraint phát sinh thêm các điều kiện sau cho mỗi phương thức. Nếu những điều kiện này không được thỏa mãn, các cảnh báo tương ứng sẽ được phát sinh: public class Invariant { public int i,j; //@ invariant i > 0; //@ constraint j > \old(j); public void m() { i = -1; // will provoke an Invariant error j = j-1; // will provoke a Constraint error } } 23 Nguyễn Thị Minh Tuyền Đặc tả hình thức Initially warning v  Một mệnh đề Initially là một điều kiện sau cho mỗi phương thức khởi tạo: public class Initially { public int i; //@ initially i == 1; public Initially() { } // does not set i - Initially warning } v  sinh ra ------------------------------------------------------------------------ Initially.java:5: Warning: Possible violation of initially condition at constructor exit (Initially) public Initially() { } // does not set i - Initially warning ˆ Associated declaration is "Initially.java", line 3, col 20: public int i; //@ initially i == 1; ˆ ------------------------------------------------------------------------ 24 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các loại cảnh báo ESC/Java2 v Các cảnh báo ESC/Java2 thường rơi vào các mục sau: §  Cảnh báo về ngoại lệ khi thực thi (runtime exception)(Cast, Null, NegSize, IndexTooBig, IndexNegative, ZeroDiv, ArrayStore). §  Cảnh báo về vi phạm đặc tả của phương thức (điều kiện trước, điều kiện sau, các thay đổi). §  Các vi phạm non null (NonNull, NonNullInit) §  Các đặc tả loop và flow (Assert, Reachable, LoopInv, DecreasesBound). §  Các cảnh báo về vi phạm đặc tả lớp có thể xảy ra (Invariant, Constraint, Initially). §  Các vấn đề về ngoại lệ (Exception). •  Các cảnh báo này gây ra bởi các ngoại lệ không được khai báo. 25 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các ngoại lệ - Lỗi v Một cảnh báo ngoại lệ cảnh báo rằng chương trình bị ngừng đột ngột bởi việc đưa ra một ngoại lệ không nằm trong danh sách các ngoại lệ trong mệnh đề throws. v  26 Nguyễn Thị Minh Tuyền Throwable Error Exception checked exceptions runtimeException unchecked exceptions Đặc tả hình thức Checked exceptions v Các ngoại lệ Java đã kiểm tra(ví dụ như FileNotFoundException) là các ngoại lệ không phải là RuntimeException: §  Các ngoại lệ đề cập trong phần thân được yêu cầu khai báo trong các mệnh đề throws. §  ESC/Java2 kiểm tra trong suốt quá trình typechecking rằng khai báo ngoại lệ đúng. §  Thường được đặc tả trong mệnh đề signals trong JML. §  ESC/Java2 kiểm tra thông qua diễn giải rằng các điều kiện trong signals đúng. §  Đặc tả mặc định: signals (Exception) true; §  ESC/Java2 giả sử rằng các ngoại lệ được kiểm tra không khai báo trong mệnh đề throws sẽ không xảy ra. 27 Nguyễn Thị Minh Tuyền Đặc tả hình thức Unchecked Exceptions v Các ngoại lệ Java không được kiểm tra (ví dụ như NoSuchElementException) là các RuntimeExceptions: §  Java không yêu cầu các ngoại lệ này phải được khai báo trong mệnh đề throws. §  ESC/Java2 chặt chẽ hơn Java – nó sẽ đưa ra một cảnh báo nếu một ngoại lệ không được kiểm tra có thể được đưa ra nhưng nó không được khai báo trong khai báo throws. v  Cảnh báo: Hiện tại ESC/Java2 sẽ giả sử rằng một ngoại lệ không được kiểm tra không được khai báo sẽ không được đưa ra, thậm chí nó được đặc tả trong mệnh đề signals §  Khai báo tất cả các ngoại lệ không được kiểm tra có thể bị đưa ra( đặc biệt khi không có cài đặt nào để kiểm tra). 28 Nguyễn Thị Minh Tuyền Đặc tả hình thức Exception warning public class Ex { public void m(Object o) { if (!(o instanceof String)) throws new ClassCastException (); } } v  sinh ra ------------------------------------------------------------------------ Ex.java:4: Warning: Possible unexpected exception (Exception) }ˆ Execution trace information: Executed then branch in "Ex.java", line 3, col 32. Executed throw in "Ex.java", line 3, col 32. ------------------------------------------------------------------------ v  Tắt cảnh báo bằng cách: §  Khai báo ngoại lệ trong mệnh đề throws §  Sử dụng //@ nowarn Exception; §  Sử dụng tùy chọn –nowarn Exception 29 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các loại cảnh báo ESC/Java2 v Các cảnh báo ESC/Java2 thường rơi vào các mục sau: §  Cảnh báo về ngoại lệ khi thực thi (runtime exception)(Cast, Null, NegSize, IndexTooBig, IndexNegative, ZeroDiv, ArrayStore). §  Cảnh báo về vi phạm đặc tả của phương thức (điều kiện trước, điều kiện sau, các thay đổi). §  Các vi phạm non null (NonNull, NonNullInit) §  Các đặc tả loop và flow (Assert, Reachable, LoopInv, DecreasesBound). §  Các cảnh báo về vi phạm đặc tả lớp có thể xảy ra (Invariant, Constraint, Initially). §  Các vấn đề về ngoại lệ (Exception). §  Đa luồng (multithreading – Race, RaceAllNull, Deadlock) •  Những cảnh báo này xảy ra bởi các vấn đề về điều khiển. •  Vấn đề đa luồng gây ra bởi sự vắng mặt của việc đồng bộ không được tìm ra. 30 Nguyễn Thị Minh Tuyền Đặc tả hình thức Race conditions v  Race condition là một tình huống trong đó hai luồng truy cập đồng thời vào cùng một biến và không phải là đọc đồng thời (nghĩa là một luồng đọc, một luồng ghi hoặc cả hai luồng ghi đồng thời). v  Để hạn chế điều này, mỗi biến được chia sẻ được điều khiển bởi một hoặc nhiều lock. Nếu một biến được điều khiển bởi một lock, một luồng không được phép truy cập một biến trừ khi nó thỏa mãn lock. v  ESC/Java cho phép các trường được được khai báo monitored bởi hai hay nhiều đối tượng. v  Để đọc một trường được điều khiển, ít nhất một điều khiển phải đúng (hoặc là một Race warning xuất hiện). v  Để ghi một trường được điều khiển, tất cả các điều khiển non-null phải đúng (hoặc là một Race warning được sinh ra). v  Để ghi một trường được điều khiển, ít nhất một trong các điều khiển của nó phải non-null (hoặc là một RaceAllNull warning được sinh ra). 31 Nguyễn Thị Minh Tuyền Đặc tả hình thức Race warnings Ví dụ: public class RaceWarning { //@ monitored int i; void m() { i = 0; // should have a synchronization guard } } v  sinh ra ------------------------------------------------------------------------ RaceWarning.java:6: Warning: Possible race condition (Race) i = 0; // should have a synchronization guard ˆ Associated declaration is "RaceWarning.java", line 2, col 6: //@ monitored ˆ ------------------------------------------------------------------------ 32 Nguyễn Thị Minh Tuyền Đặc tả hình thức Deadlock v Deadlock xảy ra nếu có một vòng lặp các luồng, mỗi luồng giữ một lock mà một số luồng khác trong vòng lặp đó phải đợi để điều khiển đúng. v Một cách để tránh điều này là luôn yêu cầu các điều khiển nằm trong một thứ tự nào đó. v Điều này yêu cầu §  Người dùng phát biểu một thứ tự (bộ phận) cho các điều khiển (thường là sử dụng một axiom). §  ESC/Java sẽ kiểm tra rằng mỗi luồng đạt được các lock theo một thứ tự cho sẵn. v  Mặc định các cảnh báo Deadlock bị tắt. Để sử dụng các cảnh báo này, ta thêm -warn Deadlock. 33 Nguyễn Thị Minh Tuyền Đặc tả hình thức Deadlock warnings v  Ví dụ: public class DeadlockWarning { /*@ non_null */ final static Object o = new Object(); /*@ non_null */ final static Object oo = new Object(); //@ axiom o < oo; //@ requires \max(\lockset) < o; public void m() { synchronized(o) { synchronized(oo) { }} } //@ requires \max(\lockset) < o; public void mm() { synchronized(oo) { synchronized(o) { }} // Deadlock warning } } 34 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các loại cảnh báo ESC/Java2 v Các cảnh báo ESC/Java2 thường rơi vào các mục sau: §  Cảnh báo về ngoại lệ khi thực thi (runtime exception)(Cast, Null, NegSize, IndexTooBig, IndexNegative, ZeroDiv, ArrayStore). §  Cảnh báo về vi phạm đặc tả của phương thức (điều kiện trước, điều kiện sau, các thay đổi). §  Các vi phạm non null (NonNull, NonNullInit) §  Các đặc tả loop và flow (Assert, Reachable, LoopInv, DecreasesBound). §  Các cảnh báo về vi phạm đặc tả lớp có thể xảy ra (Invariant, Constraint, Initially). §  Các vấn đề về ngoại lệ (Exception). §  Đa luồng (multithreading – Race, RaceAllNull, Deadlock) §  Một số cảnh báo khác (OwnerNull, Uninit, Unreadable, Writable) 35 Nguyễn Thị Minh Tuyền Đặc tả hình thức Một số cảnh báo khác v Uninit: được sử dụng với annotation uninitialized v OwnerNull: xem trong hướng dẫn ESC/Java. v Unreadable: xảy ra với annotation readable_if trên các biến được chia sẻ v Writable: xảy ra với annotation writable_if trên các biến được chia sẻ. 36 Nguyễn Thị Minh Tuyền Đặc tả hình thức Trace information v  Đối với một thân chương trình phức tạp, các thông điệp cảnh báo cung cấp một số thông tin về các nhánh if-then-else gây ra cảnh báo đó: public class Trace { //@ ensures \result > 0; int m(int i) { if (i == 0) return 1; if (i == 2) return 0; return 4; } } v  sinh ra Trace.java:8: Warning: Postcondition possibly not established (Post) }ˆ Associated declaration is "Trace.java", line 2, col 6: //@ ensures \result > 0; ˆ Execution trace information: Executed else branch in "Trace.java", line 4, col 4. Executed then branch in "Trace.java", line 5, col 16. Executed return in "Trace.java", line 5, col 16. 37 Nguyễn Thị Minh Tuyền Đặc tả hình thức Phản ví dụ v Khi một đặc tả không hợp lệ, ESC/Java2 có thể sẽ sinh ra một ngữ cảnh phản ví dụ. v Một ngữ cảnh đầy đủ sẽ sinh ra với tùy chọn –counterexample. v Các phản ví dụ này thường khó đọc, nhưng có thể cung cấp thông tin về lý do lỗi. v Các phản ví dụ đưa ra các công thức mà prover tin là đúng, nếu có gì đó mà ta nghĩ không đúng, thì đó là gợi ý để giải quyết vấn đề. 38 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ về đọc phản ví dụ public class Alias { private /*@ spec_public non_null */ int[] a = new int[10]; private /*@ spec_public @*/ boolean noneg = true; /*@ public invariant noneg ==> @ (\forall int i; 0= 0); @*/ //@ requires 0<=i && i < a.length; public void insert(int i, int v) { a[i] = v; if (v < 0) { noneg = false; } } } 39 Nguyễn Thị Minh Tuyền Đặc tả hình thức Alias.java:17: Warning: Possible violation of invariant (Invariant) Associated declaration is ..., line 7, col 13: /*@ public invariant noneg ==> ... ^ Possibly relevant .. from counterexample context: (vAllocTime(brokenObj) < alloc) ... Execution trace information: Executed then branch in ..., line 16, col 15. Counterexample context: (intFirst <= v:14.32) ... 40 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đối tượng Nghĩa brokenObj object violating invariant typeof(brokenObj) its type brokenObj.(noneg:4.38) its nonneg field brokenObj.(a@pre:2.44) its a field tmp0!a:15.4 another object 41 Nguyễn Thị Minh Tuyền