A Hoare calculus for verifying Java realizations of OCL-constrained design models

DOI10.1007/3-540-45314-8_22MaRDI QIDQ2764133zbMATH OpenFDO

Authors Bernhard Reus, Rolf Hennicker, Martin Wirsing

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/20290300

Mathematics Subject Classification ID

General topics in artificial intelligence (68T01) Logic in artificial intelligence (68T27) Computing methodologies and applications (68U99)

Recommendations

• scientific article; zbMATH DE number 5499373
• Hoare logic for Java in Isabelle/HOL
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 2090288

Cited in

(5)

• Semantics and logic of object calculi
• An assertion-based proof system for multithreaded Java
• Observable behavior of dynamic systems: component reasoning for concurrent objects
• A homage to Martin Wirsing
• Towards verification of C\(\#\) programs: a three-level approach

This page was built for publication: A Hoare calculus for verifying Java realizations of OCL-constrained design models

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