Hallo Habr. Neulich habe ich nach einer Möglichkeit gesucht, etwas in Idris zu tun, und bin auf einen guten Beitrag gestoßen, dessen kostenlose Übersetzung durchaus angemessen erscheint. Freiheiten und Knebel, wo nötig, werde ich "hier durch solche Kringel am Anfang und am Ende" bezeichnen.
Wann und wann Tests verwenden? Welche Informationen und welche Garantien erhalten wir im Austausch für unsere Bemühungen, sie zu schreiben?
Wir werden uns ein einfaches und leicht erfundenes Beispiel ansehen, das in Python, C, Haskell und Idris ausgedrückt wird. Wir werden auch sehen, was über die Implementierung gesagt werden kann, ohne jeweils zusätzliches Wissen darüber.
Wir werden die verschiedenen Hintertüren nicht berücksichtigen, die es uns ermöglichen, die unsafePerformIO explizit zu verletzen (z. B. C-Erweiterungen, unsafePerformIO in Haskell, unsichere Typkonvertierungen), da sonst keine Schlussfolgerungen gezogen werden können und dieser Beitrag recht kurz ist. "Darüber hinaus verfügt derselbe Haskell über eine Teilmenge von Safe Haskell, die die Verwendung dieser und einer Reihe anderer Tricks, die die Integrität der Sprache verletzen könnten, explizit und transitiv verbietet."
Spezifikation
Lassen Sie eine Liste und eine Bedeutung gegeben werden. Es ist erforderlich, den Index dieses Werts in der Liste zurückzugeben oder anzugeben, dass dieser Wert nicht in der Liste enthalten ist.
Die Implementierung dieser Spezifikation ist trivial, daher ist es selbstverständlich zu fragen, und hier sind im Allgemeinen Tests oder Typen. Diese Eigenschaften und Argumentationsmethoden, über die wir heute sprechen werden, sind jedoch auf einen viel komplexeren Code anwendbar. Lassen Sie die Implementierung zehntausend Zeilen unlesbaren Spaghetti-Codes verwenden, wenn dies hilft, ihre Nützlichkeit zu erkennen.
Python
def x(y, z):
Wir stellen sofort fest, dass wir nicht an den ungeprüften sem- und semantikunabhängigen Eigenschaften eines Programms wie Variablennamen und Textdokumentation interessiert sind. Daher habe ich absichtlich keinen Code geschrieben, der die Wahrnehmung unterstützt. Wir sind nur daran interessiert, dass es vorbehaltlich bestehender Tests und Typprüfungen nicht unwahr sein kann .
Im obigen Code gibt es praktisch keine nützlichen Informationen außer der Tatsache, dass wir eine Funktion haben, die zwei Argumente akzeptiert. Diese Funktion kann ebenso gut den Index des Wertes in der Liste finden oder einen beleidigenden Brief an Ihre Großmutter senden.
Analyse
Wir erhalten nicht nur fragilen Code ohne Tests und Typen, sondern unsere einzige Möglichkeit zu verstehen, was eine Funktion tut, ist die Dokumentation. Und da die Dokumentation von Personen und nicht von Maschinen überprüft wird, kann sie sich leicht als veraltet oder anfangs falsch herausstellen.
- Die Dokumentation
- ✗ Wir kennen das erwartete Verhalten
Über das Verhalten dieser Funktion haben wir nichts zu sagen. Du hasst deine Großmutter. Du bist ein Monster.
- Garantien
- ✓ Speichersicherheit
Python ist eine Garbage Collection-Sprache, die uns dieses Problem beseitigt. "Soweit ich weiß, hindert Sie jedoch nichts daran, unsichere Bibliotheken oder C FFI in diese Funktion zu ziehen."
Python mit Tests
def test_happy_path(): assert x([1, 2, 3], 2) == 1 def test_missing(): assert x([1, 2, 3], 4) is None
Jetzt wissen wir, dass unsere Funktion funktioniert, und wenn das Element fehlt, ist das Ergebnis None ?
Nun ... nein. Dies ist nur ein Beispiel. Leider ist der Umfang unserer Funktion unendlich und keine Anzahl von Beispielen kann die korrekte Funktionsweise unserer Funktion beweisen. Mehr Tests - mehr Vertrauen, aber keine Anzahl von Tests wird alle Zweifel lösen.
Die Möglichkeit, dass diese Funktion None für 4 , aber nicht für 5 zurückgibt, klingt ziemlich verrückt, und in diesem speziellen Fall ist dies höchstwahrscheinlich Unsinn. Wir können mit unserem Glaubensniveau zufrieden sein und uns mit einer bestimmten Anzahl von Beispielen befassen. Aber andererseits wird der Beitrag kurz sein. Stellen wir uns also vor, dass die Implementierung nicht so offensichtlich ist.
Da die Tests im allgemeinen Fall nichts beweisen können, sondern nur das Verhalten anhand spezifischer Beispiele zeigen, können die Tests keine Fehlerfreiheit nachweisen. Zum Beispiel gibt es keinen Test, der zeigen würde, dass unsere Funktion niemals eine Ausnahme auslöst oder niemals in den ewigen Zyklus eintritt oder keine ungültigen Links enthält. Dies kann nur eine statische Analyse sein.
Auch wenn die Beispiele in der Rolle der Beweise nicht sehr gut sind, stellen sie zumindest eine gute Dokumentation dar. Aus diesen beiden Beispielen können wir die vollständige Spezifikation unter einigen zusätzlichen a priori-Annahmen ableiten - diese beiden Beispiele erfüllen beispielsweise auch die „Gegenspezifikation“ „finde das Element im Array und gib das vorherige zurück, falls vorhanden“, für dessen Erfindung ich zehn Sekunden gebraucht habe .
Analyse
Obwohl Tests zeigen können, wie unsere Funktion verwendet wird, und auch ein wenig Sicherheit geben können, dass diese Funktion mit zumindest einigen Beispielen korrekt funktioniert, können sie im allgemeinen Fall nichts über unseren Code beweisen . Dies bedeutet leider, dass Tests nur teilweise dazu beitragen, Fehler zu vermeiden.
- Die Dokumentation
- ✓ Wir haben ein Anwendungsbeispiel
- ✓ Wir kennen einige Werteklassen , die korrekt verarbeitet werden
- ✗ Wir kennen alle Arten von Werten, die korrekt verarbeitet werden
Wir haben keine Einschränkungen hinsichtlich der Argumenttypen. Trotz der Existenz von Beispielen für die Funktionsweise der Funktion wissen wir nicht, welche Typen nicht getestet wurden. - ✗ Wir kennen das erwartete Verhalten
"Der Autor des Originalartikels hat hier angekreuzt. Ich erlaube mir, angesichts des obigen Kommentars ein Kreuz zu setzen."
- Spezifikation
- ✓ Funktioniert in mindestens einem Fall
- ✗ Der zurückgegebene Index ist immer ein gültiger Index
- ✗ Der zurückgegebene Index gibt immer einen geeigneten Wert an
- ✗ Fehlende Elemente geben immer
None / Nothing
- Häufige Fehler
- ✗ Keine Tippfehler oder falschen Namen
Statische Analysen können helfen, aber da Python eine dynamische Sprache ist, die zur Laufzeit verschiedene Dinge überschreiben kann, können wir niemals beweisen, dass es keine Fehler gibt.
Insbesondere kann es sehr schwierig oder unmöglich sein, festzustellen, ob der Methodenname korrekt ist, da die Gültigkeit des Methodenaufrufs vom Laufzeittyp des Objekts abhängt, für das der Aufruf erfolgt. - ✗ Keine unerwartete
null - ✗ Fehlerfälle werden immer behandelt
Nach meiner Erfahrung ist dies eine der häufigsten Fehlerquellen: In unserem Beispiel gibt die Funktion bei fehlendem Element None zurück, aber der Code, der diese Funktion verwendet, kann beispielsweise davon ausgehen, dass immer eine Zahl zurückgegeben wird. Darüber hinaus kann dies auch zu einer nicht behandelten Ausnahme führen.
- Garantien
- ✓ Speichersicherheit
- ✗ Die Funktion kann nicht mit dem falschen Typ aufgerufen werden
- ✗ Keine Nebenwirkungen
- ✗ Keine Ausnahmen
- ✗ Keine Fehler
- ✗ Keine ewigen Zyklen
Haskell
xyz =
Wenn Sie mit der Syntax nicht vertraut sind: Dies ist die Definition einer Funktion x mit den Parametern y und z . In Haskell können Sie Typen weglassen, da diese aus der Implementierung abgeleitet werden (es sei denn, Sie verwenden natürlich andere erweiterte Funktionen als moderne Erweiterungen des Typsystems).
Es scheint, dass dies nicht sehr verschieden von der Python-Version ist, aber nur weil wir unsere Funktion in Haskell geschrieben haben und sie gekachelt ist, können wir bereits über einige interessante Eigenschaften sprechen.
Analyse
Natürlich können wir hier nicht so viele Schlussfolgerungen ziehen, aber hier sind einige Punkte zu beachten:
- Die Dokumentation
- ✗ Wir kennen das erwartete Verhalten
- Häufige Fehler
- ✓ Keine Tippfehler oder falschen Namen
Da Haskell eine kompilierte Sprache ist, müssen alle Namen zur Kompilierungszeit aufgelöst werden. Das Programm wird einfach nicht kompiliert, wenn dieser Fehler auftritt. - ✓ Keine unerwartete
null
Haskell hat einfach keine null . Das Problem ist gelöst!
- Garantien
- ✓ Speichersicherheit
- ✓ Die Funktion kann nicht mit dem falschen Typ aufgerufen werden
- ✓ Keine unerwarteten Nebenwirkungen
⟦Der Autor des Originalartikels hat diesen Artikel nicht angegeben, aber ich erlaube mir zu beachten, dass der abgeleitete Typ dieser Funktion bei Nebenwirkungen auf deren Vorhandensein hinweist, sodass der aufrufende Code über ihre Funktionen informiert ist.⟧
Angabe des Haskell-Typs
x :: Eq a => [a] -> a -> Maybe Int xyz =
Früher haben wir über eine eher vernünftige Haltung gegenüber der Sicherheit von Großmüttern gesprochen: Aus den Tests ging hervor, dass die Funktion niemandem schaden würde, aber war die Großmutter wirklich sicher? Sendet diese Funktion genau keine Schimpfwörter?
Haskell ist bekannt als reine Funktionssprache. Dies bedeutet nicht, dass der Code keine Nebenwirkungen haben kann, aber alle Nebenwirkungen müssen im Typ vorhanden sein. Wir kennen den Typ dieser Funktion und sehen, dass sie sauber ist. Daher sind wir sicher, dass diese Funktion keinen externen Status ändert.
Dies ist aus anderen Gründen eine sehr interessante Eigenschaft: Da wir wissen, dass es keine Nebenwirkungen gibt, können wir die Funktion dieser Funktion nur anhand ihrer Signatur verstehen! Suchen Sie einfach nach dieser Hoogle- Signatur und sehen Sie sich das erste Ergebnis an. Natürlich ist dies nicht die einzig mögliche Funktion, die einen solchen Typ haben würde, aber der Typ gibt uns genug Vertrauen für die Zwecke der Dokumentation.
Analyse
- Die Dokumentation
- ✓ Wir kennen das erwartete Verhalten
- ✗ Wir haben ein Anwendungsbeispiel
- ✓ Wir kennen einige Werteklassen, die korrekt verarbeitet werden
- ✓ Wir kennen alle Arten von Werten, die korrekt verarbeitet werden
- Spezifikation
- ✗ Funktioniert in mindestens einem Fall.
Aufgrund fehlender Tests oder Beweise wissen wir nicht, ob unsere Funktion überhaupt wie erwartet funktioniert! - ✗ Der zurückgegebene Index ist immer ein gültiger Index.
- ✗ Der zurückgegebene Index gibt immer einen geeigneten Wert an.
- ✗ Ein fehlender Artikel gibt immer
None / Nothing .
- Häufige Fehler
- ✓ Keine Tippfehler oder falschen Namen
- ✓ Keine unerwartete
null - ✓ Fehlerfälle werden immer behandelt
Wenn unsere Funktion Nothing zurückgibt, stellt das Typsystem sicher, dass dieser Fall vom aufrufenden Code korrekt behandelt wird. Natürlich kann dieser Fall ignoriert werden, aber dies muss explizit erfolgen.
- Garantien
- ✓ Speichersicherheit
- ✓ Die Funktion kann nicht mit dem falschen Typ aufgerufen werden
- ✓ Keine Nebenwirkungen
- ✗ Keine Ausnahmen
Ich teile Ausnahmen und Fehler, weil ich glaube, dass es nach Ausnahmen möglich ist, sie wiederherzustellen, und nach Fehlern (zum Beispiel teilweise definierten Funktionen) - nein.
Ausnahmen werden größtenteils in Typen beschrieben (z. B. in der E / A-Monade). Auf eine gute Weise sollten wir wissen, dass eine Funktion keine Ausnahme auslöst, sondern nur aufgrund ihres Typs. Haskell bricht diese Erwartung jedoch, indem es zulässt, dass Ausnahmen aus reinem Code ausgelöst werden .
"Darüber hinaus ist anzumerken, dass in Haskell Fehler wie das falsche Aufrufen teilweise definierter Funktionen auch als Ausnahmen dargestellt werden, die abgefangen und verarbeitet werden können, sodass der Unterschied zwischen den beiden Kategorien etwas weniger offensichtlich ist." - ✗ Keine Fehler
Wir können immer noch teilweise definierte Funktionen verwenden, zum Beispiel die Division durch Null. - ✗ Keine ewigen Zyklen
Haskell mit Tests
Denken Sie daran, ich habe vorhin gesagt, dass Tests das Fehlen von Fehlern nicht beweisen können? Ich habe gelogen. Wenn die Sterne richtig konvergieren und die Tests mit Typen kombiniert werden, wird es möglich! Der erste Stern ist die Endlichkeit der Domäne unserer Funktion. Zweitens: Der Definitionsbereich sollte nicht nur endlich, sondern auch nicht sehr groß sein, da sonst ein solcher Test nur schwer in die Praxis umzusetzen ist.
Zum Beispiel:
not :: Bool -> Bool not x = ...
Die Eingabe kann entweder True oder False . Es reicht aus, diese beiden Optionen zu testen, und hier ist es, der Heilige Gral! Keine Ausnahmen, ewige Zyklen, falsche Ergebnisse, keine Fehler. ⟦Für eine etwas komplexere Funktion ist jedoch möglicherweise nicht klar, wie viel Zeit für Tests aufgewendet wird: Wenn die Durchführung lange dauert, sind wir dann in einem ewigen Zyklus gelandet oder ist sie nur schwer? Das Problem, sie aufzuhalten. «
Tatsächlich trifft dies auch bei Haskell nicht ganz zu: In jedem Haskell-Typ gibt es auch einen Wert ⊥ (der als undefined , error oder in gewissem Sinne als unendliche Rekursion erhalten werden kann), aber Haskelisten schließen traditionell ihre Augen und glauben dies es existiert nicht.
Außerschulische Lektüre: Es gibt nur vier Milliarden Schwimmer - testen Sie sie alle!
In unserem ursprünglichen Beispiel ist der Umfang in jedem Fall unendlich, sodass Tests nur zeigen können, dass unser Code für eine begrenzte Anzahl von Beispielen funktioniert.
Analyse
In diesem Fall ergänzen die Tests die Typen und verstopfen einige Löcher im Haskell-Typsystem. Wir haben viel mehr Vertrauen in unseren Code als nur Tests oder Typen.
C.
/* C , int */ int x(int *y, size_t n, int z) { /* 10000 */ }
Wir betrachten C aus Interesse für ältere Systeme. Insbesondere in C werden die Typen höchstwahrscheinlich nicht vom Programmierer, sondern vom Compiler benötigt, um schnelleren Code zu generieren.
In unserem Beispiel wissen wir nicht, was die Funktion zurückgibt, wenn das Element nicht gefunden wird. Wir müssen uns auf Tradition oder Dokumentation verlassen (in diesem Fall kann es beispielsweise -1 ).
Wir könnten auch out-Argumente verwenden: Auf diese Weise können wir einen Fehler zurückgeben und den Rückgabewert in diesem out-Argument speichern. Dies ist eine etwas aussagekräftigere Option, aber wir müssen uns immer noch auf die Dokumentation verlassen, um zu verstehen, welche Parameter gelesen und welche geschrieben werden. In beiden Fällen ist es schwierig, das Verhalten anhand von Typen zu verstehen.
/* , out- */ error_t x(int *y, size_t n, int z, size_t *w) { /* 10000 */ }
Analyse
Das Typensystem selbst gibt uns nicht so viele Garantien. Natürlich erhalten wir einige Informationen von diesen Typen, aber vergleichen Sie sie einfach mit dem Fall Haskell.
Idris
x : Eq x => List x -> x -> Maybe Int xyz = ...
Diese Funktion ist vom gleichen Typ wie im Fall von Haskell. Mit einem ausdrucksstärkeren Typsystem können wir jedoch mehr erreichen. Die Auswahl der Typen kann über die Implementierung sprechen.
%default total x : Eq x => Vect nx -> x -> Maybe (Fin n) xyz = ...
Dieser Typ kann gelesen werden als "Gib mir eine Liste mit der Größe n und einem Wert, und ich werde dir entweder eine Zahl kleiner als n oder Nothing ." Dies stellt sicher, dass die Funktion einen Index zurückgibt, der offensichtlich nicht über die Grenzen hinausgeht.
Außerdem ist diese Funktion total, dh der Timer hat überprüft, dass sie immer endet. Dies eliminiert ewige Zyklen und Fehler.
Analyse
- Spezifikation
- ✗ Funktioniert in mindestens einem Fall.
- ✓ Der zurückgegebene Index ist immer der richtige Index
- ✗ Der zurückgegebene Index gibt immer einen geeigneten Wert an
- ✗ Fehlende Elemente geben immer
None / Nothing
- Garantien
- ✓ Speichersicherheit
- ✓ Die Funktion kann nicht mit dem falschen Typ aufgerufen werden
- ✓ Keine Nebenwirkungen
- ✗ Keine Ausnahmen
- ✓ Keine Fehler
- ✓ Keine ewigen Zyklen
Idris mit Tests
Da die Typensprache von Idris genauso ausdrucksstark ist wie die Sprache seiner Begriffe (oder vielmehr ihr nachweislich vollständiger Teil), ist die Unterscheidung zwischen Test und Typ verschwommen:
ex : x [1, 2, 3] 2 = Just 1 ex = Refl
Diese Funktion hat einen ziemlich seltsamen Typ x [1, 2, 3] 2 = Just 1 . Dieser Typ bedeutet, dass der Typer für eine erfolgreiche Typprüfung nachweisen muss, dass x [1, 2, 3] 2 strukturell gleich Just 1 . ⟦In diesem Fall ist der Beweis trivial, da es für den Kipper ausreicht, die Begriffe auf beiden Seiten des Gleichheitszeichens zu normalisieren, was aufgrund der Gesamtheit aller verwendeten Funktionen in endlicher Zeit erfolgt und aufgrund von Church-Rosser zu einem einzigartigen Ergebnis führt. Danach kann man die Reflexivität der Gleichheit nutzen, was Refl .⟧
Tatsächlich haben wir einen Typ-Level-Test geschrieben.
Idris mit Beweisen
Zur Vollständigkeit der Analyse können wir die volle Leistung abhängiger Typen nutzen und unsere Implementierung beweisen (da abhängige Typen in Idris einem logischen System entsprechen, das konstruktive Logik erster Ordnung enthält).
Insbesondere können wir Eigenschaften nachweisen, die bisher für uns unerreichbar waren:
-- Eq DecEq x : DecEq a => Vect na -> (y : a) -> Maybe (Fin n) xyz = ... -- , `x` findIndexOk : DecEq a => (y : Vect na) -> (z : a) -> case xyz of Just i => index iy = z Nothing => Not (Elem zy) findIndexOk yz = ...
Der Typ findIndexOk kann gelesen werden als „für jeden Typ a so dass er einen algorithmisch entscheidbaren Vergleich ( DecEq ) hat, für jeden Vektor y Elementen vom Typ a beliebiger Länge n und jedem Wert z Typ a : Wenn xyz Index i zurückgibt, dann diesen Index liegt z , aber wenn xyz Nothing zurückgibt, dann gibt es überhaupt kein solches Element im Vektor. “
"Es ist interessant, dass der Autor des Originalartikels einen Typ angibt, der etwas schwächer ist als der oben angegebene."
Jetzt haben wir alles eingefangen! Was sind die Nachteile? Nun, all diese Beweise zu schreiben kann ziemlich schwierig sein.
Vergleich
Meinung
Meiner Meinung nach ist die Verwendung eines modernen Typsystems an sich im Hinblick auf das Verhältnis der erhaltenen Informationen und Garantien für die aufgewendeten Anstrengungen am effektivsten. Wenn Sie ziemlich zuverlässigen Code schreiben möchten, können die Typen mit Tests gewürzt werden. Idealerweise - im Stil von QuickCheck.
Bei abhängigen Typen wird die Grenze zwischen Tests und Typen weniger offensichtlich. Wenn Sie Software für Boeing oder für Herzschrittmacher schreiben, kann es hilfreich sein, Beweise zu schreiben.