A total approach to partial algebraic specification

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

Abstract

Partiality is a fact of life, but at present explicitly partial algebraic specifications lack tools and have limited proof methods. We propose a sound and complete way to support execution and formal reasoning of explicitly partial algebraic specifications within the total framework of membership equational logic (MEL) which has a highperformance interpreter (Maude) and proving tools. This is accomplished by a sound and complete mapping PMEL → MEL of partial membership equational (PMEL) theories into total ones. Furthermore, we characterize and give proof methods for a practical class of theories for which this mapping has "almost-zero representational distance," in that the partial theory and its total translation are identical up to minor syntactic sugar conventions. This then supports very direct execution of, and formal reasoningabout, partial theories at the total level. In conjunction with tools like Maude and its proving tools, our methods can be used to execute and reason about partial specifications such as those in CASL.

Original languageEnglish (US)
Title of host publicationAutomata, Languages and Programming - 29th International Colloquium, ICALP 2002, Proceedings
Pages572-584
Number of pages13
StatePublished - 2002
Event29th International Colloquium on Automata, Languages, and Programming, ICALP 2002 - Malaga, Spain
Duration: Jul 8 2002Jul 13 2002

Publication series

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

Other

Other29th International Colloquium on Automata, Languages, and Programming, ICALP 2002
Country/TerritorySpain
CityMalaga
Period7/8/027/13/02

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'A total approach to partial algebraic specification'. Together they form a unique fingerprint.

Cite this