Wie können wir die Zuverlässigkeit von Programmen mit probabilistischem Verhalten sicherstellen? Dieses Papier stellt einen Formalismus für die Argumentation über Programme vor, die probabilistisch arbeiten. Es stellt eine grundlegende Programmiersprache mit einem Operator für probabilistische Auswahl vor, begleitet von einer denotationalen Semantik. Standardprädikate der Logik erster Ordnung reichen nicht aus, um Eigenschaften solcher Programme zu spezifizieren, daher wird ein Konzept probabilistischer Prädikate eingeführt. Ein Hoare-ähnliches Beweissystem wird bereitgestellt, um Eigenschaften probabilistischer Programme zu verifizieren. Es wird gezeigt, dass das Beweissystem für eine Untersprache korrekt und vollständig ist. Einige typische Beispiele veranschaulichen die Anwendung probabilistischer Prädikate und des Beweissystems und bieten eine Grundlage für die Verifizierung der Korrektheit probabilistischer Programme.
Diese im International Journal of Foundations of Computer Science veröffentlichte Studie steht im Einklang mit dem Fokus des Journals auf theoretische Informatik und Programmverifikation. Das Papier trägt zu den formalen Methoden zur Analyse von Computersoftware bei, einem Schlüsselbereich innerhalb des Geltungsbereichs des Journals.