Proving sufficient completeness of constructor-based algebraic specifications

Masaki Nakamura, Daniel Mircea 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

Fingerprint

Specification languages
Specifications
Algebra
Formal verification
Formal specification

All Science Journal Classification (ASJC) codes

  • Industrial and Manufacturing Engineering

Cite this

Proving sufficient completeness of constructor-based algebraic specifications. / Nakamura, Masaki; Gaina, Daniel Mircea; Ogata, Kazuhiro; Futatsugi, Kokichi.

In: Lecture Notes in Electrical Engineering, Vol. 373, 01.01.2015, p. 15-21.

Research output: Contribution to journalArticle

Nakamura, Masaki ; Gaina, Daniel Mircea ; Ogata, Kazuhiro ; Futatsugi, Kokichi. / Proving sufficient completeness of constructor-based algebraic specifications. In: Lecture Notes in Electrical Engineering. 2015 ; Vol. 373. pp. 15-21.
@article{c7b5c367dd6d46e9b2402f08f12734bb,
title = "Proving sufficient completeness of constructor-based algebraic specifications",
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.",
author = "Masaki Nakamura and Gaina, {Daniel Mircea} and Kazuhiro Ogata and Kokichi Futatsugi",
year = "2015",
month = "1",
day = "1",
doi = "10.1007/978-981-10-0281-6_3",
language = "English",
volume = "373",
pages = "15--21",
journal = "Lecture Notes in Electrical Engineering",
issn = "1876-1100",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Proving sufficient completeness of constructor-based algebraic specifications

AU - Nakamura, Masaki

AU - Gaina, Daniel Mircea

AU - Ogata, Kazuhiro

AU - Futatsugi, Kokichi

PY - 2015/1/1

Y1 - 2015/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84951276636&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84951276636&partnerID=8YFLogxK

U2 - 10.1007/978-981-10-0281-6_3

DO - 10.1007/978-981-10-0281-6_3

M3 - Article

VL - 373

SP - 15

EP - 21

JO - Lecture Notes in Electrical Engineering

JF - Lecture Notes in Electrical Engineering

SN - 1876-1100

ER -