A Hoare-like proof system for analysing the computation time of programs
Versions of Hoare logic have been introduced to prove partial and total correctness properties of programs. In this paper it is shown how a Hoare-like proof system for while programs may be extended to prove properties of the computation time as well, it should be stressed that the system does not require the programs to be modified by inserting explicit operations upon a clock variable. We generalize the notions of arithmetically sound and complete and show that the proof system satisfies these. Also we derive formal rules corresponding to the informal rules for determining the computation time of while programs. The applicability of the proof system is illustrated by an example, the bubble sorting algorithm.
- Axiomatic-like performance analysis (ALPA)
- Graded Hoare logic and its categorical semantics
- Fifty years of Hoare's logic
- Hoare logics for time bounds. A study in meta theory
- Weakest precondition reasoning for expected run-times of probabilistic programs
- scientific article; zbMATH DE number 3846835 (Why is no real title available?)
- Time credits and time receipts in Iris
- Semantic foundations for cost analysis of pipeline-optimized programs
- Formal verification and evaluation of execution time in the envelope theory
- Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
This page was built for publication: A Hoare-like proof system for analysing the computation time of programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1091122)
