Are the Logical Foundations of Verifying Compiler Prototypes Matching user Expectations? |
| |
Authors: | Patrice Chalin |
| |
Affiliation: | (1) Dependable Software Research Group (DSRG), Department of Computer Science and Software Engineering, Concordia University, Montréal, QC, H3G 1M8, Canada |
| |
Abstract: | The verifying compiler (VC) project proposals suggest that mainstream software developers are its targeted end-users. Like other software engineering efforts, the VC project success depends on appropriate end-user consultation. Industrial use of program assertions for the purpose of run-time assertion checking (RAC) is becoming commonplace. A likely next step on the path to VC adoption is the use of assertions in extended static checking (ESC), a fully automated form of static program verification (SPV). Unfortunately, all current VC prototypes supporting SPV, adopt a semantics which is unsound relative to the standard run-time interpretation of assertions. In this article, we report on the results of a survey in which we asked industrial developers what logical semantics they want program assertions to have, and whether consistency across RAC and SPV tools is important. Survey results indicate that developers are in favor of a semantics for assertions that is compatible with their current use in RAC. |
| |
Keywords: | Assertions Industrial practice Survey Logical foundations Runtime assertion checking Static program verification Extended static checking Design by contract |
本文献已被 SpringerLink 等数据库收录! |
|