Beziehung zwischen Verträgen und abhängiger Eingabe
31
Ich habe einige Artikel über abhängige Typen und Programmierverträge gelesen. Aus der Mehrzahl der von mir gelesenen Artikel geht hervor, dass Verträge dynamisch überprüft werden und abhängige Typen statisch überprüft werden.
Es gab einige Papiere, die mich glauben ließen, dass es möglich ist, Verträge zu haben, die teilweise statisch überprüft werden:
Damit scheint es eine erhebliche Überschneidung zu geben, und meine Kategorisierung von Verträgen gegenüber abhängigen Typen verschwindet allmählich.
Gibt es etwas Tieferes in beiden Konzepten, das mir fehlt? Oder sind dies wirklich nur unscharfe Kategorien, die dasselbe zugrunde liegende Konzept darstellen?
Verträge sind auf praktischer Ebene Behauptungen. Mit ihnen können Sie die (quantifiziererfreien) Eigenschaften einzelner Programmausführungen überprüfen. Die Schlüsselidee bei der Vertragskontrolle ist die Idee der Schuld - im Grunde wollen Sie wissen, wer für eine Vertragsverletzung verantwortlich ist. Dies kann entweder eine Implementierung sein (die den versprochenen Wert nicht berechnet) oder der Aufrufer (der einer Funktion den falschen Wert übergeben hat).
Die entscheidende Erkenntnis ist, dass Sie die Schuld mit der gleichen Maschinerie verfolgen können wie die Einbettung von Projektionspaaren in die inverse Grenzwertkonstruktion der Domänentheorie. Grundsätzlich wechseln Sie von der Arbeit mit Zusicherungen zur Arbeit mit Paaren von Zusicherungen, von denen eine den Programmkontext und die andere das Programm beschuldigt. Auf diese Weise können Sie Funktionen höherer Ordnung in Kontrakte einschließen, da Sie die Kontravarianz des Funktionsbereichs modellieren können, indem Sie das Assertionspaar austauschen. (Siehe zum Beispiel Nick Bentons Artikel "Undoing Dynamic Typing" .)
Abhängige Typen sind Typen. Typen geben Regeln an, nach denen festgestellt werden kann, ob bestimmte Programme zulässig sind oder nicht. Infolgedessen schließen sie Dinge wie den Begriff der Schuld nicht ein, da ihre Funktion darin besteht, die Existenz von Programmen, die sich schlecht benehmen, an erster Stelle zu verhindern. Es gibt nichts zu bemängeln, da nur wohlgeformte Programme auch grammatikalische Äußerungen sind. Pragmatisch bedeutet dies, dass es sehr einfach ist, abhängige Typen zu verwenden, um über Eigenschaften von Termen mit Quantifizierern zu sprechen (z. B. dass eine Funktion für alle Eingaben funktioniert).
Diese beiden Ansichten sind nicht gleich, aber sie hängen zusammen. Grundsätzlich geht es darum, dass wir bei Verträgen mit einem universellen Wertebereich beginnen und Verträge verwenden, um Dinge zu reduzieren. Wenn wir jedoch Typen verwenden, versuchen wir, kleinere Wertebereiche (mit einer gewünschten Eigenschaft) im Voraus anzugeben. So können wir die beiden über typgesteuerte Beziehungsfamilien (dh logische Beziehungen) verbinden. Siehe zum Beispiel Ahmed, Findler, Siek und Wadlers jüngstes "Blame for All" oder Reynolds "The Meaning of Types: from Intrinsic to Extrinsic Semantics" .
Warum sind Verträge Ihrer Meinung nach quantifiziererfrei?
Radu GRIGore
3
Da Sie im Allgemeinen keine Tests verwenden können, um allgemein quantifizierte Eigenschaften von Funktionen zu ermitteln, ist dies alles.
Neel Krishnaswami
3
Sofern sich die Quantifizierer nicht über endliche Bereiche erstrecken, können sie in diesem Fall als große Konjunktionen und Disjunktionen angesehen werden. Wenn Sie Lust auf etwas haben, können Sie bestimmte Arten quantifizierter Aussagen überprüfen, vorausgesetzt, die Quantifizierer liegen über den durchsuchbaren Typen von Martin Escardo (die unendlich sein können).
Andrej Bauer
2
@Radu: Ich bezeichne Dinge wie JML & Co als "Programmlogik". Die Behauptungssprachen der Programmlogik sind nicht darauf beschränkt, Ausdrücke aus der Sprache der Programme zu sein. Auf diese Weise können Sie Dinge wie nicht abschließende oder nebenwirkende Behauptungen ausschließen, die keine gute logische Interpretation haben. (Solche Dinge sind jedoch für die Vertragskontrolle von Bedeutung - siehe Pucellas und Toves jüngste Arbeiten bei ESOP zur Verwendung zustandsbehafteter, zwingender Verträge zur Verfolgung von Linearitätseigenschaften.)
Das (ziemlich abstrakte) Problem, das sowohl Typen als auch Verträge angreifen, ist "Wie kann sichergestellt werden, dass Programme bestimmte Eigenschaften haben?". Hier besteht eine inhärente Spannung zwischen der Möglichkeit, eine breitere Klasse von Eigenschaften auszudrücken und zu überprüfen, ob ein Programm eine Eigenschaft hat oder nicht. Typensysteme stellen normalerweise eine sehr spezifische Eigenschaft sicher (das Programm stürzt niemals auf bestimmte Weise ab) und verfügen über einen Typprüfalgorithmus. Auf der anderen Seite können Sie mit Verträgen eine Vielzahl von Eigenschaften angeben (z. B. ist die Ausgabe dieses Programms eine Primzahl), haben aber keinen Überprüfungsalgorithmus.
Die Tatsache, dass es keinen Vertragsüberprüfungsalgorithmus gibt (der immer funktioniert), bedeutet jedoch nicht, dass es fast keine Vertragsüberprüfungsalgorithmen gibt (die in der Praxis in der Regel funktionieren). Ich würde empfehlen, sich Spec # und das Jessie-Plugin von Frama-C anzuschauen . Sie arbeiten beide, indem sie "Dieses Programm hält sich an diesen Vertrag" als eine Aussage in der Logik erster Ordnung über die Generierung von Überprüfungsbedingungen ausdrücken und dann eine SMT fragenversuchen, einen Beweis zu finden. Wenn der Löser keinen Beweis findet, ist entweder das Programm falsch oder der Löser hat keinen existierenden Beweis gefunden. (Aus diesem Grund handelt es sich um einen "Fast" -Vertragsprüfungsalgorithmus.) Es gibt auch Tools, die auf symbolischer Ausführung basieren. Dies bedeutet ungefähr, dass "dieses Programm diesem Vertrag gehorcht" als eine Reihe von Aussagen (in gewisser Logik) ausgedrückt wird. Siehe zum Beispiel jStar .
Flanagans Arbeit versucht, das Beste aus beiden Welten herauszuholen, so dass Sie schnell typähnliche Eigenschaften überprüfen und den Rest erledigen können. Ich kenne mich mit Hybridtypen nicht wirklich aus, erinnere mich aber an den Autor, der gesagt hat, dass er motiviert war, eine Lösung zu finden, die weniger Anmerkungen erfordert (als seine vorherige Arbeit mit ESC / Java). In gewisser Weise gibt es jedoch auch in ESC / Java (und Spec #) eine lose Integration zwischen Typen und Verträgen: Beim Prüfen von Verträgen wird dem Solver mitgeteilt, dass die Typprüfung erfolgreich war, damit er diese Informationen erkennen kann.
Verträge können statisch überprüft werden. Wenn Sie sich Dana Xus alte Arbeit über ESC / Haskell ansehen , war sie in der Lage, zur Kompilierungszeit eine vollständige Vertragsprüfung durchzuführen, wobei sie sich nur auf einen Theorembeweiser für die Arithmetik stützte. Die Beendigung wird durch eine einfache Tiefenbeschränkung gelöst, wenn ich mich richtig erinnere:
Sowohl Verträge als auch Typen ermöglichen es Ihnen, Spezifikationen für Funktionen im Hoare-Stil (vor / nach der Bedingung) darzustellen. Beide können entweder statisch zur Kompilierungszeit oder dynamisch zur Laufzeit überprüft werden.
Mit abhängigen Typen können Sie eine Vielzahl von Eigenschaften im Typsystem codieren, die von Vertragsprogrammierern erwartet werden. Dies liegt daran, dass sie von den Werten des Typs abhängen können . Abhängige Typen neigen dazu, statisch überprüft zu werden, obwohl ich der Meinung bin, dass die von Ihnen zitierten Papiere alternative Ansätze betrachten.
Letztendlich gibt es kaum einen Unterschied. Ich denke, es ist mehr so, dass abhängige Typen eine Logik sind, in der Sie Spezifikationen ausdrücken können, während Verträge eine Programmiermethode sind, in der Sie Spezifikationen ausdrücken.
Es ist etwas irreführend zu sagen, dass Anmerkungen im Hoare-Stil statisch überprüft werden können. Wenn die Logik FO ist, wie es normalerweise ist, dann ist das Problem sicherlich nicht zu entscheiden. Aber ja, ich weiß, Sie meinten, dass man in vielen Situationen versuchen und sogar erfolgreich sein kann.
Radu GRIGore
1
Ich hatte den Eindruck, dass die Erstellung des Proofs unabdingbar sein mag, aber die Überprüfung eines Proofs sollte es sein. Viele abhängig typisierte Sprachen verlassen sich darauf, dass der Benutzer den Beweiswert für die Besiedlung des Satztyps liefert.
Jason Reich
Du hast recht. Aber ich lebe in einer automatisierten Welt, in der der Benutzer normalerweise nicht nach einem Beweis gefragt wird.
Das (ziemlich abstrakte) Problem, das sowohl Typen als auch Verträge angreifen, ist "Wie kann sichergestellt werden, dass Programme bestimmte Eigenschaften haben?". Hier besteht eine inhärente Spannung zwischen der Möglichkeit, eine breitere Klasse von Eigenschaften auszudrücken und zu überprüfen, ob ein Programm eine Eigenschaft hat oder nicht. Typensysteme stellen normalerweise eine sehr spezifische Eigenschaft sicher (das Programm stürzt niemals auf bestimmte Weise ab) und verfügen über einen Typprüfalgorithmus. Auf der anderen Seite können Sie mit Verträgen eine Vielzahl von Eigenschaften angeben (z. B. ist die Ausgabe dieses Programms eine Primzahl), haben aber keinen Überprüfungsalgorithmus.
Die Tatsache, dass es keinen Vertragsüberprüfungsalgorithmus gibt (der immer funktioniert), bedeutet jedoch nicht, dass es fast keine Vertragsüberprüfungsalgorithmen gibt (die in der Praxis in der Regel funktionieren). Ich würde empfehlen, sich Spec # und das Jessie-Plugin von Frama-C anzuschauen . Sie arbeiten beide, indem sie "Dieses Programm hält sich an diesen Vertrag" als eine Aussage in der Logik erster Ordnung über die Generierung von Überprüfungsbedingungen ausdrücken und dann eine SMT fragenversuchen, einen Beweis zu finden. Wenn der Löser keinen Beweis findet, ist entweder das Programm falsch oder der Löser hat keinen existierenden Beweis gefunden. (Aus diesem Grund handelt es sich um einen "Fast" -Vertragsprüfungsalgorithmus.) Es gibt auch Tools, die auf symbolischer Ausführung basieren. Dies bedeutet ungefähr, dass "dieses Programm diesem Vertrag gehorcht" als eine Reihe von Aussagen (in gewisser Logik) ausgedrückt wird. Siehe zum Beispiel jStar .
Flanagans Arbeit versucht, das Beste aus beiden Welten herauszuholen, so dass Sie schnell typähnliche Eigenschaften überprüfen und den Rest erledigen können. Ich kenne mich mit Hybridtypen nicht wirklich aus, erinnere mich aber an den Autor, der gesagt hat, dass er motiviert war, eine Lösung zu finden, die weniger Anmerkungen erfordert (als seine vorherige Arbeit mit ESC / Java). In gewisser Weise gibt es jedoch auch in ESC / Java (und Spec #) eine lose Integration zwischen Typen und Verträgen: Beim Prüfen von Verträgen wird dem Solver mitgeteilt, dass die Typprüfung erfolgreich war, damit er diese Informationen erkennen kann.
quelle
Verträge können statisch überprüft werden. Wenn Sie sich Dana Xus alte Arbeit über ESC / Haskell ansehen , war sie in der Lage, zur Kompilierungszeit eine vollständige Vertragsprüfung durchzuführen, wobei sie sich nur auf einen Theorembeweiser für die Arithmetik stützte. Die Beendigung wird durch eine einfache Tiefenbeschränkung gelöst, wenn ich mich richtig erinnere:
quelle
Sowohl Verträge als auch Typen ermöglichen es Ihnen, Spezifikationen für Funktionen im Hoare-Stil (vor / nach der Bedingung) darzustellen. Beide können entweder statisch zur Kompilierungszeit oder dynamisch zur Laufzeit überprüft werden.
Mit abhängigen Typen können Sie eine Vielzahl von Eigenschaften im Typsystem codieren, die von Vertragsprogrammierern erwartet werden. Dies liegt daran, dass sie von den Werten des Typs abhängen können . Abhängige Typen neigen dazu, statisch überprüft zu werden, obwohl ich der Meinung bin, dass die von Ihnen zitierten Papiere alternative Ansätze betrachten.
Letztendlich gibt es kaum einen Unterschied. Ich denke, es ist mehr so, dass abhängige Typen eine Logik sind, in der Sie Spezifikationen ausdrücken können, während Verträge eine Programmiermethode sind, in der Sie Spezifikationen ausdrücken.
quelle