Rechenhärte von „echten“ Computerprogrammen

Ich habe oft gehört, dass man aufgrund des Satzes von Rice kein Programm schreiben kann, um Fehler in einem Webbrowser, einem Textverarbeitungsprogramm oder einem Betriebssystem zu erkennen: Jede semantische Eigenschaft für eine Turing-vollständige Sprache ist unentscheidbar.

Ich bin mir jedoch nicht sicher, inwieweit dies für reale Programme wie Betriebssysteme gilt. Benötigen diese Arten von Programmen die volle Stärke der Vollständigkeit von Turing? Gibt es einfachere Berechnungsmodelle (wie PR), in die diese Anwendungen geschrieben werden könnten? Wenn ja, inwieweit ermöglicht dies die Entscheidbarkeit der Programmkorrektheit?

Sie sicherlich können Programme schreiben , die fangen Bugs - es ist eine große und aktive Community von Menschen , die Programme schreiben , genau das zu tun. Der Satz von Rice hindert Sie jedoch daran, Fehlerfänger zu schreiben, die sowohl solide als auch vollständig sind (dh alle Fehler einer bestimmten Klasse ohne falsch positive Ergebnisse abzufangen).

Naive Einschränkungen des Rechenmodells helfen Ihnen jedoch nicht sehr dabei, die Praktikabilität der Programmanalyse zu verbessern. Der Grund ist, dass Sie Programme erhalten können, die "fast das Gleiche" tun, indem Sie while-Schleifen drehen

while P do 
   C

in for-Schleifen mit einer großen Iterationskonstante:

for i = 0 to BIGNUM do 
  if P then 
    C
  else
    break

Jetzt benötigt dieses Programm nicht einmal die volle Stärke der primitiven Rekursion (da die for-Schleife zu einer riesigen verschachtelten if-then-else-Anweisung makroerweitert werden kann), aber in den meisten praktischen Fällen verhält es sich genauso wie zuvor. Beachten Sie, dass dies theoretisch zur Entscheidungsfähigkeit beiträgt - das Programm ist vollständig, sodass Sie Fragen beantworten können, indem Sie das Programm ausführen und sehen, was passiert. Dies ist nicht das, was wir eigentlich wollen, nämlich Antworten schneller als das Ausführen des Programms zu erhalten - die eingeführte künstliche Beendigung hilft der Programmanalyse in der Praxis nicht wirklich, da Fehler aufgrund von Fehlern in der realen Programmlogik auftreten und wir haben ' Ich habe das überhaupt nicht berührt.

Darüber hinaus kann das Hinzufügen von Abstraktionsfunktionen zu einer Programmiersprache die Komplexität des Analyseproblems radikal verschlechtern und gleichzeitig die Überprüfung von Programmen in der Praxis erleichtern. Zum Beispiel erfordert der Nachweis der Beendigung des einfach typisierten Lambda-Kalküls mit natürlichen Zahlen eine Induktion bis zu . Durch Hinzufügen eines Typpolymorphismus erhalten Sie jedoch System F, dessen Abschlussbeweis so stark ist wie die Konsistenz der Arithmetik zweiter Ordnung. In der Praxis sind in F geschriebene Programme jedoch viel einfacher zu überprüfen, da die Modularitätseigenschaften der Quantifizierung zweiter Ordnung das Schreiben strukturierter Programme und Korrektheitsnachweise erheblich erleichtern.$\epsilon_0$

Da Sie nach der Programmkorrektheit von Programmen der realen Welt wie Betriebssystemen gefragt haben, könnte Sie das Projekt seL4 ( Journal , PDF , Konferenz ) interessieren .

Das NICTA-Team nahm einen Mikrokernel der dritten Generation mit 8700 C-Zeilen und 600 Assembler-Zeilen, die gemäß einer abstrakten Spezifikation in Haskell implementiert wurden. Sie lieferten einen formellen, maschinengeprüften Nachweis (in Isabelle / HOL), dass die Implementierung genau der Spezifikation entspricht. Dies beweist, dass ihr Programm fehlerfrei ist.

Genau wie das Problem des Anhaltens kann es, obwohl es im Allgemeinen nicht gelöst werden kann, für bestimmte Fälle gelöst werden. In diesem Fall können Sie zwar nicht beweisen, dass beliebiger C-Code fehlerfrei ist, dies könnte jedoch im Fall des seL4-Mikrokerns der Fall sein.

Die Fragen, die Sie stellen, sind tatsächlich ganz anders.

Ich bin mir jedoch nicht sicher, inwieweit dies für reale Programme wie Betriebssysteme gilt. Benötigen diese Arten von Programmen die volle Stärke der Vollständigkeit von Turing?

Es dauert äußerst wenig, bis ein Berechnungsmodell vollständig ist. Beispielsweise können verschiedene Modelle mit Zählern Turingmaschinen simulieren. Wenn Sie der Meinung sind, dass Ihre Software mehr als zwei Zähler benötigt, die Sie beliebig manipulieren können, verwenden Sie eine vollständige Turing-Sprache. Obwohl Maschinen-Ganzzahlen apriori-begrenzt sind, sind dies bei Heap-zugewiesenen Datenstrukturen normalerweise nicht der Fall. Wenn Ihre Software Listen, Bäume und andere dynamisch zugewiesene Daten benötigt, verwenden Sie eine vollständige Turing-Sprache.

Gibt es einfachere Berechnungsmodelle (wie PR), in die diese Anwendungen geschrieben werden könnten? Wenn ja, inwieweit ermöglicht dies die Entscheidbarkeit der Programmkorrektheit?

Es ist wichtig zu wissen, dass wir keine willkürlichen Eigenschaften unserer Software überprüfen möchten. Das Überprüfen sehr spezifischer, enger Eigenschaften (keine Pufferüberläufe, keine Nullzeiger-Dereferenzen, keine Endlosschleifen usw.) verbessert die Qualität und Benutzerfreundlichkeit von Software erheblich. Theoretisch sind solche Probleme immer noch unentscheidbar. In der Praxis können wir durch die Konzentration auf bestimmte Eigenschaften Strukturen in unseren Programmen entdecken, die wir häufig zur Lösung des Problems nutzen können.

Insbesondere können Sie Ihre ursprüngliche Frage in ändern

Gibt es eine Abstraktion meiner Software, die ich in einem nicht Turing-vollständigen Modell effizient analysieren kann?

Eine Abstraktion ist ein Modell, das das Verhalten der ursprünglichen Software und möglicherweise viele zusätzliche Verhaltensweisen umfasst. Es gibt Modelle wie Einzählermaschinen oder Pushdown-Systeme, die nicht vollständig sind und die wir analysieren können. Der Standardansatz bei der Programmüberprüfung mit automatisierten Tools besteht darin, eine Abstraktion in einem solchen Modell zu erstellen und algorithmisch zu überprüfen.

Es gibt Anwendungen, bei denen sich Menschen für anspruchsvolle Eigenschaften ihrer Hardware oder Software interessieren. Hardware-Unternehmen möchten, dass ihre Chips arithmetische Algorithmen korrekt implementieren, Automobil- und Avionikunternehmen möchten zertifizierbar korrekte Software. Wenn es so wichtig ist, ist es besser, einen (geschulten) Menschen zu benutzen.