Theoretical Computer Science

Tools

Matchbox (Matchbox)

TcT (Tyrolean Complexity Tool)

CaT (Complexity and Termination)

AProVE (Automated Program Verification Environment)

Oops (Oops)

Oops is no real complexity analyzer. Its main purpose was to mark unsuitable examples in the runtime complexity categories during the Termination Competition 2010. Many thanks to Georg Moser for the fitting name.

For runtime complexity, one does not analyze the derivation length of arbitrary terms (as one does in derivational complexity), but only of terms with exactly one defined symbol. For some systems this leads to much better intuition about the complexity of the described functions, but for others this definition yields strange results. For example applicative systems only have one defined symbol (the apply symbol), whereas the rest are just constants. Starting only with one apply symbol (as runtime complexity requires), one is most likely not able to build the derivation sequences the author of the example intended.

Furthermore, for such examples where all constructor symbols are constants, there are only finitely many basic terms. This makes asymptotic complexity analysis pointless, as one cannot build arbitrary large start terms.

We identified the following situations, in which we can conclude constant complexity. The strategy of oops is just to identify these situations and return an upper bound of O(1) if successful.