Relational Methods in the Analysis of While Loops: Observations of Versatility

Autor:	Ali Mili, Lamia Labed Jilani, Asma Louhichi, Olfa Mraihi, Khaled Bsaïes
Rok vydání:	2009
Předmět:	Loop invariant Theoretical computer science Software Correctness Relational calculus Refinement calculus business.industry Computer science While loop Invariant (mathematics) business Invariant (computer science)
Zdroj:	Relations and Kleene Algebra in Computer Science ISBN: 9783642046384 RelMiCS
DOI:	10.1007/978-3-642-04639-1_17
Popis:	Despite much progress in the design of programming languages, the vast majority of software being written and deployed nowadays remains written in languages where iteration is the main inductive construct, and the main source of algorithmic complexity. For the past four decades, the analysis of iterative constructs has been dominated, not undeservedly, by the concept of invariant assertions. In this paper we submit relation-based alternatives, namely invariant relations and invariant functions, and show how these can provide complementary perspectives, and can enrich the analysis of iterations. Whereas loop invariants can be used to establish the correctness of iterative programs in Hoare logics, invariant relations and invariant functions are used to derive program functions in Mills' logic. In keeping with the conference format, we do not delve too much into theoretical results, and focus instead on the applied aspects of our relation-theoretic approach.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::80cd66e7538369f4ef19e4b41838f095 https://doi.org/10.1007/978-3-642-04639-1_17 Zobrazit plný text záznamu