Proving sufficient completeness of constructor-based algebraic specifications

Masaki Nakamura, Daniel Gaina, Kazuhiro Ogata, Kokichi Futatsugi

Research output: Contribution to journalArticle

Abstract

OBJ algebraic specification languages, for example, OBJ3, CafeOBJ and Maude, are formal specification languages which support several sophisticated functions to describe and verify large and complex specifications. Recently, the proof score method, which is an interactive formal verification method for OBJ languages, based on constructor-based algebras has been developed and several practical case studies have been reported. Sufficient completeness is one of the most important properties of constructor-based specifications, which guarantees the existence of initial models. In this study, we give a sufficient condition for sufficient completeness of constructor-based specifications based on the theory of term rewriting.

Original languageEnglish
Pages (from-to)15-21
Number of pages7
JournalLecture Notes in Electrical Engineering
Volume373
DOIs
Publication statusPublished - Jan 1 2015
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Industrial and Manufacturing Engineering

Fingerprint Dive into the research topics of 'Proving sufficient completeness of constructor-based algebraic specifications'. Together they form a unique fingerprint.

  • Cite this