A logic for the Java modeling language JML

DOI10.1007/3-540-45314-8_21MaRDI QIDQ2764132zbMATH OpenFDO

Authors Bart Jacobs, Erik Poll

Publication date 22 January 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2029/20290284

Mathematics Subject Classification ID

Theory of programming languages (68N15) General topics in artificial intelligence (68T01) Logic in artificial intelligence (68T27) Computing methodologies and applications (68U99)

Recommendations

• The LOOP compiler for Java and JML
• Weakest pre-condition reasoning for Java programs with JML annotations
• Hoare logic for Java in Isabelle/HOL
• Theorem Proving in Higher Order Logics
• ZB 2005: Formal Specification and Development in Z and B

Cited in

(20)

• How the design of JML accommodates both runtime assertion checking and formal verification
• Compositionality for quantitative specifications
• Coalgebras and monads in the semantics of Java
• Weakest pre-condition reasoning for Java programs with JML annotations
• Refinement checking on parametric modal transition systems
• A program logic for resources
• Specification and verification challenges for sequential object-oriented programs
• The LOOP compiler for Java and JML
• Proving Theorems About JML Classes
• scientific article; zbMATH DE number 1953020 (Why is no real title available?)
• Verification conditions for source-level imperative programs
• A dynamic logic for deductive verification of multi-threaded programs
• Modular specification of frame properties in JML
• scientific article; zbMATH DE number 2090026 (Why is no real title available?)
• Tools and Algorithms for the Construction and Analysis of Systems
• A Bytecode Logic for JML and Types
• ZB 2005: Formal Specification and Development in Z and B
• FM 2005: Formal Methods
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• Lazy behavioral subtyping

Describes a project that uses

Uses Software

• Isabelle
• PVS
• LOOP
• JML

This page was built for publication: A logic for the Java modeling language JML

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2764132)