How the design of JML accommodates both runtime assertion checking and formal verification
From MaRDI portal
Publication:1776585
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
Formal methodsSpecification languagesJava languageProgram verificationJML languageProgramming by contractRuntime assertion checking
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
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
