Überprüfung der Programmleistung

Es wird gezeigt, dass Spezifikationen der Programmleistung formell verifiziert werden können. Formale Verifizierungstechniken, insbesondere die Methode der induktiven Aussagen, können angepasst werden, um zu zeigen, dass die maximale oder durchschnittliche Ausführungszeit eines Programms korrekt durch die mit dem Programm gelieferten Spezifikationen beschrieben wird. Um die durchschnittliche Ausführungszeit formal zu bestimmen, werden Verzweigungswahrscheinlichkeiten unter Verwendung induktiver Aussagen ausgedrückt, die Wahrscheinlichkeitsverteilungen beinhalten. Verifizierungsbedingungen werden gebildet und bewiesen, die festlegen, dass, wenn die Eingabeverteilung korrekt durch die Eingabespezifikationen beschrieben wird, die induktiven Aussagen die Wahrscheinlichkeitsverteilungen der Daten während der Ausführung korrekt beschreiben. Sobald die induktiven Aussagen als richtig erwiesen sind, werden Verzweigungswahrscheinlichkeiten ermittelt und die durchschnittliche Berechnungszeit wird berechnet.