Observational purity and encapsulation

DOI10.1016/J.TCS.2007.02.004MaRDI QIDQ882452zbMATH OpenOpenAlexFDO

Authors David A. Naumann

Publication date 23 May 2007

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2007.02.004

zbMATH Keywords

information hidingspecification and verificationbenevolent side effects

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Fundamental Approaches to Software Engineering
• Observational implementations
• A generic complete dynamic logic for reasoning about purity and effects
• Observational implementation of algebraic specifications
• Observational interpretation of Casl specifications

Cites work

• scientific article; zbMATH DE number 1728235 (Why is no real title available?)
• scientific article; zbMATH DE number 3943003 (Why is no real title available?)
• scientific article; zbMATH DE number 4050933 (Why is no real title available?)
• 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 2090153 (Why is no real title available?)
• An axiomatic basis for computer programming
• Data Refinement
• FM 2005: Formal Methods
• Fundamental Approaches to Software Engineering
• How the design of JML accommodates both runtime assertion checking and formal verification
• Modular specification and verification of object-oriented programs
• Ownership confinement ensures representation independence for object-oriented programs
• Ownership types for object encapsulation
• Program logic and equivalence in the presence of garbage collection.
• Proof of correctness of data representations
• Relational separation logic
• Representation independence, confinement and access control (extended abstract)
• Simple relational correctness proofs for static analyses and program transformations
• Stack-based access control and secure information flow
• Static Analysis
• Towards imperative modules: reasoning about invariants and sharing of mutable state

Cited in

(4)

• A generic complete dynamic logic for reasoning about purity and effects
• Observational interpretation of Casl specifications
• Checking observational purity of procedures
• Fundamental Approaches to Software Engineering

Describes a project that uses

Uses Software

• ESC/Java
• Spec#
• JML
• Eiffel

This page was built for publication: Observational purity and encapsulation

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