Computing preconditions and postconditions of while loops

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Scopus citations

Abstract

Weakest preconditions were introduced by Dijkstra as a tool to define the semantics of programming constructs, and thereby as a means to prove the correctness of programs; the dual concept of strongest postcondition was introduced subsequently as an alternative means for the same ends. In this paper, we present and discuss a method to compute weakest preconditions and strongest postconditions of while loops in a C-like programming language; to this effect, we use the concept of invariant relation. Whereas the task of computing weakest preconditions and strongest postconditions of while loops is usually approached by limiting the number of iterations and applying successive sequential compositions, invariant relations afford us a crisper, closed form solution.

Original languageEnglish (US)
Title of host publicationTheoretical Aspects of Computing, ICTAC 2011 - 8th International Colloquium, Proceedings
Pages173-193
Number of pages21
DOIs
StatePublished - Sep 19 2011
Event8th International Colloquium on Theoretical Aspects of Computing, ICTAC 2011 - Johannesburg, South Africa
Duration: Aug 31 2011Sep 2 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6916 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th International Colloquium on Theoretical Aspects of Computing, ICTAC 2011
CountrySouth Africa
CityJohannesburg
Period8/31/119/2/11

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Keywords

  • invariant relation
  • program correctness
  • programming language semantics
  • relational calculus
  • strongest postcondition
  • weakest precondition
  • while loop

Fingerprint Dive into the research topics of 'Computing preconditions and postconditions of while loops'. Together they form a unique fingerprint.

Cite this