Context induction: A proof principle for behavioural abstractions and algebraic implementations

DOI10.1007/BF01642507zbMath0739.68060MaRDI QIDQ1179807

Rolf Hennicker

Publication date: 27 June 1992

Published in: Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

behavioural specificationbehavioural implementationbehavioural theoremFRI implementation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items (17)

Circular Coinduction: A Proof Theoretical Foundation ⋮ A general framework for modular implementations of modular system specifications ⋮ Constructor-based observational logic ⋮ Behavioural approaches to algebraic specifications. A comparative study ⋮ Proof systems for structured specifications with observability operators ⋮ Complete sets of cooperations ⋮ Observational interpretations of hybrid dynamic logic with binders and silent transitions ⋮ Behavioural theories and the proof of behavioural properties ⋮ On behavioural abstraction and behavioural satisfaction in higher-order logic ⋮ Observational specifications and the indistinguishability assumption ⋮ A semi-algorithm for algebraic implementation proofs ⋮ Behavioral abstraction is hiding information ⋮ Behavioural and abstractor specifications revisited ⋮ Towards Behavioral Maude ⋮ Regular Strategies as Proof Tactics for CIRC ⋮ Observational proofs by rewriting. ⋮ On the complexity of stream equality

Uses Software

• NQTHM

Cites Work

• A systematic study of models of abstract data types
• Observational implementation of algebraic specifications
• Algebraic implementations preserve program correctness
• Final algebra semantics and data type extensions
• Algebraic implementation of abstract data types
• Abstrakte Datentypen: Die algebraische Spezifikation von Rechenstrukturen
• Final Data Types and Their Specification
• Proving Properties of Programs by Structural Induction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Context induction: A proof principle for behavioural abstractions and algebraic implementations