TY - JOUR
T1 - Proving sufficient completeness of constructor-based algebraic specifications
AU - Nakamura, Masaki
AU - Gaina, Daniel
AU - Ogata, Kazuhiro
AU - Futatsugi, Kokichi
N1 - Publisher Copyright:
© Springer Science+Business Media Singapore 2015.
Copyright:
Copyright 2015 Elsevier B.V., All rights reserved.
PY - 2015
Y1 - 2015
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
AN - SCOPUS:84951276636
SN - 1876-1100
VL - 373
SP - 15
EP - 21
JO - Lecture Notes in Electrical Engineering
JF - Lecture Notes in Electrical Engineering
ER -