Bridling the Complexity

  • W. H. J. Feijen
  • A. J. M. van Gasteren
Part of the Monographs in Computer Science book series (MCS)

Abstract

Let us consider a multiprogram with N components, each containing M atomic statements and, hence, M assertions, and let us count how much work is involved in proving the correctness of the annotation of such a multiprogram. First of all, there are M × N assertions in the game. Secondly, for each individual assertion we have to check its local correctness — counting for 1 — and its global correctness — counting for M × (N-1). As a result, the total amount of proof obligations to be fulfilled equals
$$M\; \times \;N \times \;(1 + M\; \times \;(N - 1)) $$
which is quadratic in the size — i.e. the number of atomic statements — of the multiprogram. Even for a modestly sized program with M = 7 and N = 5, the workload already consists of
$$1.015$$
proofs to be carried out. This is definitely far beyond what can be expected from a human being. Even an automatic proof system would quickly be defeated by such a quadratic explosion. The main cause of this explosion is the necessity to prove the global correctness of assertions.

Keywords

System Invariant Atomic Statement Proof System Local Correctness Mutual Exclusion 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 1999

Authors and Affiliations

  • W. H. J. Feijen
    • 1
  • A. J. M. van Gasteren
    • 1
  1. 1.Department of Computing ScienceEindhoven University of TechnologyEindhovenThe Netherlands

Personalised recommendations