| 摘要 |
<p>Disclosed is a software specification proof support device which, when a software specification proof fails, is capable of correcting the software specification without operations for confirmation and selection of correction candidates. By extracting from the inputted software specification the invariant condition candidate list thereof, inferring from the aforementioned software specification invariant condition candidates extracted from the aforementioned invariant condition candidate list, and adding to the aforementioned software specification the inferred invariant condition candidates, the software proof support device corrects the software specification.</p> |
