Modular specification of frame properties in JML

DOI10.1002/CPE.713MaRDI QIDQ4794726zbMATH OpenOpenAlexFDO

Authors Peter Müller, Arnd Poetzsch-Heffter, Gary T. Leavens

Publication date 20 February 2003

Published in Concurrency and Computation: Practice and Experience (Search for Journal in Brave)

Full work available at URL https://lib.dr.iastate.edu/cgi/viewcontent.cgi?article=1336&context=cs_techreports

zbMATH Keywords

frame problemJavaownershipformal specificationJMLalias controldepends-clausemodifies-clause

Mathematics Subject Classification ID

Theory of programming languages (68N15) Computing methodologies and applications (68U99)

Recommendations

• Modular specification and verification of object-oriented programs
• Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
• Modular specification and verification of object-oriented programs
• scientific article; zbMATH DE number 1693527
• scientific article; zbMATH DE number 177256

Cites work

• scientific article; zbMATH DE number 517385 (Why is no real title available?)
• scientific article; zbMATH DE number 1105469 (Why is no real title available?)
• scientific article; zbMATH DE number 1107134 (Why is no real title available?)
• Proof of correctness of data representations
• Writing Larch interface language specifications

Cited in

(9)

• Programming Languages and Systems
• The dynamic frames theory
• An attribute-grammar framework for specifying the accessibility in Java programs
• MRI: modular reasoning about interference in incremental programming
• A logic for secure memory access of abstract state machines
• Verifying pointer safety for programs with unknown calls
• A logical analysis of aliasing in imperative higher-order functions
• Specification and verification challenges for sequential object-oriented programs
• Modular specification and verification of object-oriented programs

Describes a project that uses

Uses Software

• JML
• Eiffel
• LARCH

This page was built for publication: Modular specification of frame properties in JML

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