A Verification-centric Software Development Process for Java
0
komentar
A Verification-centric Software Development Process for Java | Design by Contract (DBC) is an oft-cited, but rarely followed, programming practice that focuses on writing formal specifications first, and writing code that fulfills those specifications second. The development of static analysis tools over the past several years has made it possible to fully embrace DBC in Java systems by writing, type checking, and consistency checking rich behavioral specifications for Java before writing any code. This paper discusses a DBCbased, verification-centric software development process for Java that integrates the Business Object Notation (BON), the Java Modeling Language, and several associated tools including the BON compiler BONC, the ESC/Java2 static checker, a runtime assertion checker, and a specification-based unit test generator. This verification-centric process, reinforced by its rich open source tool support, is one of the most advanced, concrete, open, practical, and usable processes available today for rigorously designing and developing software systems.
Design by Contract (DBC) [1] is a design technique for (usually object-oriented) software that uses assertions both to document and enforce restrictions on data and to specify class and method behavior. The Business Object Notation (BON) [2] is an analysis and design notation for objectoriented systems based on DBC. Both were originally developed for use with the Eiffel programming language; DBC has since been added to many other programming languages through various language extensions and preprocessors.
Ideally, developers using the DBC technique write formal specifications (the contracts) for their software first, and write executable code only after completing, and performing at least some basic checking of, the contracts. However, tool support for DBC has until recently been limited primarily to runtime assertion checkers and unit test generators. There has been little support, beyond basic type checking, for verifying the logical consistency of contracts that have no implementations. In essence, the “design” component of DBC has been absent; DBC has meant writing contracts and code in tandem and using runtime assertion checking (RAC) and generated unit tests to check the contracts and code simultaneously. Unfortunately, when code is written in this way, it is often difficult to determine whether problems detected by RAC and unit testing are caused by errors in the code or by errors in the contracts. Download free A Verification-centric Software Development Process for Java.pdf here
Design by Contract (DBC) [1] is a design technique for (usually object-oriented) software that uses assertions both to document and enforce restrictions on data and to specify class and method behavior. The Business Object Notation (BON) [2] is an analysis and design notation for objectoriented systems based on DBC. Both were originally developed for use with the Eiffel programming language; DBC has since been added to many other programming languages through various language extensions and preprocessors.
Ideally, developers using the DBC technique write formal specifications (the contracts) for their software first, and write executable code only after completing, and performing at least some basic checking of, the contracts. However, tool support for DBC has until recently been limited primarily to runtime assertion checkers and unit test generators. There has been little support, beyond basic type checking, for verifying the logical consistency of contracts that have no implementations. In essence, the “design” component of DBC has been absent; DBC has meant writing contracts and code in tandem and using runtime assertion checking (RAC) and generated unit tests to check the contracts and code simultaneously. Unfortunately, when code is written in this way, it is often difficult to determine whether problems detected by RAC and unit testing are caused by errors in the code or by errors in the contracts. Download free A Verification-centric Software Development Process for Java.pdf here
Categories:
Programming
If You Like This Post, Share it With Your Friends & Peers
0 komentar:
Post a Comment