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

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