Design And Implementation Of Static Verifier In VeriJava

The reliability of software has always been a concern of the industry and the academy. As the scale and complexity of software systems has grown rapidly, it is emergent to guarantee the software reliability. At the same time, software development methodologies and software engineering have continuously developed and the object-oriented methodology has existed for over 20 years. The O-O method provides software systems with flexibility and reusability along with reliability. Design by contract is a systematic approach to constructing high reliable object-oriented software systems. Bertrand Meyer proposed the concept of design by contract in 1990s and has invented Eiffel programming system to popularize this method. The way of checking program correctness via contract in design by contract stems from early ideas of program verification. Although the compelling value of design by contract lies in the aspect of object-oriented design, the method provides a new possible approach to program verification. In the early 21st century,...