Invariant functions and invariant relations: an alternative to invariant assertions

DOI10.1016/j.jsc.2012.04.001zbMath1253.68085OpenAlexW2118456460MaRDI QIDQ1760096

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

Publication date: 12 November 2012

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2012.04.001

zbMATH Keywords

invariant functionsinvariant relationsinvariant generationloop functionsinvariant assertionsreasoning about loopswhile loops

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Related Items (2)

Convergence: integrating termination and abort-freedom ⋮ Computing Preconditions and Postconditions of While Loops

Uses Software

• LOOPUS

This page was built for publication: Invariant functions and invariant relations: an alternative to invariant assertions