Soundness in verification of algebraic specifications with OBJ

DOI10.1016/J.JLAP.2007.07.002MaRDI QIDQ2469155zbMATH OpenOpenAlexFDO

Authors K. O. Wilander

Publication date 4 February 2008

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlap.2007.07.002

zbMATH Keywords

algebraic specificationbehavioural specificationOBJsoundnessverification

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
• CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
• scientific article; zbMATH DE number 2172803
• On Equality Predicates in Algebraic Specification Languages
• From OBJ to Maude and Beyond

Cites work

• CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
• scientific article; zbMATH DE number 3703962 (Why is no real title available?)
• scientific article; zbMATH DE number 3714891 (Why is no real title available?)
• Proving and rewriting

Cited in

(3)

• On Equality Predicates in Algebraic Specification Languages
• Soundness and completeness of a synthesis algorithm based on example computations
• Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications

Describes a project that uses

Uses Software

• CafeOBJ

This page was built for publication: Soundness in verification of algebraic specifications with OBJ

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