Working of ESC/Java2

[rsarva80]

Hi,

 

I have been using ESCJAVA2 on programs that are not annotated.It does generate warnings as it would for an annotated code.Could you please explain how ESC/Java2 produces logical formulas in the absence of annotations?In other words,does ESC/Java2 depends on the program annotations to generate logical formulas(that are proved by an automatic theorem-prover) or something else,say the program code.

 

I would appreciate any reply in this regard.

 

---ESC/Java2 User

 

 

 

The checker is implemented using the technology of program verification. The program is annotated with specifications; the annotated program is presented to a “verification condition generator”, which produces logical formulas .

---

Find out what India is talking about on - Yahoo! Answers India
Send FREE SMS to your friend's mobile from Yahoo! Messenger Version 8. Get it NOW
-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava

[Joseph Kiniry]

Hi,

On 27 Oct, 2006, at 15:59, Rukmini wrote:

> Hi,
>
> I have been using ESCJAVA2 on programs that are not annotated.

Great to hear.

> It does generate warnings as it would for an annotated code.

Right.  This is one of the nice things about ESC/Java2---it can  
reason about both un-annotated code as well as incomplete (but type-
correct) code (e.g., you can have methods that have empty bodies).

> Could you please explain how ESC/Java2 produces logical formulas in  
> the absence of annotations?

Each of your methods has a default specification and assertions are  
automatically generated for the core cases that ESC/Java2 checks,  
e.g., NullPointerExceptions.

> In other words,does ESC/Java2 depends on the program annotations to  
> generate logical formulas (that are proved by an automatic theorem-
> prover) or something else, say the program code.

ESC/Java2 relies upon both, if they are available.  I suggest that  
you read the PLDI paper on ESC/Java to gain a better understanding of  
the tool's behavior.  See
   http://citeseer.ist.psu.edu/flanagan02extended.html

> I would appreciate any reply in this regard.
>
> ---ESC/Java2 User

Thanks for your use and questions!

Joe
---
Joseph Kiniry
School of Computer Science and Informatics
University College Dublin
http://secure.ucd.ie/
http://srg.cs.ucd.ie/



-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
JMLspecs-ESCJava mailing list
JMLspecs-ESCJava@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-escjava