Đang chuẩn bị nút TẢI XUỐNG, xin hãy chờ
Tải xuống
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ả,.! | 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 .