Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
From hidden to visible
Zhang M., Ogata K. Theoretical Computer Science722 (C):52-75,2018.Type:Article
Date Reviewed: Oct 12 2018

Algebraic specification is a technique in which a system is modeled by equations or conditional equations. This approach was originally used for defining data types and operations on them. An added benefit is that the equational systems can be reinterpreted as rewrite rules and hence be executed, under certain conditions.

Behavioral specifications have the same background but strive to be more abstract. This is achieved by dividing the operations into a hidden and an observable part, where equations on the observable part specify which terms of the hidden part are to be considered indistinguishable (that is, behaviorally equal).

Reasoning about nonbehavioral specifications is facilitated by a plethora of theorem provers and model checkers, but reasoning over behavioral specifications is difficult. Since the basic language is the same (only the semantics differ), it seems possible to transform one kind of specification into the other, and several approaches have been proposed. This paper presents a unified transformational approach that encompasses several previously proposed approaches.

The first two sections discuss the basics of the two algebraic specification techniques, and the third section explains the basic idea of the transformation, which is based on a subclass of behavioral theories. These 0-1 bounded behavioral transformations intuitively restrict the number of values changed in a transition to at most one. The following section explains why existing transformational approaches are subsumed by the presented approach. A transformation from one framework into another framework is only sensible if certain properties of interest are preserved by the transformation. Therefore, in the fifth section it is proved that linear time properties of the original theory are preserved in the resulting theory. The paper closes with a discussion of related work and a conclusion, followed by an appendix with some proof details.

The paper is self-contained, well written, and supported by examples. Some open questions remain, namely to find good transformations from general behavioral specifications to 0-1 bounded behavioral specifications. A simple approach of transformation to rewrite rules cannot be efficiently model checked. This is to be addressed in future work.

Reviewer:  Markus Wolf Review #: CR146277 (1812-0643)
Bookmark and Share
 
General (F.0 )
 
 
Algebraic Approaches To Semantics (F.3.2 ... )
 
 
Specification Techniques (F.3.1 ... )
 
 
Formal Definitions And Theory (D.3.1 )
 
 
General (D.2.0 )
 
 
Software/ Program Verification (D.2.4 )
 
Would you recommend this review?
yes
no
Other reviews under "General": Date
Introduction to computer theory (revised ed.)
Cohen D., John Wiley & Sons, Inc., New York, NY, 1991. Type: Book (9780471510109)
Feb 1 1993
Introduction to computer theory
Cohen D., John Wiley & Sons, Inc., New York, NY, 1986. Type: Book (9789780471802716)
Feb 1 1987
Theory of computation: formal languages, automata, and complexity
Brookshear J., Benjamin-Cummings Publ. Co., Inc., Redwood City, CA, 1989. Type: Book (9789780805301434)
Jan 1 1990
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy