[an error occurred while processing this directive]

Diploma Thesis

Type of project:
Diploma Thesis February 2009 - June 2009

Flaviu Roman

Improving relevancy of dynamically-inferred contracts in Eiffel

Supervising Assistant:
Nadia Polikarpova


This project involves proposing, trying out and evaluating some heuristics that can help filtering out the uninteresting assertions from CITADEL's output.There are already two ideas that we would like to be implemented. The first is that, since most functions in Eiffel are pure, in a function's postcondition we are interested only in properties of its return value. So, we can filter out all the assertions that do not contain "Result" variable. Another heuristic deals with loop invariant inference. In loop invariants we can try filtering out all the assertion that do not contain variables, mentioned explicitly in the loop body. It would be nice to evaluate, whether the positive effect of such filtering (removing uninteresting assertions) exceeds the negative effect (losing some relevant ones).
Other heuristics can be proposed. Another possibility would be to apply some artificial intelligence techniques to classify inferred assertions.