H. Liu, L. Qin, J. Wang, N. Vemuri, and X. Jia (USA)
Design By Contract, Java, Dynamic Contract Verifier, Static Contract Verifier
Design By Contract (DBC) is a systematic ap proach to specifying and implementing object-oriented software systems. DBC has been proved to greatly benefit software development. However, Java does not natively support DBC. We have developed a compre hensive solution to bring DBC into Java. The static and dynamic contract verifier is the most crucial part of the solution. We have developed a toolset support DBC using these two verifiers. This paper presents details of their design and implimentation. The tool used for dynamic contract verifier is ContractChecker, which generates test code into original Java code, thus enables runtime validation. Static contract verifica tion is done by Static Contract Verifier, which uses an automated theorem prover to verify contract.
Important Links:
Go Back
