A semi-algorithm for algebraic implementation proofs

DOI10.1016/0304-3975(92)90166-DzbMath0758.68048MaRDI QIDQ1199928

Rolf Hennicker

Publication date: 17 January 1993

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

zbMATH Keywords

algebraic specificationbehavioural implementationcontext inductionimplementation proofrecursive semi-algorithm

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Uses Software

• LARCH
• NQTHM

Cites Work

• Observational implementation of algebraic specifications
• Algebraic implementations preserve program correctness
• Algebraic implementation of abstract data types
• Context induction: A proof principle for behavioural abstractions and algebraic implementations
• On the algebraic definition of programming languages
• An overview of LP, the Larch Prover
• Proving Properties of Programs by Structural Induction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A semi-algorithm for algebraic implementation proofs