Observational Refinement Process

DOI10.1016/j.entcs.2008.06.006zbMath1283.68220OpenAlexW2031740403MaRDI QIDQ5403465

Alexandre Madeira

Publication date: 26 March 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.06.006

zbMATH Keywords

algebraic specificationobservational refinementobservational equalityrefinement via translation

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items

Refinement by Interpretation in a General Setting

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Foundations of algebraic specification and formal software development.
• Behavioural theories and the proof of behavioural properties
• Essential concepts of algebraic specification and program development
• Algebraic semantics for deductive systems
• Swinging types=functions+relations+transition systems
• A hidden agenda
• Observational proofs by rewriting.
• Observational logic, constructor-based logic, and their duality.
• Closure properties for the class of behavioral models
• Algebraizable logics
• Hidden coinduction: behavioural correctness proofs for objects
• Institutions: abstract model theory for specification and programming
• Behavioural reasoning for conditional equations
• Proving Behavioral Refinements of COL-specifications
• Conservative translations