Informatik – eine eigenständige Wissenschaft?

Gute Wissenschaft bildet Theorien, indem sie Modelle entwickelt. Ein Modell ist ein System von Begriffen und Bezügen zwischen den Begriffen, um die Realität besser zu verstehen. „Realität“ liegt dabei entweder in der Natur vor oder wird – wie im Fall der Informatik – in Teilen von Menschen konstruiert. Ein besonders eindrucksvolles Beispiel ist die Physik: Jahrhundertelang haben Physiker nach einem vereinheitlichenden Modell für alle Zweige der Physik gesucht und so ein eindrucksvolles Gebäude wissenschaftlicher Theoriebildung entwickelt. Insbesondere entstand eine erstaunliche Harmonie von Physik und Mathematik [26] mit sehr abstrakten, aber überaus nützlichen wissenschaftlichen Konzepten und Modellen. Ein typisches Beispiel ist der Begriff der Energie. Mit ihm können ganz unterschiedliche Phänomene aufeinander bezogen und quantitativ bestimmt werden, die beispielsweise auftreten, wenn ein stehendes Fahrzeug beschleunigt und an eine Wand gefahren wird: In diesem Prozess tritt eine bestimmte Menge an Energie auf, die erst im Benzin, dann in der Beschleunigung und schließlich in der Umformung von Blech steckt. Die Nützlichkeit des Begriffs Energie liegt in seiner quantifizierbaren Invarianz für dynamische Prozesse. Derartige Invarianten, oft als „Naturgesetze“ bezeichnet, sind das Gerüst von Wissenschaft. In den letzten Jahren sucht beispielsweise auch die „Systembiologie“ nach solchen Begriffen und Invarianten zum besseren Verständnis von Stoffwechselprozessen aller Art.

Informatik sollte von der Physik und anderen Wissenschaften lernen, eine Theorie für ihre Gesamtheit zu bilden. John McCarthy hat schon 1963 in [27] die Entwicklung einer mathematikbasierten „Science of Computation“ angemahnt angeregt, in der die wichtigen Eigenschaften und Gegenstände dieser Wissenschaft aus wenigen grundlegenden Annahmen abgeleitet werden.

Indem Modelle den Kern einer wissenschaftlichen Theorie ausmachen, stellt sich die Frage nach Modellen in der Informatik. Wie oft in Naturwissenschaften, geht es auch in der Informatik um die Beschreibung dynamischer Eigenschaften, allerdings mit einem generellen und fundamentalen Unterschied: Physik beschreibt Verhalten im Allgemeinen kontinuierlich, mit Funktionen über einer reellen Zeitachse. Damit kann man wunderbar Differenzialgleichungen und Integrale bilden und vieles mehr. Informatik beschreibt Verhalten in diskreten Schritten; damit müssen und können ganz andere Eigenschaften beschrieben und mit ganz anderen mathematischen Analysetechniken analysiert werden.

Modelle werden in der Informatik für verschiedene Zwecke verwendet:

Nun gibt es eine Reihe von Modellierungstechniken, die diesen Aspekt unterstützen; allen voran die Unified Modeling Language (UML) [6] und – primär für die Wirtschaftsinformatik – Business Process Model and Notation (BPMN) [1]. Diese Techniken schlagen eine Vielzahl grafischer Ausdrucksmittel vor, um spezielle, subtile, domänenspezifische Sachverhalte auszudrücken. Und beide Techniken (und eine Reihe weiterer, beispielsweise Statecharts) werden durchaus zur Modellierung genutzt. Aber alle diese Techniken bieten wenige Möglichkeiten, gewünschte Eigenschaften des modellierten Systems im Modell nachzuweisen. Selbst wenn man also mit diesen Techniken modelliert und daraus Software generiert, wird nicht auf Modellebene formal über Korrektheit argumentiert, sondern auf der Software-Ebene.

Daneben gibt es allerdings durchaus Modellierungstechniken mit Analyse- und Verifikationskonzepten. Dazu gehören beispielsweise ALLOY, B, Focus, Live Sequence Charts, Petrinetze, TLA und Z, neben vielen anderen. Einige davon sind allerdings eher Konzeptstudien für ganz spezielle Eigenschaften und Aspekte.

Eine Modellierungstechnik wird sich auf Dauer nur durchsetzen, wenn sie starke Analysetechniken anbietet.

In einem generellen systematischen Aufbau von Prinzipien der Modellierung in der Informatik sollte es einem Modellierer möglich sein, mit einer passenden – formalen – Modellierungstechnik ein System vertrauenswürdig, nachvollziehbar und eindeutig zu beschreiben. Für ein gegebenes Beispiel haben wir normalerweise ein gutes Verständnis dafür, was eine angemessene Beschreibung ausmacht: Sie enthält alle Aspekte, die dem Modellierer wichtig sind, und vermeidet Aspekte, über die der Modellierer nicht reden möchte. Konkreter formuliert beschreibt ein vertrauenswürdiges Modell M eines diskreten Systems S:

Zusammengefast: Elementare und zusammengesetzte Objekte und Operationen sowie Zustände und Schritte von S und M sollten sich bijektiv entsprechen. Intuitives und formal dargestelltes Verhalten sollen also so eng wie irgend möglich zusammenhängen.

Nun stellt sich die Frage nach einer Modellierungstechnik, die diese Forderungen erfüllt, zumindest für eine hinreichend große Klasse von Systemen. Es ist offensichtlich, dass solche Objekte, Operationen, Zustände und Schritte im klassischen Sinn nicht immer berechenbare Funktionen sind. Mehr oder weniger deutlich wurde dieses Problem immer wieder angesprochen. Schon in seinem grundlegenden Werk The Art of Computer Programming [22] führt Donald Knuth mit computational methods (heutzutage oft als Transitionssystem bezeichnet) einen allgemeineren Begriff des Algorithmus ein: Eine computational method besteht aus einer Menge S von Zuständen und einer Next-state-Funktion F auf S, von der es heißt „F might involve operations that mortal man can’t always perform.“ [22, S. 8]. Knuth nennt eine computational method effektiv, wenn F eine berechenbare Funktion ist. Durchaus selbstkritisch erklärt Robin Milner in seiner EATCS award lecture [29]: „… we should have achieved a mathematical model of computation, perhaps highly abstract in contrast with the concrete nature of paper and register machines, but such that programming languages are merely executable fragments of the theory ….“ Es bleibt offen, welche Art nichtausführbarer Fragmente Milner meint.

Oft wird versucht, das klassische Berechnungskonzept aus Variablen, effektiven Objekten und Operationen über Zeichenketten und Programmen aus Wertzuweisung mit Sequenz, Alternative und bedingten Schleifen zu verallgemeinern auf freigewählte mathematische Objekte und Operationen, beispielsweise in [37]. Shepherdson in [33] entwickelt eine ähnliche Idee auf der Basis von Turingmaschinen. In einem etwas anderen Stil und aus rein logischer Perspektive betrachten Abstract State Machines [19] Programme über einer Signatur (einer Symbolmenge verschiedener Sorten); der Nutzer des Formalismus kann dann eine Signatur und seine gewünschte Struktur über dieser Signatur frei wählen und mit Termen über die Struktur reden.

Ein gutes Modell verwendet also Symbole, die in der modellierten Welt unmittelbar als Objekte oder Operationen interpretiert werden. Das unterscheidet Modelle von Programmen: Eine Programmiersprache fixiert die Interpretation der Symbole eines Programms.

Invarianz ist ein Eckpfeiler wissenschaftlicher Theoriebildung (Abschn. 1); damit stellt sich die Frage nach Invarianzbegriffen in der Informatik. Der bekannteste derartige Begriff ist sicherlich Hoares Invariantenkalkül [20] mit seinem Konzept der Schleifeninvarianten für klassische Programme [16] bezeichnet Schleifeninvarianz als eine der grundlegenden Ideen der Software-Konstruktion. Das mag zutreffen, wenn man die Korrektheit eines Systementwurfs ganz am Ende, bei der Programmerstellung in einer klassischen Programmiersprache ansiedelt. Eine Theorie der Informatik sollte allerdings Korrektheit von Modellen betrachten. Tatsächlich arbeiten viele Modellierungstechniken mit speziellen Invarianten: [36] schlägt beispielsweise Invarianten für Modelle verteilter Prozesse, verteilter Algorithmen und Kommunikationsprotokolle vor. Der Invariantenkalkül für Petrinetze ist besonders ausdrucksstark (weil Transitionen reversibel sind) [31].

Jede solche Invariante beschreibt zwischen Systemvariablen eines Systems einen Zusammenhang, der in allen erreichbaren Systemzuständen invariant bleibt. Diese Invarianzbegriffe bleiben damit sehr eng am gegebenen Systemmodell. Wie das Beispiel des Begriffs der Energie (Abschn. 1) zeigt, kennt die Physik weitaus tiefer liegende, weniger offensichtliche und dennoch (oder deshalb) äußerst nützliche Invarianten. Vergleichbar tief liegende Invarianzbegriffe sollte die Informatik auch anstreben. Solche Invarianten könnten vielleicht genau bestimmen, was invariant bleibt, wenn beispielsweise rechnergestützt:

Derzeit ist das alles Spekulation; es loht aber, systematisch nach Modellierungstechniken zu suchen, die im Vergleich mit bisherigen Konzepten weit abstraktere und weniger naheliegende, aber dennoch intuitiv verständliche Begriffe und Invarianten verwenden.

Eine konstruktive Definition eines solchen Informationsbegriffs ist nicht in Sicht. Sie hätte aber eine Reihe überaus wertvoller Konsequenzen, beispielsweise sollten damit die in Abschn. 4 beschriebenen Invarianten formal fassbar sein. Man sollte präzise formulieren können, was genau sich ändert und was gleich bleibt beim Kopieren, Löschen oder Zusammenfügen von Informationen oder Dokumenten. Datenschutz, Schutz der Privatsphäre und verwandte Begriffe könnten eine sehr viel präzisere Bedeutung bekommen.

Eine weitere interessante Eigenschaft eines solchen Informationsbegriffs sind informationserhaltende Operationen: Eine solche Operation f verliert keine Informationen; ein Argument a für f kann also aus dem Resultat f(a) zurückberechnet werden. Beispiele sind die Negation der Aussagenlogik und die positive Wurzel aus positiven reellen Zahlen. Solche reversiblen Funktionen sind oft betrachtet worden, vorwiegend im Kontext von Aussagenlogik und von Schaltkreisen [39]. Die Idee reversiblen Rechnens könnte IT Sicherheit entscheidend voranbringen: Ein Angreifer könnte retrospektiv zurückverfolgt werden.

Vielleicht gelingt die Charakterisierung spezieller Informationsbegriffe über die Operationen, die mit ihnen in einem jeweils gegebenen Kontext möglich oder erlaubt sind.

Klassische theoretische Informatik abstrahiert informationstechnische Prozesse zu berechenbaren Funktionen über Symbolketten. Mit den tief liegenden Resultaten zur Komplexitätstheorie und zu den Zusammenhängen zwischen Logik und Automatentheorie hat sich dieser Ansatz als theoretische Grundlage der Informatik etabliert. Das bekannteste operationale Modell dafür sind Turingmaschinen. Eine Turingmaschine mit einem Speicher und einem Prozessor kann als Abstraktion eines Rechners der 1960er-Jahre aufgefasst werden. Eine Multiprozessorarchitektur, die mehrere Prozessoren verwendet, um die Rechengeschwindigkeit zu erhöhen, lässt sich noch plausibel zu einer Architektur mit einem einzigen Prozessor abstrahieren. Ein System aus mehreren, miteinander kommunizierenden aktiven Komponenten kann auf einem 1‑Prozessor-System zwar simuliert werden, lässt sich aber nur schlecht als 1‑Prozessor-System auffassen, ohne den Sinn des Systems zu verfälschen.

Erste solche Systeme wurden in den 1980er-Jahren vorgeschlagen, insbesondere der Actor-Formalismus von Agha und Hewitt [2]. Ähnliche Ideen verfolgte beispielsweise die Sprache LINDA [11] und die Chemical Abstract Machine (CHAM) [5]. In dieser Metapher werden aktive Elemente als eine Art Moleküle aufgefasst, die in einer – metaphorischen – chemischen Lösung schwimmen und miteinander reagieren, sobald sie aufeinandertreffen und geeignete Reaktionsbedingungen bestehen. In diesem Rahmen sind zahlreiche Algorithmen formuliert worden. Ein anderes Beispiel ist der FOCUS-Formalismus von Broy [10], mit Komponenten, die stromverarbeitende Funktionen ausbilden. Schließlich gehören auch Petrinetze [31] in diese Reihe von Modellierungstechniken: jede Transition kann aufgefasst werden als elementare aktive Einheit.

Es stellt sich die Frage nach einer Theorie, die für derartige und viele weitere Modellierungstechniken eine angemessene abstrakte Grundlage bildet, in Analogie zu den berechenbaren Funktionen für sequenzielle Ein‑/Ausgabealgorithmen.

In einer Reihe von Papieren schlägt Wegner dafür Verallgemeinerungen von Turingmaschinen vor, beispielsweise in [40] und in [41]. In [13] wird allerdings die Korrektheit von Wegners Argumentation bestritten.

Mir geht es hier nicht um die Frage, „was ein Computer im Prinzip kann“, sondern um die wesentlich breitere Fragestellung, wie Systeme angemessen modelliert und analysiert werden können, die in diskreten Schritten voranschreiten und mit ihrer Umgebung interagieren.

Das Konzept diskreter Schritte beruht auf Zuständen: Ein Schritt beginnt in einem Zustand und endet in einem Zustand. Im klassischen Rahmen von Systembeschreibungen sind Zustände global: Jeder Schritt aktualisiert den gegenwärtigen Zustand. Ein einzelnes Verhalten, ein Ablauf, eine Berechnung, ist dann eine Sequenz s₀-t₁-s₁-t₂-s₂ … von Zuständen s_i und Schritten s_i‑1-t_i-s_i (i = 1,2, …). Viele Systemmodelle konstruieren globale Zustände eines aus Komponenten C₁, …, C_n komponierten Systems als kartesisches Produkt S₁ × … × S_n der Zustandsräume S_k der Komponenten C_k. Dabei entstehen für jeden Schritt einer Komponente mehrere Schritte des komponierten Systems. Voneinander unabhängige Schritte in verschiedenen Komponenten werden in diesem Modell nichtdeterministisch in beliebiger Reihenfolge notiert.

Abb. 1 zeigt ein kleines Beispiel: A und B seien zwei unabhängige Komponenten mit 3 bzw. 2 Zuständen und Schritten, die in Zyklen angeordnet sind. Jede der beiden Komponenten hat also genau einen unendlich langen Ablauf. Die Komposition A|B von A und B ist eine Komponente mit 6 Zuständen. In jedem Zustand beginnen 2 Schritte; damit entstehen unendlich viele unendlich lange Abläufe. Diese Auffassung von Verhalten liegt intuitiv nahe und wird von vielen Analyseverfahren verwendet, insbesondere von Verfahren des Model Checking.

Diese Auffassung hat aber auch Nachteile: Die beiden in einem Zustand beginnenden Schritte sehen aus wie Alternativen; tatsächlich aber treten sie beide unabhängig voneinander ein! Alternativ daran erscheint die – auf Uhren außerhalb des Systems gemessene – zeitliche Reihenfolge der Schritte. [24] diskutiert Einzelheiten derartiger Annahmen über zeitliche Reihenfolgen und benötigt dafür perfekt genau gehende Uhren. Um solche Annahmen zu vermeiden, kann man ausnutzen, dass unabhängige Schritte in disjunkten lokalen Zuständen beginnen und enden. Damit kann man sie als ungeordnet notieren. Ein Ablauf ist dann nicht eine Sequenz, sondern eine Halbordnung von Schritten. Ordnung bezeichnet dann nicht das Voranschreiten in der Zeit, sondern nur einen „Vorher-Nachher“-Zusammenhang. Das System A|B aus Abb. 1 hat in dieser Auffassung dann wiederum nur einen Ablauf, der die beiden Abläufe von A und B vereinigt und dessen Ordnung die Ordnungen der beiden Abläufe vereinigt. Mit der zusätzlichen Forderung, dass B niemals mehr lokale Schritte ausführt als A, hat das System immer noch genau einen Ablauf, den Abb. 2 zeigt. Petrinetze verfolgen diesen Vorschlag mit dem Konzept des „verteilten Ablaufs“ [31].

Einen weiteren Nachteil der Auffassung eines einzelnen Ablaufs eines Systems als eine Sequenz von Schritten verdeutlicht Lamports Beispiel einer Stundenuhr, die von einer vollen Stunde zur nächsten in einem Schritt übergeht. Eine Stunden-und-Minuten-Uhr braucht dafür sechzig Schritte, ist also streng genommen nicht als Stundenuhr verwendbar. Lamport schlägt deshalb in seinem TLA-Formalismus [25] eine Logik vor, die einzelne Schritt konzeptuell logisch mit „beliebig viele Schritte“ gleichsetzt.

Beide Beispiele zeigen, dass die konzeptuelle Auffassung eines einzelnen Ablaufs eines Systems als Sequenz von Schritten unschöne Konsequenzen hat, wenn Systeme komponiert oder verfeinert werden. Deshalb lohnt es sich, unabhängige Ereignisse mit ihren lokalen Ursachen und Wirkungen ernst zu nehmen, und von Nichtdeterminismus zu unterscheiden. Das gilt insbesondere für große Systeme, die ja meistens systematisch als Komposition oder Verfeinerung kleinerer Systeme konstruiert werden. [23] schlägt dafür eine spezifische Logik vor.

Nicht nur Programmiersprachen, sondern auch viele Modellierungssprachen beschreiben Schritte als Wertzuweisung an Variablen. In vielen Fällen ist das angemessen oder zumindest akzeptabel, kann aber auch zu wenig überzeugenden Modellen führen. Ein Beispiel ist das „Pebble Game“, das Dijkstra in einem Video einer anspruchsvollen Serie der Stanford-Universität beschreibt [15]: Eine Urne enthält endlich viele schwarze und weiße Steine. So lange wie möglich werden wiederholt zwei Steine a und b entnommen und ein Stein c zurückgelegt. Dabei ist c weiß, wenn a und b verschieden gefärbt sind, sonst ist c schwarz. Abb. 3 zeigt Dijkstras Modell: ein nichtdeterministisches Programm aus bedingten Wertzuweisungen mit arithmetischen Operationen auf vier Integer-Variablen. Abb. 4 modelliert das Spiel als Petrinetz: PEBBLE ist ein Konstantensymbol, das mit schwarzen und weißen Steinen initialisiert wird. Jede Transition modelliert einen Schritt des Systems, bestehend aus zwei entnommenen und einem zurückgelegten Stein. Die Beschriftung der Pfeile jeder Transition zeigen die Färbung der beteiligten Steine. In diesem Modell wird „entnehmen“ und „zurücklegen“ unmittelbar modelliert. Der Umweg über die Anzahl der beteiligten schwarzen und weißen Steine wird im Modell vermieden. Mit einer Invariante zeigt Dijkstra, dass nach endlich vielen Schritten genau ein Stein übrig bleibt. Der ist genau dann weiß, wenn die Anzahl weißer Steine anfangs ungerade ist. Eine entsprechende Invariante gibt es allerdings auch für das Petrinetz [31].

Variablen und Wertzuweisung sind auch wenig geeignet zur Modellierung verteilter Systeme, Kommunikationsprotokoll, etc. Ein Beispiel ist das TLA-Modell eines asynchronen Interfaces aus [25]. Letztendlich ist dort ein Scheduler nötig, der den Zugriff mehrerer Komponenten auf die gemeinsam benutzten Variablen regelt. Die Komponenten sind also nur unter weitreichenden weiteren Annahmen wirklich verteilt implementierbar.

Eine Theorie der Informatik wird bei der Beschreibung von Schritten nicht nur Wertzuweisung verwenden, sondern eine Vielzahl anderer, ggf. abstrakterer Konzepte. Ein Beispiel sind Petrinetze: Die Bedeutung einer Transition ist gegeben durch die Änderungen der Markierung der Plätze in ihrer unmittelbaren Umgebung.

Neue Systeme können durch Verfeinern und Komponieren gegebener Systeme gebildet werden. Es stellt sich die Frage nach weiteren Methoden zur systematischen Konstruktion neuer Systeme aus gegebenen. Zu den wenigen Vorschlägen dafür gehört die Metapher des 3D-Druckens, sowie die „Living-organism“-Metapher nach [14]. Dort können mehrere „Zellen“ gemeinsam selbstständig „Kreaturen“ bilden, die ganz neue Eigenschaften haben. Generell stellt sich die Frage nach der Grenze solcher Konstruktionen und nach dem „Nichtkonstruierbaren“, in Analogie zur Grenze der Berechenbarkeit bei klassischem Rechnen.

Wissenschaftliche Theorien leben von Modellen, die interessante Konsequenzen zeigen. Ein Modell ist also erst dann wirklich nützlich, wenn man daraus etwas Interessantes ableiten kann. Der rein beschreibende Charakter von UML, BPMN, ASM und anderen Modellierungstechniken ohne spezifische Analyseverfahren schränkt entscheidend ihren Einsatz ein. Ein wirklich gutes Modell eines Systems ist vertrauenswürdig (vgl. Abschn. 3) und zugleich analysierbar, insbesondere mit tiefliegenden Invarianten (vgl. Abschn. 4).

Viele Eigenschaften von Systemen lassen sich zurückführen auf Eigenschaften einzelner Zustände und Abläufe. Zur Beschreibung solcher Eigenschaften hat temporale Logik eine dominante Stellung erreicht [17]; mit Model Checking und abstrakter Interpretation als effizienten Analyseverfahren. Sehr nützlich ist auch die Unterscheidung von Liveness- und Safety-Eigenschaften von Alpern und Schneider.

Eine Theorie der Informatik sollte jedoch wesentlich tiefer liegende Eigenschaften formulieren und nachweisen können, auf der Basis nichttrivialer Invarianten (Abschn. 4) und einem spezifischen Begriff von Informationsfluss (Abschn. 5).

Ein Nutzer eines großen Systems benötigt einen modifizierten Begriff von „Korrektheit“: Ihn interessiert nicht wirklich, ob das ganze System korrekt ist (viele große Systeme sind – für Grenzfälle – ohnehin nicht korrekt), sondern ihn interessiert nur, ob das System für seinen aktuellen Fall korrekte Resultate liefert. Idealerweise liefert ihm das System dafür eine plausible, ihm verständliche Begründung. Klassische Verifikation würde beide Anforderungen verfehlen: Auch ein fehlerhaftes System kann nützlich sein und der Hinweis auf gelungene formale Verifikation einer temporallogisch formulierten Eigenschaft stärkt nicht unbedingt das Vertrauen in die Korrektheit einer einzelnen Nutzung. Erste Vorschläge dazu sind zertifizierende Algorithmen [28] und die Verifikation zur Laufzeit [4]. Eine Theorie der Informatik muss flexible Konzepte zum Begriff der Korrektheit und ihres Nachweises suchen.

Für rechnergestützte Echtzeitsysteme, beispielsweise die Steuerung eines Airbags, sind klassische Echtzeitmodelle angemessen. Viele Modellierungstechniken argumentieren mit einem naiven Zeitbegriff, als sei die jeweils aktuelle Zeit in beliebiger Präzision und ohne zusätzlichen Aufwand verfügbar. Lamport [24] weicht diese Sicht ein wenig auf, ohne sich ganz davon zu lösen. Manche Modellierungstechniken, beispielsweise ESTEL, ESTEREL und Statecharts, verwenden die Hypothese „unendlich schneller“ digitaler Systeme, weil solche Systeme tatsächlich um Größenordnungen schneller als ihre menschlichen Nutzer arbeiten.

Tatsächlich wird „Zeit“ oft verwendet, wo es konzeptionell eher um Ursache-Wirkung-Zusammenhänge geht. „Zeit“ und „Kausalität“ in Systemen, sowie „Beobachtung“ in Modellen sind Begriffe, deren Zusammenhang im Rahmen der Modellbildung der Informatik noch nicht wirklich verstanden ist. Ein herausforderndes Beispiel ist eine formale Beschreibung des Applesort-Algorithmus (vgl. [35]): Äpfel rollen hintereinander über ein schräg gelagertes Brett mit zunehmend größeren Löchern. Jeder Apfel fällt durch das erste Loch, dessen Durchmesser den Durchmesser des Apfels erreicht oder übertrifft. Bei n Löchern klassifiziert dieser Algorithmus die Äpfel in n Größenklassen.

Große Systeme werden in aller Regel aus abstrakten Anforderungen verfeinert oder aus kleineren Systemen zusammengesetzt. Es gibt eine Vielzahl genereller Methoden, Prinzipien und Formalismen (z. B. [3]) zur systematischen Verfeinerung von Spezifikationen. Für logische Spezifikationen fundamental ist das Prinzip der Verfeinerungsimplikation: Die Spezifikation der Verfeinerung impliziert die Spezifikation des gegebenen Systems. Entsprechende Methoden, Prinzipien und Formalismen zur Komposition logischer Spezifikationen wurden für die Sprache Z [34], Lamports TLA [25] und Broys strombasiertes Focus [10] vorgeschlagen, mit dem weitreichenden Vorschlag, Komposition logisch als Konjunktion zu fassen. Auf operationeller Ebene schlägt [32] einen generellen Operator zur Komposition vor, der assoziativ ist und keine Spezifikation des Inneren von Komponenten verlangt. Alle diese Methoden, Prinzipien und Formalismen stellen richtige und wichtige Fragen, haben sich aber nicht wirklich durchgesetzt.

Die Theorie der berechenbaren Funktionen wurde lange als Grundlage einer Theorie der Informatik angesehen. Alle Versuche, die Church-Turing-These zu widerlegen, sind gescheitert. Allerdings wurde diese These oft unzulässig allgemeiner formuliert. Tatsächlich beschreibt sie lediglich einen Sachverhalt zur systematischen Manipulation von Zeichenketten [38]. Informatik und damit eine Theorie der Informatik geht weit über die Manipulation von Zeichenketten hinaus; vielmehr geht es um die Interpretation von Zeichen in der realen Welt. Mit der Manipulation von Zeichenketten werden dann Effekte in der realen Welt beschrieben und erreicht. Diese Zusammenhänge werden in [12] nüchtern dargestellt. In einer Theorie der Informatik hat die Theorie berechenbarer Funktionen einen wichtigen Platz – neben anderen Konzepten. Das gilt entsprechend auch für die formale Logik.

Eine Engineering-Disziplin, beispielsweise Electrical Engineering oder Chemical Engineering, basiert auf einer Wissenschaft (im Beispiel Physik und Chemie), deren Prinzipien, Einsichten, dann für die menschlichen Interessen nutzbar gemacht werden. Software ist aber keine solche Wissenschaft. Software ist das Resultat von Aktivitäten im Rahmen des Software Engineering [7, 9]. Auf welcher Wissenschaft basiert dann das Software Engineering? Man könnte es mit „Algorithmen“ und „Algorithm Engineering“ versuchen, wenn diese Bezeichnung nicht schon für einen engen „Algorithmen“-Begriff stehen würde, und wenn es denn einen hinreichend umfassenden Algorithmenbegriff gäbe. Hierher gehört „Informatik“ als Wissenschaft, als Grundlage verschiedener Engineering-Disziplinen. Eine davon ist dann das „Software Engineering“.

Mit diesem Text möchte ich Interesse wecken am Ziel einer umfassenden Theorie der Informatik. Vorbild einer solchen Theorie ist die Physik. Grundlegende Idee sind Vorschläge für formale Konzepte, die weit über Rechentechnik und Programmierung hinausgehen, mit einem Blickwinkel auch aus den Anwendungen und ihren Grenzen. Der Text gibt einige wenige Anregungen zur Entwicklung einer solchen umfassenden Theorie. Weitere Anregungen finden sich in der einschlägigen Literatur. Durch eine solche Theorie der Informatik werden bisherige Prinzipien der Informatik nicht obsolet; sie können aber besser eingeordnet und aufeinander bezogen werden, zusammen mit zukünftigen Engineering-Konzepten der Informatik.