Computing Preconditions and Postconditions of While Loops

DOI10.1007/978-3-642-23283-1_13zbMATH Open1350.68062OpenAlexW1819610226MaRDI QIDQ3105751FDOQ3105751

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

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

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)

Cites Work

• On the lattice of specifications: Applications to a specification methodology
• Title not available (Why is that?)
• An axiomatic basis for computer programming
• Title not available (Why is that?)
• Title not available (Why is that?)
• Guarded commands, nondeterminacy and formal derivation of programs
• Predicate abstraction for software verification
• Hoare logic for Java in Isabelle/HOL
• Efficient weakest preconditions
• Avoiding exponential explosion: generating compact verification conditions
• Mathematics for reasoning about loop functions
• Invariant functions and invariant relations: an alternative to invariant assertions
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (5)

• Efficient weakest preconditions
• Strongest invariant functions: Their use in the systematic analysis of while statements
• A versatile concept for the analysis of loops
• Title not available (Why is that?)
• Title not available (Why is that?)

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)