Sign in
Back
Invariant functions and invariant relations: An alternative to invariant assertions
Journal article   Open access  Peer reviewed

Invariant functions and invariant relations: An alternative to invariant assertions

Lamia Labed Jilani, Olfa Mraihi, Asma Louhichi, Wided Ghardallou, Khaled Bsaies and Ali Mili
Journal of symbolic computation, Vol.48, pp.1-36
01/2013
DOI: https://doi.org/10.1016/j.jsc.2012.04.001

Abstract

Invariant assertions Invariant functions Invariant generation Invariant relations Loop functions Reasoning about loops While loops
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.
url
https://doi.org/10.1016/j.jsc.2012.04.001View
Published (Version of record) Open

Metrics

1 Record Views

Details