Proof of correctness of data representations
From MaRDI portal
Publication:2554952
DOI10.1007/BF00289507zbMath0244.68009WikidataQ56656274 ScholiaQ56656274MaRDI QIDQ2554952
Publication date: 1972
Published in: Acta Informatica (Search for Journal in Brave)
68N01: General topics in the theory of software
Related Items
Program specification and data refinement in type theory, Modular specification of frame properties in JML, Algebraic implementation of abstract data types: a survey of concepts and new compositionality results, Observational interpretation of Casl specifications, Computing with locally effective matrices, Refinement and state machine abstraction, Invariant diagrams with data refinement, Interface theories for concurrency and data, Prespecification in data refinement, Blaming the client: on data refinement in the presence of pointers, Abstraction for concurrent objects, Algebraic proofs of consistency and completeness, On the correctness of modular systems, A single complete rule for data refinement, A theory of software product line refinement, A formal abstract framework for modelling and testing complex software systems, Components as coalgebras: the refinement dimension, An analysis of refinement in an abortive paradigm, Observational purity and encapsulation, Do-it-yourself type theory, Semantical analysis of specification logic, Verifying atomic data types, Derivation of efficient parallel programs: An example from genetic sequence analysis, A mechanical analysis of program verification strategies, A view of computability on term algebras, Non-deterministic data types: Models and implementations, Pushdown machines for the macro tree transducer, Crypt-equivalent algebraic specifications, Proving entailment between conceptual state specifications, Algebraic specifications of computable and semicomputable data types, Equational specification of partial higher-order algebras, Semantics and verification of monitors and systems of monitors and processes, Auxiliary variables in data refinement, Correctness proofs for abstract implementations, Final algebra semantics and data type extensions, An approach for data type specification and its use in program verification, Hierarchical program specification and verification - a many-sorted logical approach, Invariants in the application-oriented specification of control systems, Specifications, models, and implementations of data abstractions, Data refinement of predicate transformers, Iterated stack automata and complexity classes, Language design methods based on semantic principles, On a new approach to representation independent data classes, Proving programs correct through refinement, The correctness of the Schorr-Waite list marking algorithm, Program refinement in fair transition systems, The lattice of data refinement, Software perfective maintenance: Including retrainable software in software reuse, Essential concepts of algebraic specification and program development, Proof systems for structured specifications with observability operators, Swinging types=functions+relations+transition systems, A hidden agenda, The verification and synthesis of data structures, Objects and classes in Algol-like languages, Secure implementation of channel abstractions, Observational logic, constructor-based logic, and their duality., Applying abstraction and formal specification in numerical software design, Data refinement, call by value and higher order programs, Lax naturality through enrichment, Stepwise refinement of heap-manipulating code in Chalice, Calculating with acyclic and cyclic lists, Abstract implementation of algebraic specifications in a temporal logic language, Constructor-based observational logic, Preservation of probabilistic information flow under refinement, On assertion-based encapsulation for object invariants and simulations, Specification and verification challenges for sequential object-oriented programs, A Coalgebraic Semantics of Subtyping, Building a Modal Interface Theory for Concurrency and Data, Transitive Separation Logic, Partiality, State and Dependent Types, Dynamic Frames in Java Dynamic Logic, Factorising folds for faster functions, WP Semantics and Behavioral Subtyping, An Introduction to Grammar Convergence, The worker/wrapper transformation, Iterated linear control and iterated one-turn pushdowns, On the design and specification of message oriented programs, Recursive data structures
Uses Software
Cites Work
