DEBUGGING PROGRAMS WITH CONTRACT INFORMATION

In this work, we present a debugging methodology for debugging programs with contract information. The contracts are specified using pre and post conditions for the functions present in the program being debugged. A detailed function execution sequence trace containing the function invokation chain along with actual parameter values is given to us. Our debugging methodology analyzes the trace and attempts to localize the function(s) that have been called violating their contracts, thereby leading to the possibility of a bug. We have implemented the proposed automated debugging methodology into a prototype tool.