作者: Matthias Felleisen , Cormac Flanagan
DOI:
关键词:
摘要: A major cause of software unreliability is the misapplication primitive operations, such as taking car nil, dividing by zero, or using an invalid array index. These errors are traditionally discovered extensive testing and debugging, but this approach unsatisfactory because it time-consuming may not identify all potential errors. We suggest to address problem with sophisticated static debugging systems. Recent advances in proof technology have brought advanced systems within reach. Methods like control-flow analysis set-based establish invariants that can potentially faulty program operations. Past research, however, only focused on synthesis completely neglected their presentation programmer. believe programmer must be able inspect inferred browse underlying proof. Then, if some set invariant contains surprising elements, determine whether result a weakness system uncovers flaw program. This paper presents MrSpidey, user-friendly, interactive debugger integrated into DrScheme, our development environment. MrSpidey exposes those operations signal during execution; describes sets values expressions assume; also provides graphical explanation how flow through Using easily eliminate causes run-time Experimental results support belief expedites process debugging.