Space-aware Hoare specifications — definitions

Ordinary TM.HoareTime records a bounded terminating run, but logarithmic-space computation requires a bound on every reachable configuration. This module pairs those two obligations in one compositional contract.

def Complexity.TM.HoareSpace {n : ℕ} (tm : TM n) (pre : TapePred n) (inputLength spaceBound : ℕ) : Prop

An all-reachable auxiliary-space contract from tapes satisfying pre.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.HoareTimeSpace {n : ℕ} (tm : TM n) (pre post : TapePred n) (timeBound inputLength spaceBound : ℕ) : Prop

A time-and-space Hoare contract: ordinary terminating behavior paired with an independent all-reachable auxiliary-space contract.

Equations

• tm.HoareTimeSpace pre post timeBound inputLength spaceBound = (tm.HoareTime pre post timeBound ∧ tm.HoareSpace pre inputLength spaceBound)