# Fehlerfreie Software - gibts das?

## Mr. Anderson

*edit* -- think4urs11: Diskussion abgetrennt aus Hat jemand erfahrung mit XFS?

 *firefly wrote:*   

> Denn eine Software ist zu keinem Zeitpunkt 100%ig fehlerfrei.

 

Stooop. Solche Software ist extrem selten, aber es gibt sie. Hurd ist so ein Versuch.  :Wink: 

----------

## firefly

 *Mr. Anderson wrote:*   

>  *firefly wrote:*   Denn eine Software ist zu keinem Zeitpunkt 100%ig fehlerfrei. 
> 
> Stooop. Solche Software ist extrem selten, aber es gibt sie. Hurd ist so ein Versuch. 

 

Na klar und wie wollen die das beweisen? Denn der Testaufwand dafür ist so groß, das du selbst nach 1Millionen Jahren des Testens nicht sicher sein kannst, alle fehler gefunden zu haben  :Smile: .

Ich gebe dazu mal ein Beispiel:

Wir haben folgenden Codeauszug:

```
A

while (x1 > 0) {

    if (x2 == 0) {

        B

    } else if (x2 == 1) {

        C

    } else if (x2 == 2) {

        D

    } else {

        E

    }

    F

    G

    if (x3 == 1) {

        if (x4 > 0) {

            H

        }

    } else {

        if (x5 == 1) {

            I

        } else {

            J

        }

    }

}
```

A - J sind irgentwelche anweisunge, die ausgeführt werden.

Für die paar zeilen Code sind für den Boundary - Interior Pfadtest 273 Testfälle notwendig.

Der Boundary - Interior Pfadtest ist eine Test-Methode, bei der zum einen alle Pfade eines Programms geprüft werden müssen. Desweiteren müssen Schleifen einmal umgangen werden , einmal durchlaufen und dann noch 2 mal durchlaufen werden. Zur Berechnung der mindestens notwendigen Testfälle gibt es diese Formel: 

```
a^0 + a^1 + a^2
```

 wobei a = die anzahl der Pfade innerhalb der Schleife darstellt.

a^0 entpricht, daß die Schleife umgangen wird

a^1 entspricht, daß die Schleife nur einmal durchlaufen wird

a^2 entspricht, daß die Schleife 2 mal durchlaufen wird

Beim obigen Beispiel gibt es innerhalb der Schleife 16 Pfade. Wenn man das jetzt in die obige Formel einsetzt ergibt das dann:

```
16^0 + 16^1 + 16^2 = 1+16+256 = 273
```

Da bei diesem relativ simplen Code soviele Testfälle notwendig sind kannst du dir selbst ausrechnen wieviel Testfälle notwendig wären um z.b. den Kernel mit dem Boundary-Interior Pfadtest zu testen.

----------

## Mr. Anderson

 *firefly wrote:*   

>  *Mr. Anderson wrote:*    *firefly wrote:*   Denn eine Software ist zu keinem Zeitpunkt 100%ig fehlerfrei. 
> 
> Stooop. Solche Software ist extrem selten, aber es gibt sie. Hurd ist so ein Versuch.  
> 
> Na klar und wie wollen die das beweisen? Denn der Testaufwand dafür ist so groß, das du selbst nach 1Millionen Jahren des Testens nicht sicher sein kannst, alle fehler gefunden zu haben .

 

Habe ich geschrieben, dass das automatisiert gehen muss? Wozu hat man einen Kopf? Zettel, Stift und viel Mathematik lautet die Devise. Voraussetzung dafür sind natürlich abolut exakte Ein- und Ausgabespezifikationen praktisch für jede Funktion - und da fällt schon fast 100% aller Software durch.

----------

## oscarwild

 *Mr. Anderson wrote:*   

> Habe ich geschrieben, dass das automatisiert gehen muss?

 

Nichtautomatisiertes Testen ist fehlerträchtig, ungenau, und für Regressionstests unbrauchbar.

 *Mr. Anderson wrote:*   

> Voraussetzung dafür sind natürlich abolut exakte Ein- und Ausgabespezifikationen praktisch für jede Funktion.

 

Was die Voraussetzung für einen Blaxbox-Test wäre, der keinesfalls ausreichend ist.

----------

## firefly

 *Mr. Anderson wrote:*   

>  *firefly wrote:*    *Mr. Anderson wrote:*    *firefly wrote:*   Denn eine Software ist zu keinem Zeitpunkt 100%ig fehlerfrei. 
> 
> Stooop. Solche Software ist extrem selten, aber es gibt sie. Hurd ist so ein Versuch.  
> 
> Na klar und wie wollen die das beweisen? Denn der Testaufwand dafür ist so groß, das du selbst nach 1Millionen Jahren des Testens nicht sicher sein kannst, alle fehler gefunden zu haben . 
> ...

 

Ähm wo habe ich gesagt, das es automatisch laufen soll?

----------

## Mr. Anderson

 *oscarwild wrote:*   

>  *Mr. Anderson wrote:*   Habe ich geschrieben, dass das automatisiert gehen muss? 
> 
> Nichtautomatisiertes Testen ist fehlerträchtig, ungenau, und für Regressionstests unbrauchbar.

 

Und automatisiertes Testen ist weniger fehlerträchtig? Mal davon abgesehen, dass man Korrektheit nicht automatisiert nachweisen kann.

 *oscarwild wrote:*   

>  *Mr. Anderson wrote:*   Voraussetzung dafür sind natürlich abolut exakte Ein- und Ausgabespezifikationen praktisch für jede Funktion. 
> 
> Was die Voraussetzung für einen Blaxbox-Test wäre, der keinesfalls ausreichend ist.

 

Blackbox-Test... ich red nicht davon, Werte reinzuschicken und zu schauen, was rauskommt, sondern davon, sich den Code anzusehen.

 *firefly wrote:*   

> Ähm wo habe ich gesagt, das es automatisch laufen soll?

 

Was willst Du sonst mit dem "Boundary - Interior Pfadtest"? Von Hand einsetzen?

----------

## firefly

ach ja und du meinst, wenn du alles manuell machst, das du dann jeden fehler finden wirst?

Träum weiter.

Zum einen hast du überhaupt nicht die Zeit dafür bei jeder Softwareänderung die ganzen Tests von hand nochmal  durchzugehen.

Desweiteren hast du mit deiner Aussage:

 *Quote:*   

> Voraussetzung dafür sind natürlich abolut exakte Ein- und Ausgabespezifikationen praktisch für jede Funktion 

 

von einem Blackbox-test geredet, auch wenn du was anderes gemeint haben magst.

----------

## think4urs11

Der Thread gleitet langsam sehr weit in [OT]-Gewässer, das Thema war mal 'Erfahrungen mit XFS', dies nur mal so am Rande  :Smile: 

----------

## Mr. Anderson

 *firefly wrote:*   

> ach ja und du meinst, wenn du alles manuell machst, das du dann jeden fehler finden wirst?
> 
> Träum weiter.
> 
> Zum einen hast du überhaupt nicht die Zeit dafür bei jeder Softwareänderung die ganzen Tests von hand nochmal  durchzugehen.
> ...

 

Nein, ich werde jetzt nicht weiter darüber diskutieren. Wir sind nämlich wirklich vollkommen OT.

----------

## oscarwild

 *Mr. Anderson wrote:*   

> Und automatisiertes Testen ist weniger fehlerträchtig?

 

So isses. Ein Testscript wird Testfälle deutlich präziser widerholen als ein Mensch, der an einem Tag eine Kanne Kaffee getankt hat, am anderen Tag nach einem durchzechten Wochenende neben dem Testen mit der Mieze auf seinem Schädel kämpft.  :Laughing: 

 *Mr. Anderson wrote:*   

> Mal davon abgesehen, dass man Korrektheit nicht automatisiert nachweisen kann.

 

Stimmt. Davon abgesehen kann Korrektheit von Software überhaupt nicht nachgewiesen werden. Wenn man sich dazu mal jemanden anhört, der sich mit sowas auskennt:

 *Glenford J. Myers wrote:*   

> Testen ist der Prozeß, ein Softwaresystem anzuwenden/auszuführen mit der Absicht, Fehler zu finden.

 

 *Mr. Anderson wrote:*   

> ich red nicht davon, Werte reinzuschicken und zu schauen, was rauskommt, sondern davon, sich den Code anzusehen.

 

Achso, einfach mal drüberschauen und die Modulspec danebenlegen als die Ultimative Testmethode (TM). Na da wünsch ich dann mal viel Spaß mit dem fehlerfreien Produkt  :Laughing: 

Ich kann Dir wirklich nur versichern, dass man mit statischen/strukturellen Tests einiges finden, aber dynamische Tests damit keinesfalls ersetzen kann.

In einem früheren Beitrag hast Du vom Einsatz von "viel Mathematik" gesprochen. Gut und recht - das wird in der Avionik praktiziert, für hochkritische Systeme bzw. Teilsysteme. Der Aufwand ist ENORM, der Ansatz erfordert eine formale Spezifikation (nicht textuell), und klappt nur, wenn das zugrundelegende Modell korrekt ist (vgl.: Die Annahme, die Erde sei eine flache Scheibe kann zu unerwarteten Ergebnissen führen, wenn man größere  Distanzen zurücklegt  :Wink: ). 

Im weiteren verweise ich auf den Gödelschen Unvollständigkeitssatz  :Laughing: 

Bogen zurück zu den Filesystemen: ich hoffe, wir sind uns einigermaßen einige, dass man fehlerfreie Software (abgesehen von Hallo-Welt "Programmen") etwa so häufig findet wie die Nadel im Heuhaufen. Das gilt auch für Dateisysteme, sowohl für ext2/3/4/viele als auch für xfs, jfs etc.

Zumindest bei reiser3 haben genug Leute Schiffbruch erlitten, daher würde ich resier3 nicht auf kritischen Systemen einsetzen. XFS ist gut und recht für dicke Server mit SEHR großen Dateien, erprobter ist aber ext3.

Ich habe mehrere Dateisysteme ausprobiert, und komme zu dem Schluss, dass xfs für meinen Anwendungszweck keinen Nutzen bringt, beim Risiko eines konzeptbedingten Datenverlusts bei Stromausfall, als auch durch evtl. vorhandene Bugs, deren Wahrscheinlichkeit bei XFS einfach höher ist als bei ext3.

----------

## Mr. Anderson

 *Quote:*   

> Im weiteren verweise ich auf den Gödelschen Unvollständigkeitssatz 

 

Dann schreib ich halt doch noch mal den einen oder anderen Satz dazu. Der Gödelsche Satz ist mir bekannt und der Aufwand, Software wirklich zu beweisen ist enorm, das ist absolut korrekt - aber in einem gewissen Rahmen ist es möglich. Einerseits sind Computer endliche Systeme, andererseits kann man Algorithmen und Programmiersprache geschickt wählen. Afaik wurde z. B. die Korrektheit von mindestens einem ABS-System vollständig bewiesen.

Und um den Dateisystemen zurückzukommen: Ich denke, es ist möglich, auch ein vollständig bewiesenes Dateisystem zu bauen, auch wenn die Entwicklung wahrscheinlich aufwändiger wäre als sämtliche von Linux unterstützten Dateisysteme noch mal neu zu schreiben.

 *Quote:*   

> Bogen zurück zu den Filesystemen: ich hoffe, wir sind uns einigermaßen einige, dass man fehlerfreie Software (abgesehen von Hallo-Welt "Programmen") etwa so häufig findet wie die Nadel im Heuhaufen.

 

Ist es wirklich so viel? ^^

----------

## oscarwild

 *Mr. Anderson wrote:*   

> Einerseits sind Computer endliche Systeme

 

Die Hardware schon, die Software jedoch nicht!

 *Mr. Anderson wrote:*   

> Ist es wirklich so viel? ^^

 

Kommt auf den Heuhaufen an  :Wink: 

----------

## schmutzfinger

Also ein Mensch kann wohl niemals heutige Software überblicken und alle Fehler finden. Ein automatisierter Tester kanns probieren aber das Problem ist das so ein Tester auch getestet sein müsste und dessen Tester dann auch ....

Funktionalität kann man gut automatisch testen aber Sicherheitslücken kann man damit nur sehr begrenzt finden.

Ich denke es gibt keine fehlerfreie Software. Und selbst wenn es die gäbe würde sie mit hoher Sicherheit auf fehlerhafter Hardware laufen, die vielleicht mit fehlerhafter Software entworfen wurde  :Wink: .

----------

## blu3bird

Natürlich gibt es fehlerfreie Software, wer's nicht glaub, hier 2 Beispiel:

```
true
```

```
false
```

Die Frage ob es fehlerfreie Software mit mehr als 2000 Zeilen Code gibt...solange sie von Menschen programmiert wird nicht.  :Wink: 

----------

## schmutzfinger

Mhh dumm das man für deine "fehlerfreie" Software noch nen compiler/Interpreter und libs braucht. Der Code mag correct aussehen aber was macht der Compiler draus?

----------

## Knieper

Hehe - da Treffen die Praktiker auf die Theoretiker. Es gibt durchaus 100% fehlerfreie Software. "Fehlerfrei" insofern, dass Sie ein 100%iges Modell der Spezifikation ist. Allerdings muss dann auch die Spezifikation stimmen und die nimmt erfahrungsgemaess 1/3 des Umfangs des fertigen Programms an. Fuer Teile von Kommunikationsanlagen, Teile von Betriebssystemen (zB. VFiasco), Steuerungssoftware etc. wurde das schon gemacht. Natuerlich ist es ein enormer Aufwand, aber heutige Theorembeweiser sind schon ziemlich brauchbar. Auch solltet Ihr Euch vom Gedanken verabschieden, dass man dafuer iA. Programmiersprachen mit Seiteneffekten aus der Steinzeit (a la C, C++, Java...) einsetzen wuerde - denn dann wird es richtig aufwaendig. Allerdings gibt es einen relativ neuen Ansatz ueber Coalgebren, der versucht die oo-Sprachen abzudecken. Die Forschung dazu laeuft seit einigen Jahren und wurde auch schon bei C++ und Java angewandt. Mit "Testen" hat Korrektheit allerdings wenig zu tun.

Wer solche Beweissysteme mal testen will, kann sich mal PVS, Coq, Isabelle... ansehen - mathemat. Kenntnisse vorausgesetzt.

----------

## papahuhn

http://de.wikipedia.org/wiki/Hoare-Kalk%C3%BCl

Das lustige ist, dass der Typ bei Microsoft arbeitet.  :Mr. Green: 

----------

## oscarwild

 *Knieper wrote:*   

> "Fehlerfrei" insofern, dass Sie ein 100%iges Modell der Spezifikation ist. Allerdings muss dann auch die Spezifikation stimmen und die nimmt erfahrungsgemaess 1/3 des Umfangs des fertigen Programms an.

 

Das ist aber in sich etwas widersprüchlich - wäre die Software ein 100%iges Modell der Spezifikation, wäre der Umfang der Spezifikation mit der Software identisch. Letztendlich ist der Quellcode nichts weiter als eine ausführbare Spezifikation, mit den bekannten Problemen der Komplexität, die zu Spezifikationsfehlern bzw. Defekten in der Software führen, die sich wiederum in einer Fehlerwirkung äußern.

Es ist ja mitunter schon problematisch, eine konsistente, vollständige und widerspruchsfreie Top-Level Spezifikation zu erstellen, bzw. einen Kunden zu finden, der dazu in der Lage ist, seine Wünsche zu formulieren, erst recht gar nicht schon zu Projektbeginn.

 *Knieper wrote:*   

> Fuer Teile von Kommunikationsanlagen, Teile von Betriebssystemen (zB. VFiasco), Steuerungssoftware etc. wurde das schon gemacht.

 

Keine Frage - immer dann, wenn ein Ausfall zu extremen finanziellen Schäden führt, rentiert sich ggf. der Aufwand. Ein 100% Korrektheitsbeweis ist imho dennoch nicht möglich.

Dazu kommt leider: Softwareentwicklung muss stets wirtschaftlich sein, daher folgender Abstecher in die kaufmännischen Aspekte:

- in den Softwaretest, bzw. Software-QS im Allgemeinen kann ein beliebig hoher Aufwand investiert werden. Die Qualitätskosten steigen linear mit dem investierten Aufwand.

- Während eine Software ohne Test/QS mit einer Wahrscheinlichkeit gegen 1 schwerwiegende Fehler enthalten wird, erreicht die Fehlerrate auch bei extremem Aufwand nie 0, sondern nähern sich lediglich asymptotisch der 0. Die Fehlerkosten (Rückruf, Imageschaden, Fehlerbehebung etc.) sinken mit steigendem Qualitätsaufwand daher ebenfalls asymptotisch

Nun darf man als reiner Techniker durchaus etwas verblüfft sein: Ziel eines wirtschaftlich orientierten Unternehmens ist gar nicht die Fehlerfreiheit, sondern es wird der Gleichstand von Qualitäts- und Fehlerkosten angestrebt, bei dem das Minimum der Gesamtkosten liegt!

Im Übrigen, die genannten "Steinzeitsprachen" wird es auch in den nächsten 50 Jahren noch geben, im Consumer-Markt noch erheblich länger, sei es aus Kosten-, Kompatibilitäts- oder aus Performancegründen.

 *Knieper wrote:*   

> Wer solche Beweissysteme mal testen will, kann sich mal PVS, Coq, Isabelle... ansehen - mathemat. Kenntnisse vorausgesetzt.

 

Die kenne ich noch nicht, werde ich mir auf jeden Fall mal ansehen!

----------

## Knieper

 *oscarwild wrote:*   

>  *Knieper wrote:*   "Fehlerfrei" insofern, dass Sie ein 100%iges Modell der Spezifikation ist. Allerdings muss dann auch die Spezifikation stimmen und die nimmt erfahrungsgemaess 1/3 des Umfangs des fertigen Programms an. 
> 
> Das ist aber in sich etwas widersprüchlich - wäre die Software ein 100%iges Modell der Spezifikation, wäre der Umfang der Spezifikation mit der Software identisch.

 

Ist es nicht. Ich kann doch einen Sachverhalt kuerzer beschreiben, als ich ihn implementieren kann. Prosaisch: Funktion "myfunc" berechnet log(sin(x)). Fuer "myfunc" brauchst Du bestimmt Variablen, evtl. Schleifen, Klammern, Funktionsheader...

 *Quote:*   

> Keine Frage - immer dann, wenn ein Ausfall zu extremen finanziellen Schäden führt, rentiert sich ggf. der Aufwand. Ein 100% Korrektheitsbeweis ist imho dennoch nicht möglich.

 

Selbstverstaendlich ist der moeglich. Software ist nicht mehr als Mathematik. Deiner Meinung nach waere dann kein mathemat. Beweis moeglich - dabei sind nur _einige_ nicht moeglich.

 *Quote:*   

> - in den Softwaretest, bzw. Software-QS im Allgemeinen kann ein beliebig hoher Aufwand investiert werden. Die Qualitätskosten steigen linear mit dem investierten Aufwand.

 

Bei wichtiger Software hat sich in den letzten Jahren doch gezeigt, dass Testen einen hohen Stellenwert besitzt. Nur, und das ist jetzt meine Meinung, wieso sollte ich x Testfaelle schreiben, wenn ich auch gleich eine Spezifikation angeben kann. Ich denke mit ein paar Jahren Forschung werden Theorembeweiser, automat. Beweiser etc. auch im normalen Programmieralltag Einzug halten.

 *Quote:*   

> Im Übrigen, die genannten "Steinzeitsprachen" wird es auch in den nächsten 50 Jahren noch geben, im Consumer-Markt noch erheblich länger, sei es aus Kosten-, Kompatibilitäts- oder aus Performancegründen.

 

Geben evtl. noch, aber es waere schlimm, wenn sie da noch das Hauptwerkzeug der Programmierer waeren.

----------

## oscarwild

 *Knieper wrote:*   

> Ist es nicht. Ich kann doch einen Sachverhalt kuerzer beschreiben, als ich ihn implementieren kann. Prosaisch: Funktion "myfunc" berechnet log(sin(x)). Fuer "myfunc" brauchst Du bestimmt Variablen, evtl. Schleifen, Klammern, Funktionsheader...

 

Wenn Du unter "kürzer" die Anzahl der Zeichen verstehst, ja.

Sobald ich aber eine Variable benutze, die nicht in der Spezifikation enthalten ist, interpretiere bzw. detailliere ich die Spezifikation, implementiere also etwas mehr, als weiter oben steht. In der Folge gibt es aber auch immer mehrere denkbare Detaillösungen zu einer Spezifikation, die sich auch von ihrem Verhalten her geringfügig unterschieden können. Und da liegt der Käfer begraben  :Laughing: 

 *Knieper wrote:*   

> Selbstverstaendlich ist der moeglich. Software ist nicht mehr als Mathematik.

 

Jein. Ein dynamisches Softwaresystem lässt sich in einer unendlichen Gleichung ausdrücken, da liegt das Problem.

Eine Schleife ohne statische Abbruchbedingung ist nicht deterministisch; selbst wenn bei einem Boundary Interior Test oder einen strukturierten Pfadetest mit 1000 Durchläufen keine Fehler auftreten, lässt sich dennoch nicht beweisen, dass es beim 1001. Durchlauf in der Kiste rappelt - auch wenn das nicht naheliegend ist.

Ein Theorem basiert auf einer Abstraktion und Vereinfachung der Welt - mit dem Risiko, Feinheiten auszulassen.

Ein Theorem wird z.B. nicht in der Lage sein, eine Kontrollflussanomalie, die durch eine Interrupt Service Routine entsteht, abzudecken. Der Embedded-Bereich, der ein weit stärkeres Wachstumspotential besitzt als konventionelle Applikationssoftware, baut auf solchen Low-Level Konstrukten und Eigenschaften auf. Daher werden in diesem Marktsegment, auch die "Steinzeitsprachen" das Hauptwerkzeug der Programmierer bleiben.

 *Knieper wrote:*   

> Ich denke mit ein paar Jahren Forschung werden Theorembeweiser, automat. Beweiser etc. auch im normalen Programmieralltag Einzug halten.

 

Als Ergänzung sicher. Als ultimatives Heilmittel sicher nicht.

Hm, ich fürchte, wir werden es nicht schaffen, uns zu einigen  :Laughing: 

Macht aber nichts - die Zukunft wird unabhängig von jeder Spekulation zeigen, in welche Richtung der Softwarezug fährt.

----------

## firefly

Ich würde sagen das man für die meisten Anwendungen nicht 100%ig nachweisen kann das sie zu 100%ig fehlerfrei sind.

Es mag für einige Bereiche möglichkeiten geben eine 100%ig Fehlerfreiheit festzustellen.

Aber da der Aufwand meistens zu groß dafür ist, z.b aus wirtschaftlicher sicht, werden wahrscheinlich diese Möglichkeiten nur in speziellen Bereichen/bei speziellen Anforderungen angewannt, wo sich dieser Aufwand lohnt bzw. wo es überhaupt möglich ist.

----------

## Knieper

 *oscarwild wrote:*   

> Sobald ich aber eine Variable benutze, die nicht in der Spezifikation enthalten ist, interpretiere bzw. detailliere ich die Spezifikation, implementiere also etwas mehr, als weiter oben steht.

 

Da kommt wieder der Praktiker durch. Eine mathemat. Spezifikation hat mit den Muschibubuspecs in der freien Wildbahn nicht viel gemeinsam.

 *Knieper wrote:*   

> Ein dynamisches Softwaresystem lässt sich in einer unendlichen Gleichung ausdrücken, da liegt das Problem.
> 
> Eine Schleife ohne statische Abbruchbedingung ist nicht deterministisch; selbst wenn bei einem Boundary Interior Test oder einen strukturierten Pfadetest mit 1000 Durchläufen keine Fehler auftreten, lässt sich dennoch nicht beweisen, dass es beim 1001. Durchlauf in der Kiste rappelt - auch wenn das nicht naheliegend ist.

 

Es gibt aber noch viele andere Formalismen, um das Verhalten eines Systems zu beschreiben (siehe oben die Coalgebren, verschiedene Logiken...). Wenn Du beweist, dass alle natuerlichen Zahlen nichtnegativ sind, testest Du doch auch nicht alle durch, oder?   :Wink: 

 *Quote:*   

> Ein Theorem basiert auf einer Abstraktion und Vereinfachung der Welt - mit dem Risiko, Feinheiten auszulassen.

 

Die Feinheiten sind dann aber irrelevant. Solange ein Programm diese eine spezifizierte Funktionalitaet hat, ist im Prinzip egal, was es nebenher macht. Daher gibt es uU. unendlich viele Lsgn. zu einem Problem und somit auch undendl. viele verschiedene Implementationen zu einer Spec.

 *Quote:*   

> Ein Theorem wird z.B. nicht in der Lage sein, eine Kontrollflussanomalie, die durch eine Interrupt Service Routine entsteht, abzudecken.

 

Selbstverstaendlich ist es moeglich Seiteneffekte und Fehler zu behandeln.

----------

## oscarwild

 *Knieper wrote:*   

> Da kommt wieder der Praktiker durch.

 

Und das, wo ich mich schon beinahe selbst als Theoretiker empfinde. Es ist aber schon interessant, dass Leute mit praktischer Erfahrung immer als "Praktiker" belächelt werden. Impliziert das nicht zugleich, dass sich die durch die Theoretiker erdachten, visionären Ideen nicht so richtig in der Praxis bewähren?

Daher ein Aufruf: liebe Theoretiker, gebt mir ein System an die Hand, das unter dem Strich eine Entwicklung ermöglicht, die bei geringeren Entwicklungskosten eine gleichbleibende oder steigende Qualität ermöglicht.

Ich akzeptiere dafür gerne lustige Theorembeweiser aller Art, und wenns denn sein muss, Hydroschraubenschlüssel oder auch schwarze Magie. Sowohl mein Chef als auch meine Entwickler werden es Euch danken.

Um nur noch auf einige Punkte einzugehen:

 *Knieper wrote:*   

> Wenn Du beweist, dass alle natuerlichen Zahlen nichtnegativ sind, testest Du doch auch nicht alle durch, oder?  

 

Du wirst lachen - der Kunde schafft es durch geschickte Fehlbedienung - überspitzt formuliert - zur Not, auch eine negative natürliche Zahl zustande zu bringen. Fehler treten seltenst systematisch im 20%-Umfang der (spezifizierten) Sollfunktion auf, sondern sporadisch in den restlichen 80%, an die keiner so recht gedacht hat. 

 *Quote:*   

> Die Feinheiten sind dann aber irrelevant.

 

 :Laughing: 

 *Quote:*   

> Solange ein Programm diese eine spezifizierte Funktionalitaet hat

 

Wir drehen uns im Kreis - Spezifikationen sind nie vollständig, ob sie nun als Prosa in einem klassischen Pflichten/Lastenheft formuliert, als tabellarische Requirementspezifikation, oder in einer formalen Spezifikationssprache verfasst sind. Eine formale Spezifikation trägt dazu bei, z.B. eine Inkonsitenz oder einen Widerspruch, der bei einer textuellen Spezifikation zwischen Seite 15 und Seite 487 besteht, aufzudecken und daher niemandem auffällt. Die Komplexität bleibt dennoch bestehen.

Es hapert doch allein schon daran:

Kein magisches Werkzeug der Welt kann selbständig entscheiden, ob die Reaktion, den Schleudersitz auszulösen, angemessen ist, wenn der Pilot drei mal in die Hände klatscht. Diese Regel muss durch einen Menschen vorgegeben werden. Irrt sich dieser Mensch - was leider eine grundlegende Eigenschaft des Gallertklumpen in unseren Köpfen ist, und zugleich Dinge wie Kreativität erst ermöglicht - senkt das die Freude des Piloten, der sich nun leider im freien Fall befindet, obwohl er eigentlich nur vorhatte, seine Gedanken zum neuen Outfit der Stewardess Ausdruck zu verleihen.

Und es gibt unendlich viele Fälle, wo eine solche Entscheidung im Gegensatz zu den flapsigen Beispiel alles andere als trivial zu treffen ist. Da sind wir wieder bei der Komplexität...

----------

## Necoro

 *oscarwild wrote:*   

> Es hapert doch allein schon daran:
> 
> Kein magisches Werkzeug der Welt kann selbständig entscheiden, ob die Reaktion, den Schleudersitz auszulösen, angemessen ist, wenn der Pilot drei mal in die Hände klatscht. Diese Regel muss durch einen Menschen vorgegeben werden. Irrt sich dieser Mensch - was leider eine grundlegende Eigenschaft des Gallertklumpen in unseren Köpfen ist, und zugleich Dinge wie Kreativität erst ermöglicht - senkt das die Freude des Piloten, der sich nun leider im freien Fall befindet, obwohl er eigentlich nur vorhatte, seine Gedanken zum neuen Outfit der Stewardess Ausdruck zu verleihen.
> 
> Und es gibt unendlich viele Fälle, wo eine solche Entscheidung im Gegensatz zu den flapsigen Beispiel alles andere als trivial zu treffen ist. Da sind wir wieder bei der Komplexität...

 

Das hat aber nichts mit der formalen Korrektheit des Programms zu tun  :Cool: 

----------

## Knieper

 *oscarwild wrote:*   

> Es ist aber schon interessant, dass Leute mit praktischer Erfahrung immer als "Praktiker" belächelt werden. Impliziert das nicht zugleich, dass sich die durch die Theoretiker erdachten, visionären Ideen nicht so richtig in der Praxis bewähren?

 

Noe, das impliziert, dass Du Dich noch nicht mit Verifikationsprinzipien vertraut gemacht hast und es Dir momentan etwas schwer faellt, Dich dort hineinzudenken. Verifikation funktioniert schon in der Praxis - nicht nur bei Hardware.

 *Quote:*   

> Daher ein Aufruf: liebe Theoretiker, gebt mir ein System an die Hand, das unter dem Strich eine Entwicklung ermöglicht, die bei geringeren Entwicklungskosten eine gleichbleibende oder steigende Qualität ermöglicht.

 

Und den Porsche gibt's gratis dazu? Wenn Du bessere Produkte haben willst oder Fehler ganz boese Auswirkungen haben, wird sich der Aufwand auch jetzt schon rechnen.

 *Quote:*   

> Wir drehen uns im Kreis - Spezifikationen sind nie vollständig, ob sie nun als Prosa in einem klassischen Pflichten/Lastenheft formuliert, als tabellarische Requirementspezifikation, oder in einer formalen Spezifikationssprache verfasst sind. Eine formale Spezifikation trägt dazu bei, z.B. eine Inkonsitenz oder einen Widerspruch, der bei einer textuellen Spezifikation zwischen Seite 15 und Seite 487 besteht, aufzudecken und daher niemandem auffällt. Die Komplexität bleibt dennoch bestehen.

 

Also sind auch Programme nie vollstaendig, da man deren Funktionalitaet nicht beschreiben kann? Putzige Argumentation.

 *Quote:*   

> Kein magisches Werkzeug der Welt kann selbständig entscheiden, ob die Reaktion, den Schleudersitz auszulösen, angemessen ist, wenn der Pilot drei mal in die Hände klatscht. Diese Regel muss durch einen Menschen vorgegeben werden.

 

Ich habe nicht gesagt, dass Spezifikationen immer richtig sein muessen und selbstverstaendlich braucht man einen Menschen, der angibt, was das Programm tun soll. Man braucht wahrsch. auch immer einen, der dem Rechner beim Beweisen hilft.

 *Quote:*   

> Irrt sich dieser Mensch - was leider eine grundlegende Eigenschaft des Gallertklumpen in unseren Köpfen ist, und zugleich Dinge wie Kreativität erst ermöglicht - senkt das die Freude des Piloten, der sich nun leider im freien Fall befindet, obwohl er eigentlich nur vorhatte, seine Gedanken zum neuen Outfit der Stewardess Ausdruck zu verleihen.

 

Dann musst Du eben versuchen zu beweisen, dass in Deinem System der Schleudersitz nur ausgeloest wird, wenn der rote Knopf gedrueckt wird.

 *Quote:*   

> Und es gibt unendlich viele Fälle, wo eine solche Entscheidung im Gegensatz zu den flapsigen Beispiel alles andere als trivial zu treffen ist. Da sind wir wieder bei der Komplexität...

 

Und? Entweder es ist zu komplex und ich kann es nicht implementieren, oder ich kann es, dann muss ich auch wissen, was ich will -> Spec.

----------

## oscarwild

Lockheed's F-22 Raptor Gets Zapped by International Date Line

So ist das halt mit der fehlerfreien Software. Da waren bestimmt wieder die doofen Praktiker am Werk  :Laughing: 

----------

## Mr. Anderson

Da. ^^

----------

## oscarwild

Und da auch!  :Laughing: 

----------

## Mr. Anderson

 *oscarwild wrote:*   

> Und da auch! 

 

Naja, bei MS hat es erst jahrelange Arbeit einer Expertengruppe gebraucht, um herauszufinden, dass man mit automatischen Beweisern doch tatsächlich einige Fehler finden kann.

Können die Programmverifikation überhaupt buchstabieren?

----------

## Fauli

Wie jeder weiß, ist TeX fehlerfrei!

```
$ tex

This is TeX, Version 3.141592 (Web2C 7.5.5)
```

Und das bis mindestens sechs Stellen nach dem Komma!  :Wink: 

----------

## l3u

In TeX ist glaub ich wirklich seit 20 Jahren kein Fehler mehr gefunden worden.

----------

## oscarwild

jo, hat bei TeX aber auch ne ganze Weile gedauert  :Wink: 

Dass keine Fehler mehr gefunden wurden, heißt aber nicht, dass die Software tatsächlich fehlerfrei ist; es können durchaus Defekte vorhanden sein, die lediglich zu keiner Fehlerwirkung führen, was sich aber nach einer Softwareänderung - wenn auch relativ unwahrscheinlich - durchaus ändern könnte.

----------

