Proof of correctness of data representations

DOI10.1007/BF00289507zbMATH Open0244.68009OpenAlexW3023216518WikidataQ56656274 ScholiaQ56656274MaRDI QIDQ2554952FDOQ2554952

Authors: Tony Hoare 

Publication date: 1972

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00289507

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Cites Work

• An axiomatic basis for computer programming
• Program development by stepwise refinement
• Title not available (Why is that?)
• A constructive approach to the problem of program correctness

Cited In (only showing first 100 items - show all)

• Object-oriented programming: some history, and challenges for the next fifty years
• Final algebra semantics and data type extensions
• Essential concepts of algebraic specification and program development
• Program specification and data refinement in type theory
• Specifications, models, and implementations of data abstractions
• Crypt-equivalent algebraic specifications
• Proving the correctness of behavioural implementations
• Do-it-yourself type theory
• Equational specification of partial higher-order algebras
• Automatic functional correctness proofs for functional search trees
• Interface theories for concurrency and data
• Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
• Semantical analysis of specification logic
• Semantics and verification of monitors and systems of monitors and processes
• A formal abstract framework for modelling and testing complex software systems
• A theory of software product line refinement
• Correctness proofs for abstract implementations
• Blaming the client: on data refinement in the presence of pointers
• Invariant diagrams with data refinement
• Algebraic specifications of computable and semicomputable data types
• Objects and classes in Algol-like languages
• An approach for data type specification and its use in program verification
• Algebraic implementation of abstract data types: a survey of concepts and new compositionality results
• Recursive data structures
• Observational interpretation of Casl specifications
• Observational purity and encapsulation
• Non-deterministic data types: Models and implementations
• Pushdown machines for the macro tree transducer
• Auxiliary variables in data refinement
• A coalgebraic semantics of subtyping
• Secure implementation of channel abstractions
• An analysis of refinement in an abortive paradigm
• Iterated stack automata and complexity classes
• Abstraction for concurrent objects
• Calculating with acyclic and cyclic lists
• Formal communication elimination and sequentialization equivalence proofs for distributed system models
• Dynamic logic with binders and its application to the development of reactive systems
• Constructor-based observational logic
• Data refinement of predicate transformers
• Retrenchment and refinement interworking: the tower theorems
• Syntactic logical relations for polymorphic and recursive types
• A hidden agenda
• Swinging types=functions+relations+transition systems
• Proof systems for structured specifications with observability operators
• Certifying algorithms
• Verifying atomic data types
• Hierarchical program specification and verification - a many-sorted logical approach
• Iterated linear control and iterated one-turn pushdowns
• Derivation of efficient parallel programs: An example from genetic sequence analysis
• The lattice of data refinement
• Specification and verification challenges for sequential object-oriented programs
• A mechanical analysis of program verification strategies
• A logic for the stepwise development of reactive systems
• Preservation of probabilistic information flow under refinement
• On assertion-based encapsulation for object invariants and simulations
• Transitive Separation Logic
• Components as coalgebras: the refinement dimension
• Behavioural satisfaction and equivalence in concrete model categories
• Prespecification in data refinement
• A view of computability on term algebras
• Data refinement of invariant based programs
• Proving entailment between conceptual state specifications
• A single complete rule for data refinement
• Modular specification of frame properties in JML
• Algebraic proofs of consistency and completeness
• On the correctness of modular systems
• WP semantics and behavioral subtyping
• Strict linearizability and abstract atomicity
• Building a Modal Interface Theory for Concurrency and Data
• The worker/wrapper transformation
• The refinement calculus of reactive systems
• Observational logic, constructor-based logic, and their duality.
• Interfaces between languages for communicating systems
• Approximation of weighted automata with storage
• Data refinement, call by value and higher order programs
• The verification and synthesis of data structures
• Extended transitive separation logic
• Refinement and state machine abstraction
• Dynamic frames in Java dynamic logic
• Applying abstraction and formal specification in numerical software design
• Loop invariants: analysis, classification, and examples
• On the design and specification of message oriented programs
• Sound and relaxed behavioural inheritance
• The correctness of the Schorr-Waite list marking algorithm
• Types in programming languages, between modelling, abstraction, and correctness (extended abstract)
• Invariants in the application-oriented specification of control systems
• Proving programs correct through refinement
• Lax naturality through enrichment
• Partiality, state and dependent types
• Program refinement in fair transition systems
• Software perfective maintenance: Including retrainable software in software reuse
• Abstract implementation of algebraic specifications in a temporal logic language
• Axiomatics for data refinement in call by value programming languages
• Category theoretic models of data refinement
• Constructing systems as object communities
• A technique for specifying and refining TCSP processes by using guards and liveness conditions
• Stepwise refinement of heap-manipulating code in Chalice
• Invariants for non-hierarchical object structures
• Principal abstract families of weighted tree languages
• Automatic refinement to efficient data structures: a comparison of two approaches

Uses Software

• Simula 67

This page was built for publication: Proof of correctness of data representations

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