ALG-Semantics

This is an ongoing work to give formal semantics to the pseudocode in the book "introduction to algorithms" to verify the worst case execution time of each algorithm.

Instructions

The semantics uses version 4.0.1 of the K tool, on its java backend.

To compile:

kompile alg4.k

To run a program:

krun CH-2/insertion-sort.c

To run all the programs at once

ktest config.xml