### Abstract

We study three different Hoare logics for reasoning about time bounds of imperative programs and formalize them in Isabelle/HOL: a classical Hoare like logic due to Nielson, a logic with potentials due to Carbonneaux et al. and a separation logic following work by Atkey, Chaguérand and Pottier. These logics are formally shown to be sound and complete. Verification condition generators are developed and are shown sound and complete too. We also consider variants of the systems where we abstract from multiplicative constants in the running time bounds, thus supporting a big-O style of reasoning. Finally we compare the expressive power of the three systems.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics

### Related publications

- Haslbeck, M. P. L., & Nipkow, T. (2018). Hoare Logics for Time Bounds. Lecture Notes in Computer Science, 155–171. https://doi.org/10.1007/978-3-319-89960-2_9

### Session Hoare_Time

- AExp
- BExp
- Com
- Big_Step
- Big_StepT
- Nielson_Hoare
- Nielson_VCG
- Vars
- Nielson_VCGi
- Nielson_VCGi_complete
- Nielson_Examples
- Nielson_Sqrt
- Quant_Hoare
- Quant_VCG
- Quant_Examples
- QuantK_Hoare
- QuantK_VCG
- QuantK_Examples
- QuantK_Sqrt
- Partial_Evaluation
- Product_Separation_Algebra
- Sep_Algebra_Add
- Big_StepT_Partial
- SepLog_Hoare
- SepLog_Examples
- SepLogK_Hoare
- SepLogK_VCG
- Discussion
- DiscussionO
- Hoare_Time

### Depends on

- Separation Algebra

### Auto-related entries

- Combinatorial Enumeration Algorithms
- Verifying Imperative Programs using Auto2
- COMPLX: A Verification Framework for Concurrent Imperative Programs
- A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment

## Cite

×

Hoare_Time-AFP

    @article{Hoare_Time-AFP,
      author  = {Maximilian P. L. Haslbeck and Tobias Nipkow},
      title   = {Hoare Logics for Time Bounds},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Hoare_Time.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Feb 26, 2018 : Isabelle2017