Reflexive transitive invariant relations: A basis for computing loop functions

Ali Mili; Shir Aharon; Chaitanya Nadkarni; Lamia Labed Jilani; Asma Louhichi; Olfa Mraihi

doi:10.1016/j.jsc.2008.11.007

Reflexive transitive invariant relations: A basis for computing loop functions

Ali Mili, Shir Aharon, Chaitanya Nadkarni, Lamia Labed Jilani, Asma Louhichi, Olfa Mraihi

Research output: Contribution to journal › Article › peer-review

4 Scopus citations

Abstract

Invariant assertions play an important role in the analysis and verification of iterative programs. In this paper, we introduce a related but distinct concept, namely that of invariant relation. While invariant assertions are useful to prove the correctness of a loop with respect to a specification (represented by a precondition/ postcondition pair) in Hoare's logic, invariant relations are useful to derive the function of the loop in Mills' logic.

Original language	English (US)
Pages (from-to)	1114-1143
Number of pages	30
Journal	Journal of Symbolic Computation
Volume	45
Issue number	11
DOIs	https://doi.org/10.1016/j.jsc.2008.11.007
State	Published - Nov 2010

All Science Journal Classification (ASJC) codes

Algebra and Number Theory
Computational Mathematics

Keywords

Computing loop behavior
Function extraction
Invariant assertions
Invariant functions
Invariant relations
Loop functions
Refinement calculus
Relational calculus

Access to Document

10.1016/j.jsc.2008.11.007

Cite this

@article{2fa05289d6f1414082dfb62f10f681ef,

title = "Reflexive transitive invariant relations: A basis for computing loop functions",

abstract = "Invariant assertions play an important role in the analysis and verification of iterative programs. In this paper, we introduce a related but distinct concept, namely that of invariant relation. While invariant assertions are useful to prove the correctness of a loop with respect to a specification (represented by a precondition/ postcondition pair) in Hoare's logic, invariant relations are useful to derive the function of the loop in Mills' logic.",

keywords = "Computing loop behavior, Function extraction, Invariant assertions, Invariant functions, Invariant relations, Loop functions, Refinement calculus, Relational calculus",

author = "Ali Mili and Shir Aharon and Chaitanya Nadkarni and Jilani, {Lamia Labed} and Asma Louhichi and Olfa Mraihi",

year = "2010",

month = nov,

doi = "10.1016/j.jsc.2008.11.007",

language = "English (US)",

volume = "45",

pages = "1114--1143",

journal = "Journal of Symbolic Computation",

issn = "0747-7171",

publisher = "Academic Press",

number = "11",

}

TY - JOUR

T1 - Reflexive transitive invariant relations

T2 - A basis for computing loop functions

AU - Mili, Ali

AU - Aharon, Shir

AU - Nadkarni, Chaitanya

AU - Jilani, Lamia Labed

AU - Louhichi, Asma

AU - Mraihi, Olfa

PY - 2010/11

Y1 - 2010/11

N2 - Invariant assertions play an important role in the analysis and verification of iterative programs. In this paper, we introduce a related but distinct concept, namely that of invariant relation. While invariant assertions are useful to prove the correctness of a loop with respect to a specification (represented by a precondition/ postcondition pair) in Hoare's logic, invariant relations are useful to derive the function of the loop in Mills' logic.

AB - Invariant assertions play an important role in the analysis and verification of iterative programs. In this paper, we introduce a related but distinct concept, namely that of invariant relation. While invariant assertions are useful to prove the correctness of a loop with respect to a specification (represented by a precondition/ postcondition pair) in Hoare's logic, invariant relations are useful to derive the function of the loop in Mills' logic.

KW - Computing loop behavior

KW - Function extraction

KW - Invariant assertions

KW - Invariant functions

KW - Invariant relations

KW - Loop functions

KW - Refinement calculus

KW - Relational calculus

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

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

U2 - 10.1016/j.jsc.2008.11.007

DO - 10.1016/j.jsc.2008.11.007

M3 - Article

AN - SCOPUS:77956467988

SN - 0747-7171

VL - 45

SP - 1114

EP - 1143

JO - Journal of Symbolic Computation

JF - Journal of Symbolic Computation

IS - 11

ER -

Reflexive transitive invariant relations: A basis for computing loop functions

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this