A sufficient completeness reasoning tool for partial specifications

Joe Hendrix, Manuel Clavel, Jose Meseguer

Research output: Contribution to journalConference article

Abstract

We present the Maude sufficient completeness tool, which explicitly supports sufficient completeness reasoning for partial conditional specifications having sorts and subsorts and with domains of functions defined by conditional memberships. Our tool consists of two main components: (i) a sufficient completeness analyzer that generates a set of proof obligations which if discharged, ensures sufficient completeness; and (ii) Maude's inductive theorem prover (ITP) that is used as a back-end to try to automatically discharge those proof obligations.

Original languageEnglish (US)
Pages (from-to)165-174
Number of pages10
JournalLecture Notes in Computer Science
Volume3467
StatePublished - Sep 26 2005
Event16th International Conference on Term Rewriting and Applications, RTA 2005 - Nara, Japan
Duration: Apr 19 2005Apr 21 2005

Fingerprint

Completeness
Reasoning
Specification
Sufficient
Specifications
Partial
Maude
Sort
Theorem

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

A sufficient completeness reasoning tool for partial specifications. / Hendrix, Joe; Clavel, Manuel; Meseguer, Jose.

In: Lecture Notes in Computer Science, Vol. 3467, 26.09.2005, p. 165-174.

Research output: Contribution to journalConference article

@article{63869c87186f4395804b41bdad602808,
title = "A sufficient completeness reasoning tool for partial specifications",
abstract = "We present the Maude sufficient completeness tool, which explicitly supports sufficient completeness reasoning for partial conditional specifications having sorts and subsorts and with domains of functions defined by conditional memberships. Our tool consists of two main components: (i) a sufficient completeness analyzer that generates a set of proof obligations which if discharged, ensures sufficient completeness; and (ii) Maude's inductive theorem prover (ITP) that is used as a back-end to try to automatically discharge those proof obligations.",
author = "Joe Hendrix and Manuel Clavel and Jose Meseguer",
year = "2005",
month = "9",
day = "26",
language = "English (US)",
volume = "3467",
pages = "165--174",
journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - A sufficient completeness reasoning tool for partial specifications

AU - Hendrix, Joe

AU - Clavel, Manuel

AU - Meseguer, Jose

PY - 2005/9/26

Y1 - 2005/9/26

N2 - We present the Maude sufficient completeness tool, which explicitly supports sufficient completeness reasoning for partial conditional specifications having sorts and subsorts and with domains of functions defined by conditional memberships. Our tool consists of two main components: (i) a sufficient completeness analyzer that generates a set of proof obligations which if discharged, ensures sufficient completeness; and (ii) Maude's inductive theorem prover (ITP) that is used as a back-end to try to automatically discharge those proof obligations.

AB - We present the Maude sufficient completeness tool, which explicitly supports sufficient completeness reasoning for partial conditional specifications having sorts and subsorts and with domains of functions defined by conditional memberships. Our tool consists of two main components: (i) a sufficient completeness analyzer that generates a set of proof obligations which if discharged, ensures sufficient completeness; and (ii) Maude's inductive theorem prover (ITP) that is used as a back-end to try to automatically discharge those proof obligations.

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

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

M3 - Conference article

AN - SCOPUS:24944563138

VL - 3467

SP - 165

EP - 174

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

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

SN - 0302-9743

ER -