View in EDS PDF Full Text

Proving loop termination: Beyond the traditional method.

Saved in:
Bibliographic Details
Title: Proving loop termination: Beyond the traditional method.
Authors: Chen, Tennyson X.1 chen@rti.org, Meyer, Martin D.1
Source: Journal of Computational Methods in Sciences & Engineering (Sage Publications Inc.). 2009 Supplement 2, Vol. 9, p169-S178. 10p. 1 Chart.
Subjects: Loop tiling (Computer science), Iterative methods (Mathematics), Recursive functions, Recursive programming, Computer memory management
Abstract: The traditional method for proving loop termination requires us to define a bound function of program variables. The criterion in this method is well-defined and can be easy to apply, as such functions are obvious for many loops. However in some cases, it can be very difficult to define a bound function. In this paper, we discuss how to prove loop termination by using alternative methods. First we show how to prove loop termination by solving a recursive relation that defines the number of iterations remaining in any execution state. Then we introduce a step-by-step approach for applying this recursive relation method. This new method can also be used to investigate preconditions that lead to loop termination in non-deterministic cases. Finally, we illustrate another method that uses a more general criterion for proving loop termination. The new criterion is a generalization of the classical one. This paper does not attempt to offer a one-size-fits-all approach. Rather, it provides some alternative methods that make proving loop termination easier in some cases, where termination might otherwise be difficult if not impossible to prove. [ABSTRACT FROM AUTHOR]
Copyright of Journal of Computational Methods in Sciences & Engineering (Sage Publications Inc.) is the property of Sage Publications Inc. 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: 43520700
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Proving loop termination: Beyond the traditional method.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Chen%2C+Tennyson+X%2E%22">Chen, Tennyson X.</searchLink><relatesTo>1</relatesTo><i> chen@rti.org</i><br /><searchLink fieldCode="AR" term="%22Meyer%2C+Martin+D%2E%22">Meyer, Martin D.</searchLink><relatesTo>1</relatesTo>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+Computational+Methods+in+Sciences+%26+Engineering+%28Sage+Publications+Inc%2E%29%22">Journal of Computational Methods in Sciences & Engineering (Sage Publications Inc.)</searchLink>. 2009 Supplement 2, Vol. 9, p169-S178. 10p. 1 Chart.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Loop+tiling+%28Computer+science%29%22">Loop tiling (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Iterative+methods+%28Mathematics%29%22">Iterative methods (Mathematics)</searchLink><br /><searchLink fieldCode="DE" term="%22Recursive+functions%22">Recursive functions</searchLink><br /><searchLink fieldCode="DE" term="%22Recursive+programming%22">Recursive programming</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+memory+management%22">Computer memory management</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: The traditional method for proving loop termination requires us to define a bound function of program variables. The criterion in this method is well-defined and can be easy to apply, as such functions are obvious for many loops. However in some cases, it can be very difficult to define a bound function. In this paper, we discuss how to prove loop termination by using alternative methods. First we show how to prove loop termination by solving a recursive relation that defines the number of iterations remaining in any execution state. Then we introduce a step-by-step approach for applying this recursive relation method. This new method can also be used to investigate preconditions that lead to loop termination in non-deterministic cases. Finally, we illustrate another method that uses a more general criterion for proving loop termination. The new criterion is a generalization of the classical one. This paper does not attempt to offer a one-size-fits-all approach. Rather, it provides some alternative methods that make proving loop termination easier in some cases, where termination might otherwise be difficult if not impossible to prove. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Journal of Computational Methods in Sciences & Engineering (Sage Publications Inc.) is the property of Sage Publications Inc. 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=43520700
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.3233/JCM-2009-0245
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 10
        StartPage: 169
    Subjects:
      – SubjectFull: Loop tiling (Computer science)
        Type: general
      – SubjectFull: Iterative methods (Mathematics)
        Type: general
      – SubjectFull: Recursive functions
        Type: general
      – SubjectFull: Recursive programming
        Type: general
      – SubjectFull: Computer memory management
        Type: general
    Titles:
      – TitleFull: Proving loop termination: Beyond the traditional method.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Chen, Tennyson X.
      – PersonEntity:
          Name:
            NameFull: Meyer, Martin D.
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 03
              M: 02
              Text: 2009 Supplement 2
              Type: published
              Y: 2009
          Identifiers:
            – Type: issn-print
              Value: 14727978
          Numbering:
            – Type: volume
              Value: 9
          Titles:
            – TitleFull: Journal of Computational Methods in Sciences & Engineering (Sage Publications Inc.)
              Type: main
ResultId 1