Proving termination of membership equational programs

Francisco Durán, Salvador Lucas, Jose Meseguer, Claude Marché, Xavier Urbain

Research output: Contribution to conferencePaper

Abstract

Advanced typing, matching, and evaluation strategy features, as well as very general conditional rules, are routinely used in equational programming languages such as, for example, ASF+SDF, OBJ, CAFEOBJ, MAUDE, and equational subsets of ELAN and CASL. Proving termination of equational programs having such expressive features is important but nontrivial, because some of those features may not be supported by standard termination methods and tools, such as MU-TERM, CiME, APROVE, TTT, TERMPTATION, etc. Yet, use of the features may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive equational programs and termination tools, prove the correctness of such transformations, and discuss a prototype tool performing the transformations on MAUDE equational programs and sending the resulting transformed theories to some of the aforementioned tools.

Original languageEnglish (US)
Pages147-158
Number of pages12
StatePublished - Jan 1 2004
EventProceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'04 - Verona, Italy
Duration: Aug 24 2004Aug 25 2004

Other

OtherProceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'04
CountryItaly
CityVerona
Period8/24/048/25/04

Fingerprint

Computer programming languages

Keywords

  • Membership Equational Logic
  • Program Transformation
  • Term Rewriting
  • Termination

ASJC Scopus subject areas

  • Software

Cite this

Durán, F., Lucas, S., Meseguer, J., Marché, C., & Urbain, X. (2004). Proving termination of membership equational programs. 147-158. Paper presented at Proceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'04, Verona, Italy.

Proving termination of membership equational programs. / Durán, Francisco; Lucas, Salvador; Meseguer, Jose; Marché, Claude; Urbain, Xavier.

2004. 147-158 Paper presented at Proceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'04, Verona, Italy.

Research output: Contribution to conferencePaper

Durán, F, Lucas, S, Meseguer, J, Marché, C & Urbain, X 2004, 'Proving termination of membership equational programs' Paper presented at Proceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'04, Verona, Italy, 8/24/04 - 8/25/04, pp. 147-158.
Durán F, Lucas S, Meseguer J, Marché C, Urbain X. Proving termination of membership equational programs. 2004. Paper presented at Proceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'04, Verona, Italy.
Durán, Francisco ; Lucas, Salvador ; Meseguer, Jose ; Marché, Claude ; Urbain, Xavier. / Proving termination of membership equational programs. Paper presented at Proceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'04, Verona, Italy.12 p.
@conference{0aed007545a142a4a6ff803b12cab274,
title = "Proving termination of membership equational programs",
abstract = "Advanced typing, matching, and evaluation strategy features, as well as very general conditional rules, are routinely used in equational programming languages such as, for example, ASF+SDF, OBJ, CAFEOBJ, MAUDE, and equational subsets of ELAN and CASL. Proving termination of equational programs having such expressive features is important but nontrivial, because some of those features may not be supported by standard termination methods and tools, such as MU-TERM, CiME, APROVE, TTT, TERMPTATION, etc. Yet, use of the features may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive equational programs and termination tools, prove the correctness of such transformations, and discuss a prototype tool performing the transformations on MAUDE equational programs and sending the resulting transformed theories to some of the aforementioned tools.",
keywords = "Membership Equational Logic, Program Transformation, Term Rewriting, Termination",
author = "Francisco Dur{\'a}n and Salvador Lucas and Jose Meseguer and Claude March{\'e} and Xavier Urbain",
year = "2004",
month = "1",
day = "1",
language = "English (US)",
pages = "147--158",
note = "Proceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'04 ; Conference date: 24-08-2004 Through 25-08-2004",

}

TY - CONF

T1 - Proving termination of membership equational programs

AU - Durán, Francisco

AU - Lucas, Salvador

AU - Meseguer, Jose

AU - Marché, Claude

AU - Urbain, Xavier

PY - 2004/1/1

Y1 - 2004/1/1

N2 - Advanced typing, matching, and evaluation strategy features, as well as very general conditional rules, are routinely used in equational programming languages such as, for example, ASF+SDF, OBJ, CAFEOBJ, MAUDE, and equational subsets of ELAN and CASL. Proving termination of equational programs having such expressive features is important but nontrivial, because some of those features may not be supported by standard termination methods and tools, such as MU-TERM, CiME, APROVE, TTT, TERMPTATION, etc. Yet, use of the features may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive equational programs and termination tools, prove the correctness of such transformations, and discuss a prototype tool performing the transformations on MAUDE equational programs and sending the resulting transformed theories to some of the aforementioned tools.

AB - Advanced typing, matching, and evaluation strategy features, as well as very general conditional rules, are routinely used in equational programming languages such as, for example, ASF+SDF, OBJ, CAFEOBJ, MAUDE, and equational subsets of ELAN and CASL. Proving termination of equational programs having such expressive features is important but nontrivial, because some of those features may not be supported by standard termination methods and tools, such as MU-TERM, CiME, APROVE, TTT, TERMPTATION, etc. Yet, use of the features may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive equational programs and termination tools, prove the correctness of such transformations, and discuss a prototype tool performing the transformations on MAUDE equational programs and sending the resulting transformed theories to some of the aforementioned tools.

KW - Membership Equational Logic

KW - Program Transformation

KW - Term Rewriting

KW - Termination

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

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

M3 - Paper

AN - SCOPUS:11244352574

SP - 147

EP - 158

ER -