Generating high confidence contracts without user input using Daikon and ESC/Java2

dc.contributor.authorRayakota, Balaji
dc.date.accessioned2013-05-01T13:54:19Z
dc.date.available2013-05-01T13:54:19Z
dc.date.graduationmonthMay
dc.date.issued2013-05-01
dc.date.published2013
dc.description.abstractInvariants are properties which are asserted to be true at certain program points. Invariants are of paramount importance when proving program correctness and program properties. Method, constructor, and class invariants can serve as contracts which specify program behavior and can lead to more accurate reuse of code; more accurate than comments because contracts are less error prone and they may be proved without testing. Dynamic invariant generation techniques run the program under inspection and observe the values that are computed at each program point and report a list of invariants that were observed to be possibly true. Static checkers observe program code and try to prove the correctness of annotated invariants by generating proofs for them. This project attempts to get strong invariants for a subset of classes in Java; there are two phases first we use Daikon, a tool that suggests invariants using dynamic invariant generation techniques, and next we get the invariants checked using ESC/Java2, which is a static checker for Java. In the first phase an ‘Instrumenter’ program inspects Java classes and generates code such that sufficient information is supplied to Daikon to generate strong invariants. All of this is achieved without any user input. The aim is to be able to understand the behavior of a program using already existing tools.
dc.description.advisorTorben Amtoft
dc.description.degreeMaster of Science
dc.description.departmentDepartment of Computing and Information Science
dc.description.levelMasters
dc.identifier.urihttp://hdl.handle.net/2097/15731
dc.language.isoen
dc.publisherKansas State University
dc.rights© the author. This Item is protected by copyright and/or related rights. You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use. For other uses you need to obtain permission from the rights-holder(s).
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/
dc.subjectSoftware Contracts
dc.subjectAutomatic Invariant Generation
dc.subjectDaikon
dc.subjectESC/Java2
dc.subject.umiComputer Science (0984)
dc.titleGenerating high confidence contracts without user input using Daikon and ESC/Java2
dc.typeReport

Files

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
BalajiRayakota2013rev.pdf
Size:
706.36 KB
Format:
Adobe Portable Document Format
Description:

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.62 KB
Format:
Item-specific license agreed upon to submission
Description: