Computing Preconditions and Postconditions of While Loops

DOI10.1007/978-3-642-23283-1_13zbMath1350.68062OpenAlexW1819610226MaRDI QIDQ3105751

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

Publication date: 6 January 2012

Published in: Theoretical Aspects of Computing – ICTAC 2011 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-23283-1_13

zbMATH Keywords

relational calculusprogram correctnessprogramming language semanticsweakest preconditioninvariant relationstrongest postconditionwhile loop

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

A versatile concept for the analysis of loops

Cites Work

• Efficient weakest preconditions
• Mathematics for reasoning about loop functions
• On the lattice of specifications: Applications to a specification methodology
• Invariant functions and invariant relations: an alternative to invariant assertions
• Guarded commands, nondeterminacy and formal derivation of programs
• Hoare logic for Java in Isabelle/HOL
• Avoiding exponential explosion
• Predicate abstraction for software verification
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Computing Preconditions and Postconditions of While Loops