A semi-algorithm for algebraic implementation proofs

DOI10.1016/0304-3975(92)90166-DMaRDI QIDQ1199928zbMATH OpenFDO

Authors Rolf Hennicker

Publication date 17 January 1993

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

Full work available at URL https://doi.org/10.1016/0304-3975(92)90166-D

zbMATH Keywords

algebraic specificationbehavioural implementationcontext inductionimplementation proofrecursive semi-algorithm

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• Proving the correctness of behavioural implementations
• Modular correctness proofs of behavioural implementations
• Observational implementation of algebraic specifications
• Observational implementations
• scientific article; zbMATH DE number 785047

Cites work

• Algebraic implementation of abstract data types
• Algebraic implementations preserve program correctness
• An overview of LP, the Larch Prover
• Context induction: A proof principle for behavioural abstractions and algebraic implementations
• scientific article; zbMATH DE number 3888893 (Why is no real title available?)
• scientific article; zbMATH DE number 3956411 (Why is no real title available?)
• scientific article; zbMATH DE number 4112064 (Why is no real title available?)
• scientific article; zbMATH DE number 3784848 (Why is no real title available?)
• scientific article; zbMATH DE number 4113952 (Why is no real title available?)
• Observational implementation of algebraic specifications
• On the algebraic definition of programming languages
• Proving Properties of Programs by Structural Induction

Cited in

(8)

• Context induction: A proof principle for behavioural abstractions and algebraic implementations
• scientific article; zbMATH DE number 8763 (Why is no real title available?)
• scientific article; zbMATH DE number 844104 (Why is no real title available?)
• Observational implementations
• scientific article; zbMATH DE number 6403889 (Why is no real title available?)
• Semialgebraic Proofs and Efficient Algorithm Design
• The Alf proof editor and its proof engine
• Observational implementation of algebraic specifications

Describes a project that uses

Uses Software

• LARCH
• NQTHM

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1199928)