On Describing Terminating Algebraic Specifications Based on Their Models.

Saved in:

Bibliographic Details
Title:	On Describing Terminating Algebraic Specifications Based on Their Models.
Authors:	Nakamura, Masaki¹, Ogata, Kazuhiro², Futatsugi, Kokichi²
Source:	Proceedings of the International MultiConference of Engineers & Computer Scientists 2012 Volume I. 2012, Vol. 1, p192-197. 6p.
Subjects:	Rewriting systems (Computer science), Algebra, Machine theory, Technical specifications, Computer software termination
Abstract:	OBJ algebraic specification languages support automated equational reasoning based on term rewriting systems (TRSs) for specification verification. Termination is one of the most important properties of TRSs. Terminating TRSs guarantee that any equational reasoning terminates in finite times. Although termination is an undecidable property, several sufficient conditions have been proposed, and several termination provers have been developed. In this study, we focus on a way to describe terminating algebraic specifications, that is, the coresponding TRSs are terminating. Existing termination provers may inform us whether a given specification is terminating or not. However, they do not give a guideline to describe terminating specifications. We propose a model-based method for describing terminating specifications. In our method, a model of a given specification can be used for proving its termination. Since specifiers are describing a specification while thinking its model in their mind, our model-based termination methods are suitable for algebraic specifications. [ABSTRACT FROM AUTHOR]
	Copyright of Proceedings of the International MultiConference of Engineers & Computer Scientists 2012 Volume I is the property of International Association of Engineers (IAENG) and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database:	Engineering Source

Description
Abstract:	OBJ algebraic specification languages support automated equational reasoning based on term rewriting systems (TRSs) for specification verification. Termination is one of the most important properties of TRSs. Terminating TRSs guarantee that any equational reasoning terminates in finite times. Although termination is an undecidable property, several sufficient conditions have been proposed, and several termination provers have been developed. In this study, we focus on a way to describe terminating algebraic specifications, that is, the coresponding TRSs are terminating. Existing termination provers may inform us whether a given specification is terminating or not. However, they do not give a guideline to describe terminating specifications. We propose a model-based method for describing terminating specifications. In our method, a model of a given specification can be used for proving its termination. Since specifiers are describing a specification while thinking its model in their mind, our model-based termination methods are suitable for algebraic specifications. [ABSTRACT FROM AUTHOR]
ISBN:	9789881925114