Invariant functions and invariant relations: An alternative to invariant assertions

Lamia Labed Jilani; Olfa Mraihi; Asma Louhichi; Wided Ghardallou; Khaled Bsaies; Ali Mili

doi:10.1016/j.jsc.2012.04.001

Invariant functions and invariant relations: An alternative to invariant assertions

Lamia Labed Jilani, Olfa Mraihi, Asma Louhichi, Wided Ghardallou, Khaled Bsaies, Ali Mili

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

7 Scopus citations

Abstract

Whereas the analysis of loops in imperative programs is, justifiably, dominated by the concept of invariant assertion, we submit a related but different concept, of invariant relation, and show how it can be used to analyze diverse aspects of a while loop. We also introduce the concept of invariant function, which is used to generate a broad class of invariant relations.

Original language	English (US)
Pages (from-to)	1-36
Number of pages	36
Journal	Journal of Symbolic Computation
Volume	48
DOIs	https://doi.org/10.1016/j.jsc.2012.04.001
State	Published - Jan 2013

All Science Journal Classification (ASJC) codes

Algebra and Number Theory
Computational Mathematics

Keywords

Invariant assertions
Invariant functions
Invariant generation
Invariant relations
Loop functions
Reasoning about loops
While loops

Access to Document

10.1016/j.jsc.2012.04.001

Cite this

@article{51d59321150244e39c05373a9a97ee9c,

title = "Invariant functions and invariant relations: An alternative to invariant assertions",

abstract = "Whereas the analysis of loops in imperative programs is, justifiably, dominated by the concept of invariant assertion, we submit a related but different concept, of invariant relation, and show how it can be used to analyze diverse aspects of a while loop. We also introduce the concept of invariant function, which is used to generate a broad class of invariant relations.",

keywords = "Invariant assertions, Invariant functions, Invariant generation, Invariant relations, Loop functions, Reasoning about loops, While loops",

author = "Jilani, \{Lamia Labed\} and Olfa Mraihi and Asma Louhichi and Wided Ghardallou and Khaled Bsaies and Ali Mili",

year = "2013",

month = jan,

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

language = "English (US)",

volume = "48",

pages = "1--36",

journal = "Journal of Symbolic Computation",

issn = "0747-7171",

publisher = "Academic Press",

}

TY - JOUR

T1 - Invariant functions and invariant relations

T2 - An alternative to invariant assertions

AU - Jilani, Lamia Labed

AU - Mraihi, Olfa

AU - Louhichi, Asma

AU - Ghardallou, Wided

AU - Bsaies, Khaled

AU - Mili, Ali

PY - 2013/1

Y1 - 2013/1

N2 - Whereas the analysis of loops in imperative programs is, justifiably, dominated by the concept of invariant assertion, we submit a related but different concept, of invariant relation, and show how it can be used to analyze diverse aspects of a while loop. We also introduce the concept of invariant function, which is used to generate a broad class of invariant relations.

AB - Whereas the analysis of loops in imperative programs is, justifiably, dominated by the concept of invariant assertion, we submit a related but different concept, of invariant relation, and show how it can be used to analyze diverse aspects of a while loop. We also introduce the concept of invariant function, which is used to generate a broad class of invariant relations.

KW - Invariant assertions

KW - Invariant functions

KW - Invariant generation

KW - Invariant relations

KW - Loop functions

KW - Reasoning about loops

KW - While loops

UR - https://www.scopus.com/pages/publications/84867234206

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

U2 - 10.1016/j.jsc.2012.04.001

DO - 10.1016/j.jsc.2012.04.001

M3 - Article

AN - SCOPUS:84867234206

SN - 0747-7171

VL - 48

SP - 1

EP - 36

JO - Journal of Symbolic Computation

JF - Journal of Symbolic Computation

ER -

Invariant functions and invariant relations: An alternative to invariant assertions

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this