TY - GEN

T1 - Conditional specifications with inequational assumptions

AU - Mohan, Chilukuri K

AU - Srivas, Mandayam K.

PY - 1988/1/1

Y1 - 1988/1/1

N2 - Equational-Inequational Conditional Term Rewriting Systems (EI-CTRS) are a natural formalism for expressing data type and function specifications. EI-CTRS are sets of oriented conditional equations (rules) (eg.a=b Λ c ≠ d ::lhs → rhs), whose antecedents are conjunctions of equations and inequations. The EI-CTRS formalism extends existing equational languages such as OBJ2, by allowing within the rules the direct use of the = (or ≠) relation being defined. Using = and ≠ in rules clearly enhances the expressive power of the formalism, but it poses termination and semantic problems in executing a specification. We define a conditional rewriting mechanism, called EI-rewriting, which assumes two terms to be equal if they can be rewritten to a common term and inequal otherwise. We show that ground EI-rewriting is sound and complete, and can hence be used to correctly execute specifications expressed as EI-CTRS which satisfy a sufficient completeness-like property We give syntactic conditions and procedures to check that a specification in the formalism denotes a well-defined total function. We illustrate that useful and meaningful specifications can be constructed using EI-CTRS.

AB - Equational-Inequational Conditional Term Rewriting Systems (EI-CTRS) are a natural formalism for expressing data type and function specifications. EI-CTRS are sets of oriented conditional equations (rules) (eg.a=b Λ c ≠ d ::lhs → rhs), whose antecedents are conjunctions of equations and inequations. The EI-CTRS formalism extends existing equational languages such as OBJ2, by allowing within the rules the direct use of the = (or ≠) relation being defined. Using = and ≠ in rules clearly enhances the expressive power of the formalism, but it poses termination and semantic problems in executing a specification. We define a conditional rewriting mechanism, called EI-rewriting, which assumes two terms to be equal if they can be rewritten to a common term and inequal otherwise. We show that ground EI-rewriting is sound and complete, and can hence be used to correctly execute specifications expressed as EI-CTRS which satisfy a sufficient completeness-like property We give syntactic conditions and procedures to check that a specification in the formalism denotes a well-defined total function. We illustrate that useful and meaningful specifications can be constructed using EI-CTRS.

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

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

U2 - 10.1007/3-540-19242-5_13

DO - 10.1007/3-540-19242-5_13

M3 - Conference contribution

AN - SCOPUS:85034851261

SN - 9783540192428

VL - 308 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 161

EP - 178

BT - Conditional Term Rewriting Systems - 1st International Workshop, Proceedings

PB - Springer Verlag

T2 - 1st International Workshop on Conditional Term Rewriting Systems, 1987

Y2 - 8 July 1987 through 10 July 1987

ER -