Proof of correctness of data representations
From MaRDI portal
Publication:2554952
DOI10.1007/BF00289507zbMath0244.68009OpenAlexW3023216518WikidataQ56656274 ScholiaQ56656274MaRDI QIDQ2554952
Publication date: 1972
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00289507
Related Items
Computing with locally effective matrices, Retrenchment and refinement interworking: the tower theorems, Refinement and state machine abstraction, Interfaces between languages for communicating systems, Observational interpretation of Casl specifications, Strict Linearizability and Abstract Atomicity, Sound and Relaxed Behavioural Inheritance, Behavioural satisfaction and equivalence in concrete model categories, Components as coalgebras: the refinement dimension, Observational logic, constructor-based logic, and their duality., Software perfective maintenance: Including retrainable software in software reuse, Logical relations and parametricity -- a Reynolds programme for category theory and programming languages, Building a Modal Interface Theory for Concurrency and Data, A technique for specifying and refining TCSP processes by using guards and liveness conditions, Constructing systems as object communities, Constructor-based observational logic, Modular specification of frame properties in JML, Pushdown machines for the macro tree transducer, Crypt-equivalent algebraic specifications, Proving entailment between conceptual state specifications, Dynamic Logic with Binders and Its Application to the Development of Reactive Systems, Algebraic specifications of computable and semicomputable data types, An analysis of refinement in an abortive paradigm, Equational specification of partial higher-order algebras, Transitive Separation Logic, Program specification and data refinement in type theory, Types in Programming Languages, Between Modelling, Abstraction, and Correctness, On assertion-based encapsulation for object invariants and simulations, Specification and verification challenges for sequential object-oriented programs, Applying abstraction and formal specification in numerical software design, Data refinement, call by value and higher order programs, Semantics and verification of monitors and systems of monitors and processes, Auxiliary variables in data refinement, Correctness proofs for abstract implementations, Essential concepts of algebraic specification and program development, Lax naturality through enrichment, Blaming the client: on data refinement in the presence of pointers, Observational purity and encapsulation, Final algebra semantics and data type extensions, The refinement calculus of reactive systems, Proving the correctness of behavioural implementations, A decade of TAPSOFT, Object-oriented programming: some history, and challenges for the next fifty years, Abstraction for concurrent objects, Proof systems for structured specifications with observability operators, Automatic refinement to efficient data structures: a comparison of two approaches, An approach for data type specification and its use in program verification, Hierarchical program specification and verification - a many-sorted logical approach, Stepwise refinement of heap-manipulating code in Chalice, Iterated linear control and iterated one-turn pushdowns, Invariant diagrams with data refinement, Recursive data structures, Do-it-yourself type theory, Invariants in the application-oriented specification of control systems, Semantical analysis of specification logic, Verifying atomic data types, Specifications, models, and implementations of data abstractions, Unnamed Item, Derivation of efficient parallel programs: An example from genetic sequence analysis, Calculating with acyclic and cyclic lists, Algebraic implementation of abstract data types: a survey of concepts and new compositionality results, Certifying algorithms, Formal communication elimination and sequentialization equivalence proofs for distributed system models, A mechanical analysis of program verification strategies, Data Refinement of Invariant Based Programs, Data refinement of predicate transformers, Iterated stack automata and complexity classes, Algebraic proofs of consistency and completeness, Partiality, State and Dependent Types, On the correctness of modular systems, A Coalgebraic Semantics of Subtyping, A single complete rule for data refinement, Preservation of probabilistic information flow under refinement, Loop invariants, Interface theories for concurrency and data, Language design methods based on semantic principles, A theory of software product line refinement, A formal abstract framework for modelling and testing complex software systems, Prespecification in data refinement, On a new approach to representation independent data classes, Abstract implementation of algebraic specifications in a temporal logic language, An Introduction to Grammar Convergence, A logic for the stepwise development of reactive systems, Proving programs correct through refinement, Dynamic Frames in Java Dynamic Logic, The correctness of the Schorr-Waite list marking algorithm, The worker/wrapper transformation, Factorising folds for faster functions, On the design and specification of message oriented programs, Principal abstract families of weighted tree languages, Category Theoretic Models of Data Refinement, Axiomatics for Data Refinement in Call by Value Programming Languages, Automatic Functional Correctness Proofs for Functional Search Trees, WP Semantics and Behavioral Subtyping, Swinging types=functions+relations+transition systems, A hidden agenda, The verification and synthesis of data structures, A view of computability on term algebras, Non-deterministic data types: Models and implementations, Objects and classes in Algol-like languages, Secure implementation of channel abstractions, Syntactic Logical Relations for Polymorphic and Recursive Types, Extended transitive separation logic, A Framework for Establishing Formal Conformance between Object Models and Object-Oriented Programs, Invariants for Non-Hierarchical Object Structures, Work it, wrap it, fix it, fold it, Program refinement in fair transition systems, The lattice of data refinement
Uses Software
Cites Work
