Computing preconditions and postconditions of while loops

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

doi:10.1007/978-3-642-23283-1_13

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 proceeding › Conference 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 language	English (US)
Title of host publication	Theoretical Aspects of Computing, ICTAC 2011 - 8th International Colloquium, Proceedings
Pages	173-193
Number of pages	21
DOIs	https://doi.org/10.1007/978-3-642-23283-1_13
State	Published - 2011
Event	8th International Colloquium on Theoretical Aspects of Computing, ICTAC 2011 - Johannesburg, South Africa Duration: Aug 31 2011 → Sep 2 2011

Publication series

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

Other

Other	8th International Colloquium on Theoretical Aspects of Computing, ICTAC 2011
Country/Territory	South Africa
City	Johannesburg
Period	8/31/11 → 9/2/11

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Keywords

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

Access to Document

10.1007/978-3-642-23283-1_13

Cite this

Mraihi, O., Ghardallou, W., Louhichi, A., Labed Jilani, L., Bsaies, K., & Mili, A. (2011). Computing preconditions and postconditions of while loops. In Theoretical Aspects of Computing, ICTAC 2011 - 8th International Colloquium, Proceedings (pp. 173-193). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6916 LNCS). https://doi.org/10.1007/978-3-642-23283-1_13

@inproceedings{ef463da89d804ca6a9aeee7932d358c5,

title = "Computing preconditions and postconditions of while loops",

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.",

keywords = "invariant relation, program correctness, programming language semantics, relational calculus, strongest postcondition, weakest precondition, while loop",

author = "Olfa Mraihi and Wided Ghardallou and Asma Louhichi and {Labed Jilani}, Lamia and Khaled Bsaies and Ali Mili",

year = "2011",

doi = "10.1007/978-3-642-23283-1_13",

language = "English (US)",

isbn = "9783642232824",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "173--193",

booktitle = "Theoretical Aspects of Computing, ICTAC 2011 - 8th International Colloquium, Proceedings",

note = "8th International Colloquium on Theoretical Aspects of Computing, ICTAC 2011 ; Conference date: 31-08-2011 Through 02-09-2011",

}

Mraihi, O, Ghardallou, W, Louhichi, A, Labed Jilani, L, Bsaies, K & Mili, A 2011, Computing preconditions and postconditions of while loops. in Theoretical Aspects of Computing, ICTAC 2011 - 8th International Colloquium, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6916 LNCS, pp. 173-193, 8th International Colloquium on Theoretical Aspects of Computing, ICTAC 2011, Johannesburg, South Africa, 8/31/11. https://doi.org/10.1007/978-3-642-23283-1_13

Computing preconditions and postconditions of while loops. / Mraihi, Olfa; Ghardallou, Wided; Louhichi, Asma et al.
Theoretical Aspects of Computing, ICTAC 2011 - 8th International Colloquium, Proceedings. 2011. p. 173-193 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6916 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Computing preconditions and postconditions of while loops

AU - Mraihi, Olfa

AU - Ghardallou, Wided

AU - Louhichi, Asma

AU - Labed Jilani, Lamia

AU - Bsaies, Khaled

AU - Mili, Ali

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

KW - invariant relation

KW - program correctness

KW - programming language semantics

KW - relational calculus

KW - strongest postcondition

KW - weakest precondition

KW - while loop

UR - http://www.scopus.com/inward/record.url?scp=80052726204&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80052726204&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-23283-1_13

DO - 10.1007/978-3-642-23283-1_13

M3 - Conference contribution

AN - SCOPUS:80052726204

SN - 9783642232824

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 173

EP - 193

BT - Theoretical Aspects of Computing, ICTAC 2011 - 8th International Colloquium, Proceedings

T2 - 8th International Colloquium on Theoretical Aspects of Computing, ICTAC 2011

Y2 - 31 August 2011 through 2 September 2011

ER -

Mraihi O, Ghardallou W, Louhichi A, Labed Jilani L, Bsaies K, Mili A. Computing preconditions and postconditions of while loops. In Theoretical Aspects of Computing, ICTAC 2011 - 8th International Colloquium, Proceedings. 2011. p. 173-193. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-23283-1_13

Computing preconditions and postconditions of while loops

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this