LOGO
Đặc t hình thc
Nguyn Th Minh Tuyn
1
Gii thiu v ESC/Java2
Cách s dng và thuc tính
Ni dung slide này được dch t các slide ca David Cok, Joe Kiniry, Eric Poll
Đặc t hình thc
vESC/Java
§Extended Static Checker for Java
2
Nguyn Th Minh Tuyn
Đặc t hình thc
Cu trúc ca ESC/Java2
vESC/Java2 gm
§Mt pha kim tra cú pháp
§Mt pha typechecking (kim tra loi và cách s dng)
§Mt pha kim tra tĩnh ( din gii để tìm ra các li tìm
tàng) – chy mt prover behind-the-scenes gi là
Simplify.
vKim tra cú pháp và typechecking to
ra các cnh báo hoc li.
vKim tra tĩnh đưa ra các cnh báo.
3
Nguyn Th Minh Tuyn
Đặc t hình thc
Chy ESC/Java2
vTi ESC/Java2 t
§http://www.kindsoftware.com/products/opensource/
ESCJava2/download.html
vS dng ESC/Java2:
§Chy công c bng lnh.
§S dng Eclipse plug-in.
§Hướng dn cài đặt:
http://kindsoftware.com/products/opensource/
ESCJava2/
4
Nguyn Th Minh Tuyn
Đặc t hình thc
Platform được h tr
vESC/Java2 được h tr trên
§Linux
§MacOSX
§Cygwin on Windows
§Windows (nhưng vn còn mt s vn đề v môi
trường cn được gii quyết)
§Solaris
5
Nguyn Th Minh Tuyn