TÌM HIỂU CÔNG NGHỆ DESIGN BY CONTRACT VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ CHO C# - 8

Chia sẻ: Cao Tt | Ngày: | Loại File: PDF | Số trang:12

Thêm vào BST

Báo xấu

115
lượt xem 6
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# nhỏ hơn một giá trị cho trước Yêu cầu đối tượng nhập vào LessThanOrEqual hoặc trả về phải nhỏ hơn hoặc cho trước Yêu cầu số thành phần của đối tượng nhập MaxCount vào hoặc trả về phải nhỏ hơn hoặc bằng một giá trị cho trước Quy ước chiều dài tối đa của MaxLength một chuỗi là một giá trị cho trước Yêu cầu số thành phần của đối tượng nhập MinCount vào hoặc trả về phải lớn hơn hoặc bằng một giá trị...

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: TÌM HIỂU CÔNG NGHỆ DESIGN BY CONTRACT VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ CHO C# - 8

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# nhỏ hơn một giá trị cho trước Yêu cầu đối tượng nhập vào Void hoặc trả về phải SetData([LessThanOrEqual (5)] LessThanOrEqual nhỏ hơn hoặc int value) {} bằng một giá trị //value
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# một chuỗi là //str.Length >= 10 một giá trị cho trước Yêu cầu đối tượng nhập vào Void SetData([NotEqual (5)] int hoặc trả về phải value) {} NotEqual “not equal” với //value != 5 một giá trị cho trước Quy ước giá trị nhập vào hay trả Void SetData([OneOf về của một giá (1,3,5,7,9,10)] int value) {} OneOf trị phải nằm //value có giá trị là một trong các trong các giá trị giá trị sau : [1,3,5,7,9,10] cho trước …. 15.4. Ví dụ lớp Stack private Object[] representation; public int count; // inv: count>=0 (count khong am) public int capacity;// inv: count=0 // [Requires ("size >= 0")] [Ensures ("representation != null && capacity == size && IsEmpty()")] public MyStack([GreaterThanOrEqual (0)]int size) { 86
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# capacity = size; representation = new Object[capacity]; } [Requires ("!IsFull()")] [Ensures ("!IsEmpty() && (int)representation[count-1] == obj")] public void put(int obj) { representation[count++] = obj; } [Requires ("!IsEmpty()")] [Ensures ("!IsFull()")] public void remove() { --count; } [Ensures ("result == (count == capacity)")] public bool IsFull() { return count == capacity; } [Ensures ("result == (count == 0)")] public bool IsEmpty() { return count == 0; } 87
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# [Requires ("position >= 0 && position < count")] [Ensures ("current == position")] public void SetCurrentItem(int position) { current = position; } [Ensures ("current == count - 1")] public void ResetCurrentItem() { current = count - 1; } [Requires ("!IsEmpty()")] [Ensures ("result != null && current >= 0")] public Object nextItem() { return representation[current--]; } Chương 16: Kết quả thực nghiệm: công cụ DCS 16.1. Nguyên lý làm việc DCS là một Add-In trong môi trường Visual C#, nguyên lý làm việc của DCS là bắt sự kiện OnBuildBegin của project, thực hiện những bước sau: Duyệt qua tất cả những lớp của project (mỗi lớp ứng với một file *.cs, trừ file AssemblyInfo.cs) và lưu thông tin của mỗi lớp (tên lớp, tên file, tên những lớp dẫn xuất). Trong mỗi lớp, chương trình thực hiện những bước sau: − Kiểm tra xem lớp có chứa những xác nhận (Invariant, PreCondition, PostCondition) hay không. Lưu thông tin của Invariant (các mệnh đề và thông báo 88
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# tương ứng của Invariant) nếu có, sau đó, duyệt qua từng hàm trong lớp, trong mỗi hàm, thực hiện những bước sau: + Kiểm tra hàm có PreCondition hoặc PostCondition hay không. Nếu có, lưu lại thông tin của hàm. Thông tin lưu trữ gồm có: Tên hàm, PreCondition và PostCondition (lưu các mệnh đề và thông báo). + Đổi tên hàm, nếu lớp có Invariant, tất cả tên hàm sẽ được đổi, nếu không có Invariant, chỉ những hàm có PreCondition hoặc PostCondition mới được đổi tên. Tên hàm được đổi như sau: Tên hàm mới = @origin_[Tên hàm cũ] − Dựa vào thông tin đã lưu trữ được, bổ sung thông tin về những xác nhận của các lớp dẫn xuất cho mỗi lớp. Việc lưu trữ này thực hiện bằng cách duyệt qua tất cả các lớp. Trong đó, ở mỗi lớp: + Duyệt qua tất cả tất cả những lớp dẫn xuất của lớp này (đã được lưu trữ), lưu thông tin Invariant của những lớp dẫn xuất. + Duyệt qua các hàm, hàm nào là hàm cài đặt lại sẽ được lưu trữ thông tin về Assertion của lớp dẫn xuất. Phát sinh source code bổ sung để kiểm tra các xác nhận cho các lớp. Trong mỗi lớp, source code sẽ được thêm vào phía dưới của source code hiện tại. Mỗi hàm sẽ phát sinh source code tương ứng của mình. Với mỗi hàm, dựa vào thông tin đã lưu trữ, source code được phát sinh như sau: [Khai báo hàm theo tên hàm cũ] { Gọi hàm kiểm tra PreCondition Gọi hàm kiểm tra Invariant Gọi hàm gốc (hàm đã được đổi tên @origin_*) Gọi hàm kiểm tra PostCondition Gọi hàm kiểm tra Invariant } 89
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# [Hàm kiểm tra PreCondition] { Các câu lệnh kiểm tra các mệnh đề và xuất thông báo tương ứng của PreCondition } [Hàm kiểm tra Invariant] { Các câu lệnh kiểm tra các mệnh đề và xuất thông báo tương ứng của Invariant } [Hàm kiểm tra PostCondition] { Các câu lệnh kiểm tra các mệnh đề và xuất thông báo tương ứng của PostCondition } Ví dụ: Hàm và PreCondition, PostCondition, Invariant: /* @#$Require: !IsFull() # Stack Full @#$Ensure: !IsEmpty() (int)representation[count-1] == obj count == OLD_count + 1 $int # New count = Old count + 1 */ public void put(int obj) 90
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# { representation[count++] = obj; } /* @#$Invariant: count >= 0 count = 0 */ 91
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Code phát sinh: public void put(int obj) { int OLD_count = count; if(put_PreCondition(obj)!="") throw new Exception("PreCondition Violated at [MyStack - public void put(int obj)]:" +put_PreCondition(obj)); if(put_Invariant(obj)!="") throw new Exception("Invariant Violated at [MyStack]:" +put_Invariant(obj)); @origin_put(obj); if(put_PostCondition(obj,OLD_count)!="") throw new Exception("PostCondition Violated at [MyStack - public void put(int obj)]:" +put_PostCondition(obj,OLD_count)); if(put_Invariant(obj)!="") throw new Exception("Invariant Violated at [MyStack]:" +put_Invariant(obj)); } private string put_PreCondition(int obj) { if (!(!IsFull() )) return " Stack Full"; return ""; } 92
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# private string put_Invariant(int obj) { if (!(count >= 0)) return " "; if (!(count = 0)) return " "; return ""; } private string put_PostCondition(int obj,int OLD_count) { if (!(!IsEmpty())) return " "; if (!((int)representation[count-1] == obj)) return " "; if (!(count == OLD_count + 1 )) return " New count = Old count + 1"; return ""; } Project được biên dịch theo source code mới. Bắt sự kiện OnBuildDone của project, thực hiện việc trả lại source code như cũ cho project. 93
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 16.2. Thiết kế 16.2.1. Tổng thể Hình 16-1: Sơ đồ thiết kế tổng thể Danh sách các lớp đối tượng: STT Tên Ý nghĩa Màn hình cho phép người dùng enable hoặc disable 1 Configuration chức năng kiểm tra của PreCondition, PostCondition, Invariant. Lớp chính của chương trình, đây là lớp quản lý mọi 2 Connect thao tác của Add-In với project. 94
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Lớp đối tượng để lưu trữ thông tin của project hiện 3 ProjectInfo hành. Lớp đối tượng để lưu trữ thông tin của một lớp trong 4 ClassInfo project. Lớp đối tượng để lưu trữ thông tin của một phương 5 FunctionInfo thức trong class. Lớp đối tượng để lưu trữ thông tin của một Assertion 6 Assertion (precondition, postcondition, invariant) Lớp đối tượng chứa những hàm riêng, không thuộc 7 Extra trách nhiệm của những lớp trên. 16.2.2. Chi tiết các lớp đối tượng 16.2.2.1 Màn hình Configuration Hình 16-2: Màn hình Configuration 95
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Hình 16-3: Chi tiết màn hình Configuration Danh sách các đối tượng thể hiện: STT Tên Loại / Kiểu Ý nghĩa Xác định có sử dụng PreCondition 1 chkPreCondition checkbox hay không. Xác định có sử dụng PostCondition 2 chkPostCondition checkbox hay không. Xác định có sử dụng Invariant hay 3 chkInvariant checkbox không. Xác định có sử dụng PreCondition của 4 chkBasePre checkbox những lớp dẫn xuất hay không. Xác định có sử dụng PostCondition 5 chkBasePost checkbox của những lớp dẫn xuất hay không. Xác định có sử dụng Invariant của 6 chkBaseInv checkbox những lớp dẫn xuất hay không. Đồng ý với những thông số đã chọn 7 btnOK Button và thoát khỏi màn hình 8 btnClose Button Thoát khỏi màn hình 96