View in EDS PDF Full Text

On Describing Terminating Algebraic Specifications Based on Their Models.

Saved in:
Bibliographic Details
Title: On Describing Terminating Algebraic Specifications Based on Their Models.
Authors: Nakamura, Masaki1, Ogata, Kazuhiro2, Futatsugi, Kokichi2
Source: Proceedings of the International MultiConference of Engineers & Computer Scientists 2012 Volume I. 2012, Vol. 1, p192-197. 6p.
Subjects: Rewriting systems (Computer science), Algebra, Machine theory, Technical specifications, Computer software termination
Abstract: OBJ algebraic specification languages support automated equational reasoning based on term rewriting systems (TRSs) for specification verification. Termination is one of the most important properties of TRSs. Terminating TRSs guarantee that any equational reasoning terminates in finite times. Although termination is an undecidable property, several sufficient conditions have been proposed, and several termination provers have been developed. In this study, we focus on a way to describe terminating algebraic specifications, that is, the coresponding TRSs are terminating. Existing termination provers may inform us whether a given specification is terminating or not. However, they do not give a guideline to describe terminating specifications. We propose a model-based method for describing terminating specifications. In our method, a model of a given specification can be used for proving its termination. Since specifiers are describing a specification while thinking its model in their mind, our model-based termination methods are suitable for algebraic specifications. [ABSTRACT FROM AUTHOR]
Copyright of Proceedings of the International MultiConference of Engineers & Computer Scientists 2012 Volume I is the property of International Association of Engineers (IAENG) and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 82785061
AccessLevel: 6
PubType: Conference
PubTypeId: conference
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: On Describing Terminating Algebraic Specifications Based on Their Models.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Nakamura%2C+Masaki%22">Nakamura, Masaki</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Ogata%2C+Kazuhiro%22">Ogata, Kazuhiro</searchLink><relatesTo>2</relatesTo><br /><searchLink fieldCode="AR" term="%22Futatsugi%2C+Kokichi%22">Futatsugi, Kokichi</searchLink><relatesTo>2</relatesTo>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Proceedings+of+the+International+MultiConference+of+Engineers+%26+Computer+Scientists+2012+Volume+I%22">Proceedings of the International MultiConference of Engineers & Computer Scientists 2012 Volume I</searchLink>. 2012, Vol. 1, p192-197. 6p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Rewriting+systems+%28Computer+science%29%22">Rewriting systems (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Algebra%22">Algebra</searchLink><br /><searchLink fieldCode="DE" term="%22Machine+theory%22">Machine theory</searchLink><br /><searchLink fieldCode="DE" term="%22Technical+specifications%22">Technical specifications</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+termination%22">Computer software termination</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: OBJ algebraic specification languages support automated equational reasoning based on term rewriting systems (TRSs) for specification verification. Termination is one of the most important properties of TRSs. Terminating TRSs guarantee that any equational reasoning terminates in finite times. Although termination is an undecidable property, several sufficient conditions have been proposed, and several termination provers have been developed. In this study, we focus on a way to describe terminating algebraic specifications, that is, the coresponding TRSs are terminating. Existing termination provers may inform us whether a given specification is terminating or not. However, they do not give a guideline to describe terminating specifications. We propose a model-based method for describing terminating specifications. In our method, a model of a given specification can be used for proving its termination. Since specifiers are describing a specification while thinking its model in their mind, our model-based termination methods are suitable for algebraic specifications. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Proceedings of the International MultiConference of Engineers & Computer Scientists 2012 Volume I is the property of International Association of Engineers (IAENG) and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=82785061
RecordInfo BibRecord:
  BibEntity:
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 6
        StartPage: 192
    Subjects:
      – SubjectFull: Rewriting systems (Computer science)
        Type: general
      – SubjectFull: Algebra
        Type: general
      – SubjectFull: Machine theory
        Type: general
      – SubjectFull: Technical specifications
        Type: general
      – SubjectFull: Computer software termination
        Type: general
    Titles:
      – TitleFull: On Describing Terminating Algebraic Specifications Based on Their Models.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Nakamura, Masaki
      – PersonEntity:
          Name:
            NameFull: Ogata, Kazuhiro
      – PersonEntity:
          Name:
            NameFull: Futatsugi, Kokichi
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 07
              Text: 2012
              Type: published
              Y: 2012
          Identifiers:
            – Type: isbn-print
              Value: 9789881925114
          Numbering:
            – Type: volume
              Value: 1
          Titles:
            – TitleFull: Proceedings of the International MultiConference of Engineers & Computer Scientists 2012 Volume I
              Type: main
ResultId 1