Weakest pre-condition reasoning for Java programs with JML annotations

DOI10.1016/j.jlap.2003.07.005zbMath1073.68024OpenAlexW2031111340MaRDI QIDQ1881666

Bart Jacobs

Publication date: 14 October 2004

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2003.07.005

zbMATH Keywords

JavaProgram correctnessWeakest preconditionProgram logics

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Related Items

The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML, Specification and verification challenges for sequential object-oriented programs, Verification of object-oriented programs: a transformational approach, Verification conditions for source-level imperative programs, All-Path Reachability Logic, WP Semantics and Behavioral Subtyping, A proof outline logic for object-oriented programming

Uses Software

• KRAKATOA
• PVS
• JML
• HOL
• ESC/Java
• LOOP

Cites Work

• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Source code verification of a secure payment applet
• Programming as a Discipline of Mathematical Nature
• A case study in class library verification: Java's vector class
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item