Computing Preconditions and Postconditions of While Loops

DOI10.1007/978-3-642-23283-1_13MaRDI QIDQ3105751zbMATH OpenOpenAlexFDO

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

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

program correctnessprogramming language semanticsweakest preconditionrelational calculusinvariant relationstrongest postconditionwhile loop

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 3917681
• Methods of calculating the preconditions of programs
• Inferring Loop Invariants Using Postconditions
• Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
• Reasoning about loops in total and general correctness
• scientific article; zbMATH DE number 813263
• Loop checking and the well-founded semantics
• Heuristics for constructing while loops

Cites work

• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1330435 (Why is no real title available?)
• scientific article; zbMATH DE number 1531358 (Why is no real title available?)
• An axiomatic basis for computer programming
• Avoiding exponential explosion: generating compact verification conditions
• Efficient weakest preconditions
• Guarded commands, nondeterminacy and formal derivation of programs
• Hoare logic for Java in Isabelle/HOL
• Invariant functions and invariant relations: an alternative to invariant assertions
• Mathematics for reasoning about loop functions
• On the lattice of specifications: Applications to a specification methodology
• Predicate abstraction for software verification

Cited in

(5)

• Strongest invariant functions: Their use in the systematic analysis of while statements
• Efficient weakest preconditions
• A versatile concept for the analysis of loops
• scientific article; zbMATH DE number 4047056 (Why is no real title available?)
• scientific article; zbMATH DE number 3917681 (Why is no real title available?)

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3105751)