Invariant assertions, invariant relations, and invariant functions

Olfa Mraihi; Asma Louhichi; Lamia Labed Jilani; Jules Desharnais; Ali Mili

doi:10.1016/j.scico.2012.05.006

Invariant assertions, invariant relations, and invariant functions

Olfa Mraihi, Asma Louhichi, Lamia Labed Jilani, Jules Desharnais, Ali Mili

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

15 Scopus citations

Abstract

Invariant assertions play an important role in the analysis and documentation of while loops of imperative programs. Invariant functions and invariant relations are alternative analysis tools that are distinct from invariant assertions but are related to them. In this paper we discuss these three concepts and analyze their relationships. The study of invariant functions and invariant relations is interesting not only because it provides alternative means to analyze loops, but also because it gives us insights into the structure of invariant assertions, hence it may help us enhance techniques for generating invariant assertions.

Original language	English (US)
Pages (from-to)	1212-1239
Number of pages	28
Journal	Science of Computer Programming
Volume	78
Issue number	9
DOIs	https://doi.org/10.1016/j.scico.2012.05.006
State	Published - Sep 1 2013

All Science Journal Classification (ASJC) codes

Software
Information Systems
Modeling and Simulation
Computational Theory and Mathematics

Keywords

Invariant assertions
Invariant functions
Invariant relations
Loop functions
Loop invariants
Program analysis
Program verification
While loops

Access to Document

10.1016/j.scico.2012.05.006

Cite this

@article{137ffffc28f94403b3b9ef45c6eedfb0,

title = "Invariant assertions, invariant relations, and invariant functions",

abstract = "Invariant assertions play an important role in the analysis and documentation of while loops of imperative programs. Invariant functions and invariant relations are alternative analysis tools that are distinct from invariant assertions but are related to them. In this paper we discuss these three concepts and analyze their relationships. The study of invariant functions and invariant relations is interesting not only because it provides alternative means to analyze loops, but also because it gives us insights into the structure of invariant assertions, hence it may help us enhance techniques for generating invariant assertions.",

keywords = "Invariant assertions, Invariant functions, Invariant relations, Loop functions, Loop invariants, Program analysis, Program verification, While loops",

author = "Olfa Mraihi and Asma Louhichi and Jilani, {Lamia Labed} and Jules Desharnais and Ali Mili",

year = "2013",

month = sep,

day = "1",

doi = "10.1016/j.scico.2012.05.006",

language = "English (US)",

volume = "78",

pages = "1212--1239",

journal = "Science of Computer Programming",

issn = "0167-6423",

publisher = "Elsevier",

number = "9",

}

TY - JOUR

T1 - Invariant assertions, invariant relations, and invariant functions

AU - Mraihi, Olfa

AU - Louhichi, Asma

AU - Jilani, Lamia Labed

AU - Desharnais, Jules

AU - Mili, Ali

PY - 2013/9/1

Y1 - 2013/9/1

N2 - Invariant assertions play an important role in the analysis and documentation of while loops of imperative programs. Invariant functions and invariant relations are alternative analysis tools that are distinct from invariant assertions but are related to them. In this paper we discuss these three concepts and analyze their relationships. The study of invariant functions and invariant relations is interesting not only because it provides alternative means to analyze loops, but also because it gives us insights into the structure of invariant assertions, hence it may help us enhance techniques for generating invariant assertions.

AB - Invariant assertions play an important role in the analysis and documentation of while loops of imperative programs. Invariant functions and invariant relations are alternative analysis tools that are distinct from invariant assertions but are related to them. In this paper we discuss these three concepts and analyze their relationships. The study of invariant functions and invariant relations is interesting not only because it provides alternative means to analyze loops, but also because it gives us insights into the structure of invariant assertions, hence it may help us enhance techniques for generating invariant assertions.

KW - Invariant assertions

KW - Invariant functions

KW - Invariant relations

KW - Loop functions

KW - Loop invariants

KW - Program analysis

KW - Program verification

KW - While loops

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

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

U2 - 10.1016/j.scico.2012.05.006

DO - 10.1016/j.scico.2012.05.006

M3 - Article

AN - SCOPUS:84878822973

SN - 0167-6423

VL - 78

SP - 1212

EP - 1239

JO - Science of Computer Programming

JF - Science of Computer Programming

IS - 9

ER -

Invariant assertions, invariant relations, and invariant functions

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this