Modular specification of frame properties in JML

DOI10.1002/cpe.713zbMath1005.68583OpenAlexW2101928793MaRDI QIDQ4794726

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

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

Javaformal specificationframe problemownershipJMLalias controldepends-clausemodifies-clause

Mathematics Subject Classification ID

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

Related Items

MRI: Modular reasoning about interference in incremental programming ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Verifying pointer safety for programs with unknown calls ⋮ The dynamic frames theory ⋮ A logic for secure memory access of abstract state machines ⋮ A logical analysis of aliasing in imperative higher-order functions

Uses Software

• LARCH
• Eiffel
• JML

Cites Work

• Proof of correctness of data representations
• Writing Larch interface language specifications
• Unnamed Item
• Unnamed Item
• Unnamed Item