Invariant relations for affine loops
Wided Ghardallou, Hessamaldin Mohammadi, Richard C. Linger, Mark G. Pleszkoch, JiMeng Loh, Ali Mili · Acta Informatica · 2024
Abstract Invariant relations are used to analyze while loops; while their primary application is to derive the function of a loop, they can also be used to derive loop invariants, weakest preconditions, strongest postconditions, sufficient conditions of correctness, necessary conditions of correctness, and termination conditions of loops. In this paper we present two generic invariant relations that capture the semantics of loops whose loop body applies affine transformations on numeric variables.