### 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

### Topics

### 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