LOGO
Đặc tả hình thức
Nguyễn Thị Minh Tuyền
1
Giới thiệu về ESC/Java2
Cách sử dụng và thuộc tính
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
v ESC/Java
§ Extended Static Checker for Java
2
Nguyễn Thị Minh Tuyền
Đặ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.
3
Nguyễn Thị Minh Tuyền
Đặ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/
4
Nguyễn Thị Minh Tuyền
Đặ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
5
Nguyễn Thị Minh Tuyền