How the design of JML accommodates both runtime assertion checking and formal verification

DOI10.1016/j.scico.2004.05.015zbMath1075.68009OpenAlexW2035529004MaRDI QIDQ1776585

Yoonsik Cheon, Curtis Clifton, Clyde Ruby, David R. Cok, Gary T. Leavens

Publication date: 12 May 2005

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://lib.dr.iastate.edu/cs_techreports/355

zbMATH Keywords

Formal methodsSpecification languagesJava languageProgram verificationJML languageProgramming by contractRuntime assertion checking

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (12)

The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML ⋮ Towards imperative modules: reasoning about invariants and sharing of mutable state ⋮ On assertion-based encapsulation for object invariants and simulations ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Observational purity and encapsulation ⋮ Integrating a formal method into a software engineering process with UML and Java ⋮ An assertion-based proof system for multithreaded Java ⋮ Fifty years of Hoare's logic ⋮ JMLUnit: The Next Generation ⋮ Verification of Equivalent-Results Methods ⋮ A proof outline logic for object-oriented programming ⋮ Verifying Whiley programs with Boogie

Uses Software

• jContractor
• LARCH
• Eiffel
• Daikon
• JML
• ESC/Java
• Korat
• JUnit

This page was built for publication: How the design of JML accommodates both runtime assertion checking and formal verification