Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs.

Saved in:

Bibliographic Details
Title:	Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs.
Authors:	Masaki Nakamura¹, Kazuhiro Ogata², Kokichi Futatsugi²
Source:	International MultiConference of Engineers & Computer Scientists 2013. 2013, Vol. 1, p1-6. 6p.
Subjects:	Rewriting systems (Computer science), Proof theory, Feature extraction, Programming languages, Object-oriented methods (Computer science), Computer software termination
Abstract:	OBJ algebraic specification languages support semi-automated verification of algebraic specifications based on equational reasoning by term rewriting systems (TRS). Termination is one of the most important properties of TRSs. Termination guarantees that any execution of the specification terminates in finite times. Another important feature of OBJ languages is a module system with module imports to describe large and complex specifications in a modular way. In this study, we focus on a way to prove termination of OBJ specifications incrementally, based on the notion of modular conditional dependency pairs (MCDP). [ABSTRACT FROM AUTHOR]
	Copyright of International MultiConference of Engineers & Computer Scientists 2013 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 semi-automated verification of algebraic specifications based on equational reasoning by term rewriting systems (TRS). Termination is one of the most important properties of TRSs. Termination guarantees that any execution of the specification terminates in finite times. Another important feature of OBJ languages is a module system with module imports to describe large and complex specifications in a modular way. In this study, we focus on a way to prove termination of OBJ specifications incrementally, based on the notion of modular conditional dependency pairs (MCDP). [ABSTRACT FROM AUTHOR]