Bài giảng Đặc tả hình thức: Chương 11 - Nguyễn Thị Minh Tuyền

Số trang: 20 Loại file: pdf Dung lượng: 406.55 KB Lượt xem: 10 Lượt tải: 0

Hoai.2512

Phí tải xuống: 3,000 VND

Xem trước 2 trang đầu tiên của tài liệu này:

Thông tin tài liệu:

Nội dung của Bài giảng Đặc tả hình thức Chương 11 được trình bày như sau: Cấu trúc của ESC/Java2, chạy ESC/Java2, Platform được hỗ trợ, ứng dụng dựa vào môi trường có, các tùy chọn dòng lệnh, Các file đặc tả,...Mời các bạn cùng tham khảo!
Nội dung trích xuất từ tài liệu:
Bài giảng Đặc tả hình thức: Chương 11 - Nguyễn Thị Minh Tuyền LOGO Đặc tả hình thức Giới thiệu về ESC/Java2 Cách sử dụng và thuộc tính Nguyễn Thị Minh Tuyền Nội dung slide này được dịch từ các slide của David Cok, Joe Kiniry, Eric Poll 1 v ESC/Java §  Extended Static Checker for Java Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức Cấu trúc của ESC/Java2 v ESC/Java2 gồm §  Một pha kiểm tra cú pháp §  Một pha typechecking (kiểm tra loại và cách sử dụng) §  Một pha kiểm tra tĩnh ( diễn giải để tìm ra các lỗi tìm tàng) – chạy một prover behind-the-scenes gọi là Simplify. v Kiểm tra cú pháp và typechecking tạo ra các cảnh báo hoặc lỗi. v Kiểm tra tĩnh đưa ra các cảnh báo. Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức Chạy ESC/Java2 v Tải ESC/Java2 từ §  http://www.kindsoftware.com/products/opensource/ ESCJava2/download.html v Sử dụng ESC/Java2: §  Chạy công cụ bằng lệnh. §  Sử dụng Eclipse plug-in. §  Hướng dẫn cài đặt: http://kindsoftware.com/products/opensource/ ESCJava2/ Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức Platform được hỗ trợ v ESC/Java2 được hỗ trợ trên §  Linux §  MacOSX §  Cygwin on Windows §  Windows (nhưng vẫn còn một số vấn đề về môi trường cần được giải quyết) §  Solaris Nguyễn Thị Minh Tuyền 5 Đặc tả hình thức