Conditional specifications with inequational assumptions

Chilukuri K Mohan, Mandayam K. Srivas

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationConditional Term Rewriting Systems - 1st International Workshop, Proceedings
PublisherSpringer Verlag
Pages161-178
Number of pages18
Volume308 LNCS
ISBN (Print)9783540192428
DOIs
StatePublished - Jan 1 1988
Externally publishedYes
Event1st International Workshop on Conditional Term Rewriting Systems, 1987 - Orsay, France
Duration: Jul 8 1987Jul 10 1987

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume308 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other1st International Workshop on Conditional Term Rewriting Systems, 1987
CountryFrance
CityOrsay
Period7/8/877/10/87

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Conditional specifications with inequational assumptions'. Together they form a unique fingerprint.

Cite this