Contract-Based Data Structure Repair Using Alloy

13 years 25 days ago
Contract-Based Data Structure Repair Using Alloy
Contracts and specifications have long been used in object-oriented design, programming and testing to enhance reliability before software deployment. However, the use of specifications in deployed software is commonly limited to runtime checking where assertions form a basis for detecting incorrect program states to terminate the erroneous executions. This paper presents a contractbased approach for data structure repair, which allows repairing erroneous executions in deployed software by repairing erroneous states. The key novelty is the support for rich behavioral specifications, such as those that relate prestates with post-states of the method to accurately specify expected behavior and hence to enable precise repair. The approach is based on the view of a specification as a non-deterministic implementation, which may permit a high degree of non-determinism. The key insight is to use any correct state mutations by an otherwise erroneous execution to prune the non-determinism in th...
Razieh Nokhbeh Zaeem, Sarfraz Khurshid
Added 02 Sep 2010
Updated 02 Sep 2010
Type Conference
Year 2010
Authors Razieh Nokhbeh Zaeem, Sarfraz Khurshid
Comments (0)