Observational purity and encapsulation
type: Item
instance of: scholarly article
title: Observational purity and encapsulation
zbMATH Open document ID: 1116.68052
author: David A. Naumann
published in: Theoretical Computer Science
publication date: 2007-05-23T00:00:00Z
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 5156656
zbMATH Keywords: specification and verification
zbMATH Keywords: information hiding
zbMATH Keywords: benevolent side effects
describes a project that uses: Spec#
describes a project that uses: JML
describes a project that uses: ESC/Java
describes a project that uses: Eiffel
MaRDI profile type: Publication
full work available at URL: j.tcs.2007.02.004
OpenAlex ID: W2101530705
cites work: Representation independence, confinement and access control [extended abstract]
cites work: Ownership confinement ensures representation independence for object-oriented programs
cites work: Stack-based access control and secure information flow
cites work: Simple relational correctness proofs for static analyses and program transformations
cites work: Ownership types for object encapsulation
cites work: Program logic and equivalence in the presence of garbage collection.
cites work: Q4808846
cites work: Q2779232
cites work: Data Refinement
cites work: Q4282672
cites work: Q3713577
cites work: An axiomatic basis for computer programming
cites work: Proof of correctness of data representations
cites work: How the design of JML accommodates both runtime assertion checking and formal verification
cites work: Q3787422
cites work: Q4371400
cites work: Modular specification and verification of object-oriented programs
cites work: Fundamental Approaches to Software Engineering
cites work: Towards imperative modules: reasoning about invariants and sharing of mutable state
cites work: FM 2005: Formal Methods
cites work: Static Analysis
cites work: Relational separation logic
DOI: 10.1016/J.TCS.2007.02.004
description: scientific article; zbMATH DE number 5156656