Content deleted Content added
m →Techniques using Formal Verification: Add internal pointer to Program synthesis |
m →Test-and-Validate Techniques: Add internal pointer for oracle and assertions Bill |
||
Line 19:
==Test-and-Validate Techniques==
In Test-and-Validate approaches, program repair is performed with respect to an [[Oracle (software testing)|oracle]], encompassing the desired functionality of the program, which is used for validation of the generated fix. A simple example is a test-suite - the input/output pairs specify the functionality of the program, possibly captured in [[Assertion (software development)|assertions]]. This oracle can in fact be divided between the ''bug oracle'' that detects faulty behaviour, and the ''regression oracle'', which encapsulates the functionality any program repair method must preserve.
A variety of tools are employed to generate a candidate repair, typically either deterministic approaches using solvers for [[Satisfiability Modulo Theories]] (SMT)
| |||