SPARK Ada - Formale Methoden (was: [OT])
Vinzent Hoefler
>Vinzent Hoefler <JeLlyFish...@gmx.net> writes:
>> Rainer Weikusat <weik...@students.uni-mainz.de> wrote:
>>>
>>> Falls Du es 'vertrauenerweckend' findest,
>>> zu einem Berg von Quellcode, den Du nicht verstehst, noch einen ebenso
>>> unverständlichen Berg an Nathetik zu bekommen,
>>
>> [ ] Du hast SPARK verstanden.
>
>Ich habe mich solange durch die website gewühlt, bis ich unter der
>buzzword-Bergen das hier gefunden hatte:
>
> We formally specified the system using Z, coded it in SPARK
> Ada, and mathematically proved the specification and code of
> the safety critical functions.
Ich unterstreiche mal: "...mathematically proved the specification..."
> This project has shown that
> mathematical analysis of industrial scale software is
> practicable, giving the highest level of confidence in the
> correctness of the software.
>
>Angesichts der Tatsache, daß jedes Jahr Menschen sterben, weil andere
>sich verrechnet haben, mutet diese Aussage etwas seltsam an.
In der Praxis scheint das aber recht gut zu funktionieren, wenn ich
den Leuten von Lockheed-Martin und Boeing Glauben schenken darf.
Dagegen muten Aussagen wie
"Nicht wirklich. Korrektheitsbeweise sind prinzipiell redundant, denn
die Semantik einer Programmiersprache ist eindeutig definiert."
(<87n0lqw...@winter.inter-i.wohnheim.uni-mainz.de>)
und
"Falls jemand einen vetrackten logischen Fehler in einem Programm mit
mehreren parallellen Kontrolflüssen hat, der durch eine abartig
seltene Kombination fehlerhafter Eingabedaten ausgelöst wird, ist das
tolerabel (wenngleich ärgerlich)."
(<87n0lxjr...@winter.inter-i.wohnheim.uni-mainz.de>)
doch wesentlich komischer an.
Wenn ich das jetzt mal frei interpretiere, akzeptierst Du damit den
Tod von Menschen als aergerlich, aber tolerabel, waehrend es komisch
waere, doch wenigstens zu versuchen, zu beweisen, dass das von der
Software her (nahezu) ausgeschlossen werden kann, da das korrekte
Verhalten der Software ohnehin im Quellcode steht? :-)
Nein, ich halte auch vertrackte logische Fehler nicht fuer tolerabel.
Und Korrektheitsbeweise koennen solche Fehler sicher finden, wenn sie
ausserhalb der beschriebenen Spezifikation sind.
>Es bleibt
>auch unklar, wer mir die Äquivalenz dessen, was bewiesen wurde, mit
>dem Quelltext garantiert
Der SPARK-Examiner. Der Beweis *ist* der Quelltext. Es gibt keinen
zweiten Ordner mit vielen tollen Formeln dazu. Ein SPARK-Quelltext,
dessen Korrektheit (in erster Linie heisst das frei von
Laufzeitfehlern) nicht formal bewiesen werden kann, ist einfach kein
gueltiges SPARK-Programm.
>und warum beim Aufstellen des Beweise eine
>geringere Wahrscheinlichkeit für Fehler bestand, als beim Schreiben
>des Quellcodes.
Weil der Beweis auf formalen Methoden beruht, es duerfte von daher
wesentlich leichter sein, die moeglicherweise vorhandenen
Inkonsistenzen zu finden als das in einem beliebigen Quelltext der
Fall waere.
Da SPARK eben die Uebereinstimmung aller Pre- und Postconditions mit
dem Quellcode garantiert, ist letztendlich so ziemlich das einzige,
was Dir passieren kann, dass Du die Spezifikation falsch angibst oder
der Compiler nachher den Quellcode in den falschen Objektcode
umwandelt.
Wegen letzterem wird ja ueblicherweise noch die Uebereinstimmung des
Objektcodes mit dem Sourcecode gezeigt. Allerdings ist Boeing
mittlerweile eine Schritt weiter, indem sie sich von der FAA einen
speziellen Compiler (der recht SPARK-aehnlich ist) haben
zertifizieren[0] lassen koennen, der garantiert, dass er immer
Objektcode erzeugt, der der Semantik des Quellcodes entspricht. Somit
reicht dann der Beweise auf Source-Code-Ebene aus.
> I agree. Testing will always be essential no matter how
> efficient proof is, because of the limitations of what proof
> models.
> <URL:http://www.cs.york.ac.uk/hise/safety-critical-archive/2000/0504.html>
Ja. Unter anderem, weil eine Aequivalenz des Quelltextes mit der
Spezifikation nicht beweist, dass die Spezifikation das ist, was Du
wirklich haben moechtest.
Aus demselben Beitrag:
|The unit testing process was (at least comparatively) pretty
|inefficient and understanding that has certainly helped on other
|projects.
Unit-testing ist entfernt wohl das, was Du damit meintest:
"Ein Programm mit mehr als fünfhundert Zeilen besteht aus sauber
getrennten Subsystemen/ Modulen, die ausschließlich über
definierte Interfaces kommunizieren und deren Interna unterhalb einer
prozeduralen Spezifiaktion des Interfaces lokalisiert bleiben und
jeder einzelne dieser Teile ist klein genug, damit man ihn separat
debuggen kann."
(<87n0lxjr...@winter.inter-i.wohnheim.uni-mainz.de>)
So die Theorie und in den vielen Faellen mag das stimmen. Laut Rod
(und ich glaube da einfach mal seiner Erfahrung) findet man die
meisten Fehler aber, wenn man diese einzelnen Unit zusammenfuegen
will, also letztendlich im Interface. Das ist im uebrigen auch meine
Erfahrung.
Naja, den Rest des Absatzes quote ich einfach deshalb noch, weil Deine
Frage ja, IIRC, urspruenglich war, wer denn ueberhaupt Software formal
verifiziert:
|Also seeing the faults that the Z proof work found early on,
|especially in comparison with the effort it took, has personally
|made me much more likely to do such proof work in the future.
Wenn es Dich interessiert, kann ich Dir gerne auch mal die Zahlen
raussuchen, wieviele Fehler man in welcher Phase waehrend der
Entwicklung des MultOS-Kernels gefunden und beseitigt hat. IIRC haben
es von ~150 Fehlern nur vier ueberhaupt bis in die Testphase
geschafft. Und, das war es, was ich oben erwaehnte, eine nicht ganz
unerhebliche Zahl waren Fehler in der Spezifikation, die das
Verifikationssystem aufgedeckt hat.
>> >> >Nur für Spielzeugsprachen wie z.B. kleine Turingmaschinen mit nicht
>> >> >allzuviel Zuständen.
>> >>
>> >> Spielzeugsprache? http://www.sparkada.com
>> >
>> >Genauso klingt das.
>>
>> google SHOLIS
>
> * SPARK Language Features
> SPARK is a subset of the [13]Ada language. It includes Ada
> constructs regarded as essential for the construction of
> complex software, such as packages, private types, typed
> constants, functions with structured values, and the library
> system.
Was davon kann C? Packages kann man ja notfalls noch durch #include
substituieren. Demzufolge ist C fuer Dich eine Spielzeugsprache?
> It excludes tasks, exceptions, generic units, access
> types, use clauses, type aliasing, anonymous types, default
> values in record declarations, default subprogram parameters,
> goto statements, and declare statements.
C kennt keine Tasks (nachdem, was Rod Chapman im Dezember erzaehlt
hat, arbeiten PCS allerdings momentan an einem SPARK-System, dass das
Ravenscar-Profile erfuellen soll, somit waeren Tasks dort in der
naechsten Version enthalten), keine Exceptions (SPARK braucht keine,
da ja gerade die Abwesenheit von Laufzeitfehlern bewiesen wird) und
auch keine Generics. Das einzige, was Dir fehlt, sind gotos (braucht
man die?) und access-types, sprich (dynamische) pointer und das ist
nicht wirklich ein Verlust, da in C Zeiger eher zu extensiv auch in
statischen Zusammenhaengen benoetigt werden. Der Rest ist
ausschliesslich syntactic sugar.
Was ich mit SHOLIS meinte: Wenn mit SPARK ein System beschreiben kann,
welches die sicherheitskritische Software eines Helikopters darstellt,
kann man das wohl kaum als Spielzeugsprache ansehen. Das Teil fliegt
ausserhalb von Kinderzimmern.
Lockheed-Martin nutzte das in der Hercules-C130J und sie behaupten,
damit 80% der Entwicklungskosten gegenueber herkoemmlichen Methoden
gespart haben zu koennen und vor allem: "It worked from the first
time."
Da wir damit in de.comp.lang.c aber nun wirklich ziemlich gruendlich
OT sind, wuerde ich das ganze mal nach de.comp.lang.misc crossposten
und gleichzeitig auch das F'up nach dorthin vorschlagen.
Vinzent.
[0] Um mal einen Eindruck davon zu bekommen, was FAA-Zertifizierung
bedeutet, der Mensch von Boeing sprach von IIRC, ueber 2000 (in
Worten: zweitausend) Unterschriften, die im Laufe des
Zertifizierungsprozesses benoetigt wurden. Aber ich kann die Papers
gern noch mal raussuchen.
Florian Weimer
> Ich unterstreiche mal: "...mathematically proved the
> specification..."
Warum? Weil es Quatsch ist? ;-)
Vinzent Hoefler
>Vinzent Hoefler <JeLlyFish...@gmx.net> writes:
>
>> Ich unterstreiche mal: "...mathematically proved the
>> specification..."
>
>Warum?
Weil damit nicht bewiesen ist, dass die Spezifikation korrekt ist?
>Weil es Quatsch ist? ;-)
Inwiefern? Man sollte das vielleicht nicht ganz aus dem Zusammenhang
reissen.
Vinzent.
Rainer Weikusat
> Rainer Weikusat <weik...@students.uni-mainz.de> wrote:
> >Ich habe mich solange durch die website gewühlt, bis ich unter der
> >buzzword-Bergen das hier gefunden hatte:
> >
> > We formally specified the system using Z, coded it in SPARK
> > Ada, and mathematically proved the specification and code of
> > the safety critical functions.
>
> Ich unterstreiche mal: "...mathematically proved the
> specification..."
Wozu?
[...]
> >Angesichts der Tatsache, daß jedes Jahr Menschen sterben, weil andere
> >sich verrechnet haben, mutet diese Aussage etwas seltsam an.
>
> In der Praxis scheint das aber recht gut zu funktionieren, wenn ich
> den Leuten von Lockheed-Martin und Boeing Glauben schenken darf.
>
> Dagegen muten Aussagen wie
>
> "Nicht wirklich. Korrektheitsbeweise sind prinzipiell redundant, denn
> die Semantik einer Programmiersprache ist eindeutig definiert."
> (<87n0lqw...@winter.inter-i.wohnheim.uni-mainz.de>)
>
> und
>
> "Falls jemand einen vetrackten logischen Fehler in einem Programm mit
> mehreren parallellen Kontrolflüssen hat, der durch eine abartig
> seltene Kombination fehlerhafter Eingabedaten ausgelöst wird, ist das
> tolerabel (wenngleich ärgerlich)."
> (<87n0lxjr...@winter.inter-i.wohnheim.uni-mainz.de>)
>
> doch wesentlich komischer an.
>
> Wenn ich das jetzt mal frei interpretiere, akzeptierst Du damit den
> Tod von Menschen als aergerlich, aber tolerabel,
Lieber Vinzent, ich glaube, ich lege Maßstäbe an Software an, die Du
Dir noch nicht einmal vorstellen kannst.
> waehrend es komisch waere, doch wenigstens zu versuchen, zu
> beweisen, dass das von der Software her (nahezu) ausgeschlossen
> werden kann, da das korrekte Verhalten der Software ohnehin im
> Quellcode steht?
Falls Du zum Verständnis des Quellcodes irgendetwas anderes außer dem
Quellcode benötigst darfst Du aufhören, Dir darüber Sorgen zu machen.
> Nein, ich halte auch vertrackte logische Fehler nicht fuer tolerabel.
> Und Korrektheitsbeweise koennen solche Fehler sicher finden, wenn sie
> ausserhalb der beschriebenen Spezifikation sind.
«There's a killer on the loose again».
> >Es bleibt auch unklar, wer mir die Äquivalenz dessen, was bewiesen
> >wurde, mit dem Quelltext garantiert
>
> Der SPARK-Examiner. Der Beweis *ist* der Quelltext. Es gibt keinen
> zweiten Ordner mit vielen tollen Formeln dazu. Ein SPARK-Quelltext,
> dessen Korrektheit (in erster Linie heisst das frei von
> Laufzeitfehlern) nicht formal bewiesen werden kann, ist einfach kein
> gueltiges SPARK-Programm.
Normale Leute nennen sowas einen Zirkelschluß.
> >und warum beim Aufstellen des Beweise eine geringere
> >Wahrscheinlichkeit für Fehler bestand, als beim Schreiben des
> >Quellcodes.
>
> Weil der Beweis auf formalen Methoden beruht,
> es duerfte von daher wesentlich leichter sein, die moeglicherweise
> vorhandenen Inkonsistenzen zu finden als das in einem beliebigen
> Quelltext der Fall waere.
Vertrau mir: "Engineers learn quickly how to avoid warnings" wird von
fünf von zehn Fällen "den Kommentar kann ich grade nicht brauchen"
heißen.
> Unit-testing ist entfernt wohl das, was Du damit meintest:
>
> "Ein Programm mit mehr als fünfhundert Zeilen besteht aus sauber
> getrennten Subsystemen/ Modulen, die ausschließlich über
> definierte Interfaces kommunizieren und deren Interna unterhalb einer
> prozeduralen Spezifiaktion des Interfaces lokalisiert bleiben und
> jeder einzelne dieser Teile ist klein genug, damit man ihn separat
> debuggen kann."
> (<87n0lxjr...@winter.inter-i.wohnheim.uni-mainz.de>)
>
> So die Theorie und in den vielen Faellen mag das stimmen. Laut Rod
> (und ich glaube da einfach mal seiner Erfahrung) findet man die
> meisten Fehler aber, wenn man diese einzelnen Unit zusammenfuegen
> will, also letztendlich im Interface. Das ist im uebrigen auch meine
> Erfahrung.
Das ist eine groteskte Horrortheorie, deren Implikationen
ausschließlich besagen, daß die Resultate lebensgefährlich sein
werden.
> Wenn es Dich interessiert, kann ich Dir gerne auch mal die Zahlen
> raussuchen, wieviele Fehler man in welcher Phase waehrend der
> Entwicklung des MultOS-Kernels gefunden und beseitigt hat.
Bitte nicht. Ich denke ohnehin schon darüber nach, sofort zum
militanten Technikfeind zu werden.
> >> >> Spielzeugsprache? http://www.sparkada.com
> >> >
> >> >Genauso klingt das.
> >>
> >> google SHOLIS
> >
> > * SPARK Language Features
> > SPARK is a subset of the [13]Ada language. It includes Ada
> > constructs regarded as essential for the construction of
> > complex software, such as packages, private types, typed
> > constants, functions with structured values, and the library
> > system.
>
> Was davon kann C?
Was kann man damit ausdrücken, das man nicht in jeder
turing-vollständigen Sprache ausdrücken kann?
[...]
> keine Exceptions (SPARK braucht keine, da ja gerade die Abwesenheit
> von Laufzeitfehlern bewiesen wird)
In einem System mit mechanischen Komponenten?
> und auch keine Generics.
> Das einzige, was Dir fehlt, sind gotos (braucht
> man die?)
«Man» benutzt sie ständig, was vom Compiler mehr oder minder hinter
einem Feigenblatt verborgen wird.
> und access-types, sprich (dynamische) pointer und das ist
> nicht wirklich ein Verlust, da in C Zeiger eher zu extensiv auch in
> statischen Zusammenhaengen benoetigt werden.
Obiges gilt entsprechend: Objekte im RAM haben eine Adresse, die die
CPU benutzt, um sie zu adressieren.
> Was ich mit SHOLIS meinte: Wenn mit SPARK ein System beschreiben kann,
> welches die sicherheitskritische Software eines Helikopters
> darstellt,
Es ist «bewiesen», daß man so ein System in Visual Basic beschreiben
kann.
Stefan Nobis
> Was kann man damit ausdrücken, das man nicht in jeder
> turing-vollständigen Sprache ausdrücken kann?
(Komplexere) Abstraktionen und (konzeptionelle) Zusammenhänge.
Wenn alles, was man für komplexere Programme benötigen würde, eine
beliebige turing-vollständige Sprache wäre, wäre C totaler Overkill. C
unterstützt schon eine Menge Abstraktionen, die für
Turing-Vollständigkeit vollkommen überflüssig sind.
Ist C also bloatig? Nein? Wo genau ist dann die Grenze von sinnvollen
Abstraktionen? It depends? Ah, und warum dann nicht Sprachen
verwenden, die mehr Abstraktionsmittel als C zur Verfügung stellen
(sofern man sie benötigt!)?
--
Stefan.
Georg Bauhaus
: Falls Du zum Verst?ndnis des Quellcodes irgendetwas anderes au?er dem
: Quellcode ben?tigst darfst Du aufh?ren, Dir dar?ber Sorgen zu machen.
Ich weiss nicht ob ich den worueber-Bezug aufloesen konnte. Sonst:
Definiere die Wirkung von ":=" in a := b, a und b Referenzen auf Instanzen
konformer Typen in einer Sprache deiner Wahl, mit vordefiniertem ":=".
Schnell, ohne Blick in Handbuecher. Du musst das Programm pruefen, weil
eine Fehlfunktion entdeckt wurde. Formale Hilfsmittel sind nicht zu
gelassen.
:> Weil der Beweis auf formalen Methoden beruht,
:> es duerfte von daher wesentlich leichter sein, die moeglicherweise
:> vorhandenen Inkonsistenzen zu finden als das in einem beliebigen
:> Quelltext der Fall waere.
:
: Vertrau mir: "Engineers learn quickly how to avoid warnings" wird von
: f?nf von zehn F?llen "den Kommentar kann ich grade nicht brauchen"
: hei?en.
Das wird schnell anders, wenn die "Engineers" mit persoenlichen
Folgen rechnen muessen. Der Kommentar sagt nichts dazu, ob formale
MEthoden erleichtern, erschweren, ... ?
:> Laut Rod
:> (und ich glaube da einfach mal seiner Erfahrung) findet man die
:> meisten Fehler aber, wenn man diese einzelnen Unit zusammenfuegen
:> will, also letztendlich im Interface.
:
: Das ist eine groteskte Horrortheorie,
Hm. Warum?
: deren Implikationen : ausschlie?lich besagen, da? die Resultate
: lebensgef?hrlich sein werden.
Deine Loesung ist ___?
:> Was davon kann C?
:
: Was kann man damit ausdr?cken, das man nicht in jeder
: turing-Vollst?ndigen Sprache ausdr?cken kann?
{ (ascii + 72),
(ascii + 105),
(ascii + 108),
(ascii + 102),
(ascii + 114),
(ascii + 101),
(ascii + 105),
(ascii + 99),
(ascii + 104),
(ascii + 101),
(ascii + 115)
}
Jedes turing-vollstaendige setup koennte Speichersammlung
bereitstellen. Wer/was schuetzt die Steuerung des Roentgen-Kastens
davor, dass das jemand versehentlich genutzt hat?
:> Das einzige, was Dir fehlt, sind gotos (braucht
:> man die?)
: ?Man? benutzt sie st?ndig, was vom Compiler mehr oder minder hinter
: einem Feigenblatt verborgen wird.
Sicher, aber "compiler" != "man".
: Obiges gilt entsprechend: Objekte im RAM haben eine Adresse, die die
: CPU benutzt, um sie zu adressieren.
Was ueberlegen laesst, dass CPUs indirekte Adressierung ueber
Bereichs-Tabellen benutzten koennten, und die koennten ja auch kaputt
sein, wegen Hardware-Fehlers... Nur, was bedeutet das fuer das
Formulieren von Programmen in Hochsprache X?
Die Behauptungen, die in einem Programm-Quelltext enthalten sind,
koennen glaube ich ohne Gesichtsverlust explizit gemacht werden,
zum Nutzen derer, die es nutzen, oder warten, oder pruefen.
Das kann die Autoren selber betreffen.
Schliesslich hat nicht jeder die vollstaendige Sprachdefinition
der Sprache X im Kopf, geschweige denn jede Herleitung zur Loesung
einer Sprachfrage.
: Es ist ?bewiesen?, da? man so ein System in Visual Basic beschreiben
: kann.
Welche Laufzeit-Umgebung wird von Miscrosoft fuer Echtzeit-STeuerungen
verkauf? (Egal ob VB, C#, C++, Fortran...)
Wie geht Bit-Adressierung auf Sparc-CPUs mit Visual-Basic?
Ich bin sicher, dass es moeglich ist, in einer konkreten Prolog-Variante
eine Motor-Steuerung zu beschreiben, bleibt aber zu beurteilen,
ob das in endlicher Zeit moeglich ist, ob es ueberschaubar bleibt,
und m.a.W. ob das je verwirklicht werden kann, in einem Forschungs-Labor
oder bei einem Kfz-Hersteller.
Aehnliches ist mit Haskell und Ada probiert worden. Ja, es ist moeglich
in Haskell praktischerweise reaktive Systeme sauber zu beschreiben,
zu simulieren.
Nein, es ist derzeit nicht moeglich, etwas Anderes als ein lauffaehiges,
aber zu langsames, zu viel Speicher benoetigendes Modell damit zu erzeugen
(in der echten Welt).
Gruesse,
Georg
Vinzent Hoefler
> Vinzent Hoefler <JeLlyFish...@gmx.net> writes:
>> Rainer Weikusat <weik...@students.uni-mainz.de> wrote:
>> >Ich habe mich solange durch die website gewühlt, bis ich unter der
>>
>> Ich unterstreiche mal: "...mathematically proved the
>> specification..."
>
> Wozu?
Das hatte ich weiter unten ausgefuehrt.
>> Wenn ich das jetzt mal frei interpretiere, akzeptierst Du damit den
>> Tod von Menschen als aergerlich, aber tolerabel,
>
> Lieber Vinzent, ich glaube, ich lege Maßstäbe an Software an, die Du
> Dir noch nicht einmal vorstellen kannst.
Ehrlich gesagt, das *will* ich mir auch gar nicht vorstellen.
>> waehrend es komisch waere, doch wenigstens zu versuchen, zu
>> beweisen, dass das von der Software her (nahezu) ausgeschlossen
>> werden kann, da das korrekte Verhalten der Software ohnehin im
>> Quellcode steht?
>
> Falls Du zum Verständnis des Quellcodes irgendetwas anderes außer dem
> Quellcode benötigst darfst Du aufhören, Dir darüber Sorgen zu machen.
Das Verstaendnis des Quellcodes sagt nichts ueber seine Korrektheit aus.
Und es wohl kaum moeglich, ein 100'000 Zeilen-Programm vollstaendig zu
verstehen und garantieren zu koennen, dass es das tut, was es tun soll,
unter allen Umstaenden.
>> Nein, ich halte auch vertrackte logische Fehler nicht fuer tolerabel.
>> Und Korrektheitsbeweise koennen solche Fehler sicher finden, wenn sie
>> ausserhalb der beschriebenen Spezifikation sind.
>
> «There's a killer on the loose again».
Was willst Du damit sagen? It is easier to fit the specification to a
program than vice versa?
>> >Es bleibt auch unklar, wer mir die Äquivalenz dessen, was bewiesen
>> >wurde, mit dem Quelltext garantiert
>>
>> Der SPARK-Examiner. Der Beweis *ist* der Quelltext. Es gibt keinen
>> zweiten Ordner mit vielen tollen Formeln dazu. Ein SPARK-Quelltext,
>> dessen Korrektheit (in erster Linie heisst das frei von
>> Laufzeitfehlern) nicht formal bewiesen werden kann, ist einfach kein
>> gueltiges SPARK-Programm.
>
> Normale Leute nennen sowas einen Zirkelschluß.
Und Leute, die sich ein klein wenig mit diesen Methoden beschaeftigt
haben, wissen, dass die SPARK-Annotations nicht den ausfuehrenden Code
darstellen. Ja, es ist redundant, nachdem der Examiner festgestellt
hat, dass beides korreliert.
>> Weil der Beweis auf formalen Methoden beruht,
>> es duerfte von daher wesentlich leichter sein, die moeglicherweise
>> vorhandenen Inkonsistenzen zu finden als das in einem beliebigen
>> Quelltext der Fall waere.
>
> Vertrau mir: "Engineers learn quickly how to avoid warnings" wird von
> fünf von zehn Fällen "den Kommentar kann ich grade nicht brauchen"
> heißen.
Tja, dann haben diese 50% ihren Beruf verfehlt.
Du stimmst mir also zu, dass Fehler im Quellcode wesentlich schwerer zu
finden sind als im Zuge einer formalen Beschreibung?
>> Unit-testing ist entfernt wohl das, was Du damit meintest:
>>
>> "Ein Programm mit mehr als fünfhundert Zeilen besteht aus sauber
>> getrennten Subsystemen/ Modulen, die ausschließlich über
>> definierte Interfaces kommunizieren und deren Interna unterhalb einer
>> prozeduralen Spezifiaktion des Interfaces lokalisiert bleiben und
>> jeder einzelne dieser Teile ist klein genug, damit man ihn separat
>> debuggen kann."
>> (<87n0lxjr...@winter.inter-i.wohnheim.uni-mainz.de>)
>>
>> So die Theorie und in den vielen Faellen mag das stimmen. Laut Rod
>> (und ich glaube da einfach mal seiner Erfahrung) findet man die
>> meisten Fehler aber, wenn man diese einzelnen Unit zusammenfuegen
>> will, also letztendlich im Interface. Das ist im uebrigen auch meine
>> Erfahrung.
>
> Das ist eine groteskte Horrortheorie,
Diese Theorie stammt von Dir, danke. Oder meintest Du eher:
IEEE Software Vol. 19, No. 1, Jan/Feb 2002:
"Traditionally critical-systems testings is very expensive. A reason for
this is that testing occurs several times: we test indivisual units,
integrate them and test the integration, and then the system as whole.
Our experience with previous safety-critical projects suggests that
this approach is inefficient and particularly that unit testing is
ineffective because most errors are interface errors, not internal
errors in units. It is expensive because we must build test harnesses
to test units in isolation."
> deren Implikationen
> ausschließlich besagen, daß die Resultate lebensgefährlich sein
> werden.
Interessant. Wie kommst Du darauf?
>> Wenn es Dich interessiert, kann ich Dir gerne auch mal die Zahlen
>> raussuchen, wieviele Fehler man in welcher Phase waehrend der
>> Entwicklung des MultOS-Kernels gefunden und beseitigt hat.
>
> Bitte nicht.
Sicher? Es sind uebrigens ein paar mehr als ich in Erinnerung hatte.
> Ich denke ohnehin schon darüber nach, sofort zum
> militanten Technikfeind zu werden.
Tu das.
>> >> >> Spielzeugsprache? http://www.sparkada.com
[...]
>> > * SPARK Language Features
[...]
>>
>> Was davon kann C?
>
> Was kann man damit ausdrücken, das man nicht in jeder
> turing-vollständigen Sprache ausdrücken kann?
Eine Registermaschine ist auch turing-vollstaendig. Warum also C? Ich
bin immer noch nicht ganz dahintergekommen, was Du mit Spielzeugsprache
meinst.
Eine Sprache, die es einfacher macht, korrekten Code zu schreiben, weil
das dann ja jedes Kind tun kann? Dein Problem, ich schreibe keine
Software, um mit Compiler und Debugger zu kaempfen, ich schreibe
Software, um etwas zum Laufen zu bekommen.
>> keine Exceptions (SPARK braucht keine, da ja gerade die Abwesenheit
>> von Laufzeitfehlern bewiesen wird)
>
> In einem System mit mechanischen Komponenten?
In der Software? Ja.
>> und auch keine Generics.
>
>> Das einzige, was Dir fehlt, sind gotos (braucht
>> man die?)
>
> «Man» benutzt sie ständig, was vom Compiler mehr oder minder hinter
> einem Feigenblatt verborgen wird.
*Das* weiss ich selbst.
>> und access-types, sprich (dynamische) pointer und das ist
>> nicht wirklich ein Verlust, da in C Zeiger eher zu extensiv auch in
>> statischen Zusammenhaengen benoetigt werden.
>
> Obiges gilt entsprechend: Objekte im RAM haben eine Adresse, die die
> CPU benutzt, um sie zu adressieren.
Und? Deswegen muss ich das Objekt auf Source-Ebene nicht mit seiner
Adresse ansprechen.
Da kannst Du auch gleich wieder Assembler programmieren.
>> Was ich mit SHOLIS meinte: Wenn mit SPARK ein System beschreiben
>> kann, welches die sicherheitskritische Software eines Helikopters
>> darstellt,
>
> Es ist «bewiesen», daß man so ein System in Visual Basic beschreiben
> kann.
So, kann man das? Welches Zeitfenster setzt Du an bis zur Zertifikation
nach DO-178B und/oder ITSEC E6?
Vinzent.
--
Getting an education at the University of California is like having
$50.00 shoved up your ass, a nickel at a time.
Rainer Weikusat
> Rainer Weikusat <weik...@students.uni-mainz.de> wrote:
> : Falls Du zum Verst?ndnis des Quellcodes irgendetwas anderes au?er dem
> : Quellcode ben?tigst darfst Du aufh?ren, Dir dar?ber Sorgen zu machen.
>
> Ich weiss nicht ob ich den worueber-Bezug aufloesen konnte. Sonst:
> Definiere die Wirkung von ":=" in a := b, a und b Referenzen auf Instanzen
> konformer Typen in einer Sprache deiner Wahl, mit vordefiniertem ":=".
> Schnell, ohne Blick in Handbuecher. Du musst das Programm pruefen, weil
> eine Fehlfunktion entdeckt wurde. Formale Hilfsmittel sind nicht zu
> gelassen.
In allen Sprachen, die ich verwende, ist := ein
Syntaxfehler. Dokumentation benutzt man im übrigen zum Nachschlagen,
denn dafür ist sie da. Ich muß allerdings gestehen, Dir nicht ganz
folgen zu können.
> :> Laut Rod
> :> (und ich glaube da einfach mal seiner Erfahrung) findet man die
> :> meisten Fehler aber, wenn man diese einzelnen Unit zusammenfuegen
> :> will, also letztendlich im Interface.
> :
> : Das ist eine groteskte Horrortheorie,
>
> Hm. Warum?
Vielleicht sollte man es zur grotesken Horror-Realität aufwerten ...
> :> Was davon kann C?
> :
> : Was kann man damit ausdr?cken, das man nicht in jeder
> : turing-Vollst?ndigen Sprache ausdr?cken kann?
>
> { (ascii + 72),
> (ascii + 105),
> (ascii + 108),
> (ascii + 102),
> (ascii + 114),
> (ascii + 101),
> (ascii + 105),
> (ascii + 99),
> (ascii + 104),
> (ascii + 101),
> (ascii + 115)
> }
>
> Jedes turing-vollstaendige setup koennte Speichersammlung
> bereitstellen. Wer/was schuetzt die Steuerung des Roentgen-Kastens
> davor, dass das jemand versehentlich genutzt hat?
Wovon sprichst Du?
> :> Das einzige, was Dir fehlt, sind gotos (braucht
> :> man die?)
>
> : ?Man? benutzt sie st?ndig, was vom Compiler mehr oder minder hinter
> : einem Feigenblatt verborgen wird.
>
> Sicher, aber "compiler" != "man".
Der Compiler tut aber nichts von alleine.
> Die Behauptungen, die in einem Programm-Quelltext enthalten sind,
> koennen glaube ich ohne Gesichtsverlust explizit gemacht werden,
Sie sind es bereits.
> zum Nutzen derer, die es nutzen, oder warten, oder pruefen.
> Das kann die Autoren selber betreffen.
Das nützt nichts: Wenn Du den Quellcode verändern möchtest, mußt Du
den vorher gelesen und verstanden haben.
Rainer Weikusat
> Rainer Weikusat <weik...@students.uni-mainz.de> writes:
> > Was kann man damit ausdrücken, das man nicht in jeder
> > turing-vollständigen Sprache ausdrücken kann?
>
> (Komplexere) Abstraktionen und (konzeptionelle) Zusammenhänge.
>
> Wenn alles, was man für komplexere Programme benötigen würde, eine
> beliebige turing-vollständige Sprache wäre, wäre C totaler Overkill. C
> unterstützt schon eine Menge Abstraktionen, die für
> Turing-Vollständigkeit vollkommen überflüssig sind.
Und?
> Ist C also bloatig? Nein? Wo genau ist dann die Grenze von sinnvollen
> Abstraktionen?
Es ging um notwendige Abstraktionen.
> It depends? Ah, und warum dann nicht Sprachen verwenden, die mehr
> Abstraktionsmittel als C zur Verfügung stellen (sofern man sie
> benötigt!)?
Weil einem diese Dinge real auch ohne spezifischen language support
zur Verfügung stehen.
Vinzent Hoefler
> Stefan Nobis <ste...@snobis.de> writes:
>> Rainer Weikusat <weik...@students.uni-mainz.de> writes:
>>
>> Ist C also bloatig? Nein? Wo genau ist dann die Grenze von sinnvollen
>> Abstraktionen?
>
> Es ging um notwendige Abstraktionen.
Wo genau ist die Grenze zwischen sinnvoll und notwendig? Die absolut
untere Grenze duerfte jedenfalls bei der Abstraktion Maschinencode ->
Mnemonic zu liegen.
>> It depends? Ah, und warum dann nicht Sprachen verwenden, die mehr
>> Abstraktionsmittel als C zur Verfügung stellen (sofern man sie
>> benötigt!)?
>
> Weil einem diese Dinge real auch ohne spezifischen language support
> zur Verfügung stehen.
Und alle Sprachen, die mehr Features als C zur Verfuegung stellen, sind
demzufolge Spielzeugsprachen? Ich kann Dir nicht ganz folgen, aber
bitte:
|function Get_Speed (Distance : in Meter;
| Time : in Seconds) return Speed;
Natuerlich *kann* man in C selbst darauf achten, dass man die Funktion
immer mit den richtigen Parametern aufruft und dass der Aufruf dieser
Funktion keine Seiteneffekte hat.
Aber warum sollte ich das auch noch muessen? Ich habe durchaus besseres
zu tun.
Vinzent.
--
Why is it that there are so many more horses' asses than there are
horses?
-- G. Gordon Liddy
Lutz Donnerhacke
> Natuerlich *kann* man in C selbst darauf achten, dass man die Funktion
> immer mit den richtigen Parametern aufruft und dass der Aufruf dieser
> Funktion keine Seiteneffekte hat.
Viel schlimmer ist es, jedesmal wieder das korrekte Taskingverhalten zu
implementieren. Klar, kann man das in Bibliotheken auslagern, aber ist das
dann noch C? Nein, die Bibliotheken gehören nicht zur Sprache, können also
nicht benutzt werden. Oder müssen selbst verifiziert werden.
Rainer Weikusat
> Rainer Weikusat wrote:
> > Vinzent Hoefler <JeLlyFish...@gmx.net> writes:
> >> Rainer Weikusat <weik...@students.uni-mainz.de> wrote:
> >> >Ich habe mich solange durch die website gewühlt, bis ich unter der
> >>
> >> Ich unterstreiche mal: "...mathematically proved the
> >> specification..."
> >
> > Wozu?
>
> Das hatte ich weiter unten ausgefuehrt.
Das muß mir dann entgangen sein.
> >> Wenn ich das jetzt mal frei interpretiere, akzeptierst Du damit den
> >> Tod von Menschen als aergerlich, aber tolerabel,
> >
> > Lieber Vinzent, ich glaube, ich lege Maßstäbe an Software an, die Du
> > Dir noch nicht einmal vorstellen kannst.
>
> Ehrlich gesagt, das *will* ich mir auch gar nicht vorstellen.
Dann bleibt zu hoffen, daß Dich jemand aus dem Verkehr zieht, bevor Du
wegen gemeingefährlicher Lernresistenz ein paar Menschen auf dem
Gewissen hast. Tut mir leid, aber das ist definitiv nicht mehr
komisch.
> >> waehrend es komisch waere, doch wenigstens zu versuchen, zu
> >> beweisen, dass das von der Software her (nahezu) ausgeschlossen
> >> werden kann, da das korrekte Verhalten der Software ohnehin im
> >> Quellcode steht?
> >
> > Falls Du zum Verständnis des Quellcodes irgendetwas anderes außer dem
> > Quellcode benötigst darfst Du aufhören, Dir darüber Sorgen zu machen.
>
> Das Verstaendnis des Quellcodes sagt nichts ueber seine Korrektheit
> aus.
Das «Verständnis» sagt per se gar nichts aus. Aber der Quelltext tut
das: Er ist eine vollständige Beschreibung dessen, was die Software zur
Laufzeit tun wird.
> Und es wohl kaum moeglich, ein 100'000 Zeilen-Programm vollstaendig zu
> verstehen und garantieren zu koennen, dass es das tut, was es tun soll,
> unter allen Umstaenden.
Es ist möglich, eine 100.000-Zeilen-Programm so zu konstruieren, daß
man keine Einheiten von mehr als maximal tausend Zeilen hat und so,
daß diese Einheiten keine internen Abhängigkeiten haben.
> >> Nein, ich halte auch vertrackte logische Fehler nicht fuer tolerabel.
> >> Und Korrektheitsbeweise koennen solche Fehler sicher finden, wenn sie
> >> ausserhalb der beschriebenen Spezifikation sind.
> >
> > «There's a killer on the loose again».
>
> Was willst Du damit sagen?
Die Grundvoraussetung für das, was ich geschrieben hatte
(«Tolerabilität von fringe case-Fehlersituationen»), ist, daß das
System deswegen nicht Amok läuft, was man durch einen geeigneten
internen Aufbau sicherstellt. Wenn das für Dich nicht
selbstverständlich ist, und diesen Eindruck erweckst Du gerade, bist
Du eine Gefahr für Deine Umgebung, deren Umfang ausschließlich von dem
Gefahrenpotential dessen, womit man Dich herumspielen läßt, limitiert
wird.
> It is easier to fit the specification to a program than vice versa?
Entweder das Programm ist eine Übersetzung der Spezifikation in eine
andere Sprache oder Du hast einen schrecklichen Fehler gemacht, der
sich auch mit 400t glue code im Nachhinein nicht mehr wird
reparieren lassen.
> >> >Es bleibt auch unklar, wer mir die Äquivalenz dessen, was bewiesen
> >> >wurde, mit dem Quelltext garantiert
> >>
> >> Der SPARK-Examiner. Der Beweis *ist* der Quelltext. Es gibt keinen
> >> zweiten Ordner mit vielen tollen Formeln dazu. Ein SPARK-Quelltext,
> >> dessen Korrektheit (in erster Linie heisst das frei von
> >> Laufzeitfehlern) nicht formal bewiesen werden kann, ist einfach kein
> >> gueltiges SPARK-Programm.
> >
> > Normale Leute nennen sowas einen Zirkelschluß.
>
> Und Leute, die sich ein klein wenig mit diesen Methoden beschaeftigt
> haben, wissen, dass die SPARK-Annotations nicht den ausfuehrenden Code
> darstellen. Ja, es ist redundant, nachdem der Examiner festgestellt
> hat, dass beides korreliert.
Lediglich wird von dem nicht erwartet, tatsächlich alle Fehler zu
finden, sondern bloß alle möglichen Fehler. Der Rest wird dann wieder
dem Programmierer überlassen. Falls man dem vorher nicht zutrauen
konnte, faktisch korrekten Code zu schreiben (insofern möglich), warum
sollte er es hinterher plötzlich können?
> >> Weil der Beweis auf formalen Methoden beruht,
> >> es duerfte von daher wesentlich leichter sein, die moeglicherweise
> >> vorhandenen Inkonsistenzen zu finden als das in einem beliebigen
> >> Quelltext der Fall waere.
> >
> > Vertrau mir: "Engineers learn quickly how to avoid warnings" wird von
> > fünf von zehn Fällen "den Kommentar kann ich grade nicht brauchen"
> > heißen.
>
> Tja, dann haben diese 50% ihren Beruf verfehlt.
>
> Du stimmst mir also zu, dass Fehler im Quellcode wesentlich schwerer zu
> finden sind als im Zuge einer formalen Beschreibung?
Wie käme ich denn dazu? Wegen einer formalen Beschreibung ohne Fehler
bekomme ich keinen Quelltext ohne Fehler, und (zum 1000x): Ein
Programm ist bereits eine formale Beschreibung.
> >> Unit-testing ist entfernt wohl das, was Du damit meintest:
> >>
> >> "Ein Programm mit mehr als fünfhundert Zeilen besteht aus sauber
> >> getrennten Subsystemen/ Modulen, die ausschließlich über
> >> definierte Interfaces kommunizieren und deren Interna unterhalb einer
> >> prozeduralen Spezifiaktion des Interfaces lokalisiert bleiben und
> >> jeder einzelne dieser Teile ist klein genug, damit man ihn separat
> >> debuggen kann."
> >> (<87n0lxjr...@winter.inter-i.wohnheim.uni-mainz.de>)
> >>
> >> So die Theorie und in den vielen Faellen mag das stimmen. Laut Rod
> >> (und ich glaube da einfach mal seiner Erfahrung) findet man die
> >> meisten Fehler aber, wenn man diese einzelnen Unit zusammenfuegen
> >> will, also letztendlich im Interface. Das ist im uebrigen auch meine
> >> Erfahrung.
> >
> > Das ist eine groteskte Horrortheorie,
>
> Diese Theorie stammt von Dir, danke.
Warum sollte ich mich denn vollkommen widersinnig auf meinen Text
beziehen anstelle auf Deinen?
> Oder meintest Du eher:
>
> IEEE Software Vol. 19, No. 1, Jan/Feb 2002:
>
> "Traditionally critical-systems testings is very expensive. A reason for
> this is that testing occurs several times: we test indivisual units,
> integrate them and test the integration, and then the system as whole.
> Our experience with previous safety-critical projects suggests that
> this approach is inefficient and particularly that unit testing is
> ineffective because most errors are interface errors, not internal
> errors in units.
Bei allen Dingen, mit denen ich praktisch zu tun habe, und dazu gehört
Quellcode anderer Leute mit dazu, verhält sich das genau umgekehrt, dh
der Code tut nicht das, was das Interface angeblich bereitstellt.
> > deren Implikationen ausschließlich besagen, daß die Resultate
> > lebensgefährlich sein werden.
>
> Interessant. Wie kommst Du darauf?
Ich denke nicht, daß ich das Dir in einem Usenet-angemessenen Rahmen
erklären kann, aber jedenfalls würde ich nie so wahnsinnig sein, mein
Leben einem Computerprogramm anzuvertrauen, auf das diese Aussage
zutrifft, falls ich nicht ohnehin Hazard spiele.
> Tu das.
>
> >> >> >> Spielzeugsprache? http://www.sparkada.com
> [...]
> >> > * SPARK Language Features
> [...]
> >>
> >> Was davon kann C?
> >
> > Was kann man damit ausdrücken, das man nicht in jeder
> > turing-vollständigen Sprache ausdrücken kann?
>
> Eine Registermaschine ist auch turing-vollstaendig. Warum also C?
C-Programme beschreiben normalerweise Registermaschinen.
> Ich bin immer noch nicht ganz dahintergekommen, was Du mit
> Spielzeugsprache meinst.
ZB eine ohne dynamische Speicherverwaltung und ohne
Rekursionen. Insbesondere letzteres mutet abstrus an, denn gerade
rekursive Algorithmen kann man oft einfach durch Induktion beweisen.
> Eine Sprache, die es einfacher macht, korrekten Code zu schreiben,
> weil das dann ja jedes Kind tun kann?
Wie bereits erwähnt: Ich möchte nicht mein Leben einem Programm von
jemandem anvertrauen, dem es «kompliziert» erscheint,
integer-Überläufe im Quelltext sinnvoll zu behandeln und der ein
Spezialtool braucht, um potentielle zu finden. Dazu gibt es zuviele
esoterische Fehlermöglichkeiten.
> Dein Problem, ich schreibe keine Software, um mit Compiler und
> Debugger zu kaempfen, ich schreibe Software, um etwas zum Laufen zu
> bekommen.
Vermutlich wäre «davonlaufen» anzuraten.
> >> Das einzige, was Dir fehlt, sind gotos (braucht
> >> man die?)
> >
> > «Man» benutzt sie ständig, was vom Compiler mehr oder minder hinter
> > einem Feigenblatt verborgen wird.
>
> *Das* weiss ich selbst.
Warum fragst Du dann? Du weißt sicher auch, daß die meisten
Kontrollstrukturen prinzipiell redundant sind und der Bequemlichkeit/
Übersichtlichkeit halber verwendet werden.
----------------------
p = pacct->gr_mem;
while (1) {
if (!*p) break;
if (strcmp(*p, user->pw_name) == 0) {
if (argv[1]) log_access(user->pw_name, argv + 1, argc - 1);
goto found;
}
++p;
}
setuid(uid);
}
found:
execve(COMMAND, argv, env);
perror("execve");
----------------------
Für goto gilt das desgleichen.
> > Obiges gilt entsprechend: Objekte im RAM haben eine Adresse, die die
> > CPU benutzt, um sie zu adressieren.
>
> Und? Deswegen muss ich das Objekt auf Source-Ebene nicht mit seiner
> Adresse ansprechen.
>
> Da kannst Du auch gleich wieder Assembler programmieren.
Das Gegenteil von A ist !A und nicht B. Es bringt nichts, die Adressen
wegzuabstrahieren, also wozu tun?
> >> Was ich mit SHOLIS meinte: Wenn mit SPARK ein System beschreiben
> >> kann, welches die sicherheitskritische Software eines Helikopters
> >> darstellt,
> >
> > Es ist «bewiesen», daß man so ein System in Visual Basic beschreiben
> > kann.
>
> So, kann man das?
Ja und zwar wegen 'turing vollständig'.
Stefan Nobis
> Das «Verständnis» sagt per se gar nichts aus. Aber der Quelltext tut
> das: Er ist eine vollständige Beschreibung dessen, was die Software zur
> Laufzeit tun wird.
Davon träumst du, oder?
Dein Programm nutzt Bibliotheksfunktionen, greift auf Syscalls zurück,
läuft auf komplexen ICs usw. Und in derart umfangreichen und komplexen
Systemen hälst du einen Quelltext für eine *vollständige* Beschreibung
dess, was das Programm zur Laufzeit (also der durch das compilierte
Programm im Prinzip beschriebene Task) tut?
Aberwitziger Unsinn!
> dem Programmierer überlassen. Falls man dem vorher nicht zutrauen
> konnte, faktisch korrekten Code zu schreiben (insofern möglich), warum
> sollte er es hinterher plötzlich können?
Wenn es um kritische Systeme geht, kann man getrost davon ausgehen,
dass *kein* einziger Mensch jemals korrekten, sprich 100%
fehlerfreien, Code schreibt.
Ziel muss es also sein, einerseits Fehler verstärkt zu vermeiden und
es gibt Möglichkeiten, die (durchschnittliche) Fehlerquote beim
Programmieren mit diversen Mitteln zu reduzieren. Andererseits
versucht man möglichst automatisiert Fehler zu finden -- dazu ist
natürlich ein Mindestmaß an Redundanz notwendig (dies beruht auf der
Annahme, dass in hinreichend unterschiedlichen Beschreibungssystemen
Menschen nicht dieselben Detailfehler machen -- die Erfahrung legt
nahe, dass dies stimmt; wie gesagt Detailfehler; grundlegendere
(logische) Fehler wird man so sicher kaum finden, dafür hat man dann
die Leute, die grundlegende Elemente/Algorithmen des Systems auf
Korrektheit prüfen und diese auch Beweisen -- und dies durch
Peer-Review kontrollieren lassen).
> Wegen einer formalen Beschreibung ohne Fehler
> bekomme ich keinen Quelltext ohne Fehler, und (zum 1000x):
Natürlich nicht.
> Ein Programm ist bereits eine formale Beschreibung.
Aber auf einem völlig anderen Abstraktionsniveau. Auf diese Weise
bekomme ich etliche neue Fehlerquellen.
Wenn nun die nicht-quelltext Spezifikation auf höherem
Abstraktionsniveau nachgewiesen fehlerfrei ist/wäre, so muss ich im
Quelltext nur noch auf unterster Ebene nach Detailfehlern bei der
Umsetzung suchen und nicht mehr auf jeder Ebene auf Fehler achten.
Dies wirkt sich auch auf verschiedene Weise aus: Ein Peer-Review ist
evtl. auf breiterer Basis möglich, abstraktere Konzepte und Module
lassen sich (bei evtl. unterschiedlicher Implementation) leichter
wiederverwenden, durch verschiedene Ausdrucksformen fallen
evtl. eher/mehr Fehler auf etc.
> > Eine Registermaschine ist auch turing-vollstaendig. Warum also C?
> C-Programme beschreiben normalerweise Registermaschinen.
So ein Quark. C basiert noch nicht einmal auf einer klaren
Maschinenbeschreibung (wie z.B. Lisp) und noch viel weniger
beschreiben C Programme eine Registermaschine (welchen Sinn sollte das
auch machen) -- du selbst hast doch gesagt, Quelltext beschreiben, was
zur Laufzeit passiert. Wie sollen sie außerdem auch noch Maschinen
beschreiben?
[Spielzeugsprache]
> ZB eine ohne dynamische Speicherverwaltung und ohne
> Rekursionen. Insbesondere letzteres mutet abstrus an, denn gerade
> rekursive Algorithmen kann man oft einfach durch Induktion beweisen.
[...]
> Wie bereits erwähnt: Ich möchte nicht mein Leben einem Programm von
> jemandem anvertrauen, dem es «kompliziert» erscheint,
> integer-Überläufe im Quelltext sinnvoll zu behandeln und der ein
> Spezialtool braucht, um potentielle zu finden. Dazu gibt es zuviele
> esoterische Fehlermöglichkeiten.
Und eben weil es viele esoterische Fehlermöglichkeiten gibt, sollte
man alle Möglichkeiten, Fehler zu vermeiden, nutzen. Wieso nicht
gleich eine Sprache, bei der etliche Fehlerklassen (z.B. wilde Zeiger)
schlicht unmöglich sind?
Wieso sind einige Abstraktionskonzepte, wie Rekursionen u.a., wichtig
und gut und andere wieder völlig überflüssig und böse?
> > > Obiges gilt entsprechend: Objekte im RAM haben eine Adresse, die die
> > > CPU benutzt, um sie zu adressieren.
> > Und? Deswegen muss ich das Objekt auf Source-Ebene nicht mit seiner
> > Adresse ansprechen.
> > Da kannst Du auch gleich wieder Assembler programmieren.
> Das Gegenteil von A ist !A und nicht B. Es bringt nichts, die Adressen
> wegzuabstrahieren, also wozu tun?
Um Fehlerquellen zu vermeiden. Mit Adressen, zumal ihrer
Repräsentation(!) in C, kann man rechnen, mit Referenzen (einer
anderen Repräsentation) kann man nicht rechnen -- damit sind wilde
Zeiger z.B. (nahezu) unmöglich. Eine komplette Klasse von Fehler
ausgemerzt. Und das ist jetzt noch mal aus welchem Grund schlecht?
--
Stefan.
Rainer Weikusat
> Rainer Weikusat wrote:
> > Stefan Nobis <ste...@snobis.de> writes:
> >> Ist C also bloatig? Nein? Wo genau ist dann die Grenze von sinnvollen
> >> Abstraktionen?
> >
> > Es ging um notwendige Abstraktionen.
>
> Wo genau ist die Grenze zwischen sinnvoll und notwendig?
Falls ich concurrency brauche (oder auch nur benutzen möchte), brauche
ich notwendigerweise einen Mechanismus dafür. Sowohl C als auch Ada
bieten das und in beiden Fällen ist es Bestandteil des
Laufzeitsystems, falls vorhanden: In Ada deswegen, weil eine konkrete
Semantik vorgeschrieben ist, in C, weil keine konkrete Semantik
verboten wird.
> >> It depends? Ah, und warum dann nicht Sprachen verwenden, die mehr
> >> Abstraktionsmittel als C zur Verfügung stellen (sofern man sie
> >> benötigt!)?
> >
> > Weil einem diese Dinge real auch ohne spezifischen language support
> > zur Verfügung stehen.
>
> Und alle Sprachen, die mehr Features als C zur Verfuegung stellen, sind
> demzufolge Spielzeugsprachen? Ich kann Dir nicht ganz folgen,
Dann solltest Du etwas mehr auf meine Worte hören, anstatt meine
wahrscheinlichen Gedanken zu erraten versuchen.
> aber
> bitte:
>
> |function Get_Speed (Distance : in Meter;
> | Time : in Seconds) return Speed;
>
> Natuerlich *kann* man in C selbst darauf achten, dass man die Funktion
> immer mit den richtigen Parametern aufruft und dass der Aufruf dieser
> Funktion keine Seiteneffekte hat.
Man kann auch stattdessen einen vernünftigen Entwurf machen:
double get_speed(double distance)¹
{
static double last_distance = -1;
static uint32_t last_time = 0;
Alternativ
struct dist_info {
uint32_t last_time;
double last_pos;
};
double get_speed(struct dist_info *info, double distance)
1) Ein Subsystem ist äquivalent zu einem Objekt, von dem es genau eine
Instanz gibt. Aus dem Umkehrschluß folgt außerdem, das
hemmungsloser Gebrauch globaler Variablen immer noch sehr populär
ist.
> Aber warum sollte ich das auch noch muessen? Ich habe durchaus besseres
> zu tun.
Wolltest Du jetzt damit andeuten, Du hättest durchaus besseres zu tun,
als semantisch richtigen Code zu schreiben, oder eher, es würde Dich
übermäßig viel Mühe kosten, die Reihenfolge zweier Parameter zu
behalten oder zu korrigieren? :->
Ich wage die Behauptung, daß überkomplexe (also -generalisierte :->)
Interfaces für mehr Fehler verantwortlich sind, als integer-Überläufe,
sowie, daß diese Fehler außerdem schwerer zu finden sind. Das
Zwei-Parameer-Beispiel ist natürlich etwas konstruiert, aber tools,
die schlechte Entwürfe einfacher handhabbar machen, halte ich nicht
für notwendig.
Vinzent Hoefler
> Vinzent Hoefler <JeLlyFish...@gmx.net> writes:
>> Rainer Weikusat wrote:
>> > Vinzent Hoefler <JeLlyFish...@gmx.net> writes:
>> >> Rainer Weikusat <weik...@students.uni-mainz.de> wrote:
>
>> >> Wenn ich das jetzt mal frei interpretiere, akzeptierst Du damit
>> >> den Tod von Menschen als aergerlich, aber tolerabel,
>> >
>> > Lieber Vinzent, ich glaube, ich lege Maßstäbe an Software an, die
>> > Du Dir noch nicht einmal vorstellen kannst.
>>
>> Ehrlich gesagt, das *will* ich mir auch gar nicht vorstellen.
>
> Dann bleibt zu hoffen, daß Dich jemand aus dem Verkehr zieht, bevor Du
> wegen gemeingefährlicher Lernresistenz ein paar Menschen auf dem
> Gewissen hast.
Eher andersrum.
> Tut mir leid, aber das ist definitiv nicht mehr komisch.
Eben. Aber Deinen Aussagen nach zu urteilen, die darauf schliessen
lassen, dass Du ausschliesslich dem "faehigen Programmierer" vertraust,
koennen Deine Massstaebe an Software nicht allzu hoch sein.
>> Das Verstaendnis des Quellcodes sagt nichts ueber seine Korrektheit
>> aus.
>
> Das «Verständnis» sagt per se gar nichts aus. Aber der Quelltext tut
> das: Er ist eine vollständige Beschreibung dessen, was die Software
> zur Laufzeit tun wird.
Nein, diese Beschreibung ist mitnichten vollstaendig. Was tut das
System, wenn die Software einen Zeiger dereferenziert, der auf ein
zufaellig bereits freigegebenes Objekt zeigt? Was passiert, wenn mit
den Ergebnissen aus uninitialisierten Variablen gerechnet wird? Das
ganze ist nicht einmal mehr deterministisch, was willst Du da mit dem
Source anfangen?
Und *Du* kannst bei 100KSLOC *garantieren*, dass keiner dieser Fehler
auftritt?
>> Und es wohl kaum moeglich, ein 100'000 Zeilen-Programm vollstaendig
>> zu verstehen und garantieren zu koennen, dass es das tut, was es tun
>> soll, unter allen Umstaenden.
>
> Es ist möglich, eine 100.000-Zeilen-Programm so zu konstruieren, daß
> man keine Einheiten von mehr als maximal tausend Zeilen hat und so,
> daß diese Einheiten keine internen Abhängigkeiten haben.
Ja. Was nicht heisst, dass es nachher funktioniert.
> Die Grundvoraussetung für das, was ich geschrieben hatte
> («Tolerabilität von fringe case-Fehlersituationen»), ist, daß das
> System deswegen nicht Amok läuft, was man durch einen geeigneten
> internen Aufbau sicherstellt.
Und in SPARK durch den Beweis der Abwesenheit von Laufzeitfehlern
garantieren kann.
> Wenn das für Dich nicht selbstverständlich ist,
Das ist fuer mich durchaus selbstverstaendlich. Was fuer mich nicht
selbstverstaendlich ist, wie das in irgendeiner Weise korrekte Software
garantieren soll.
> und diesen Eindruck erweckst Du gerade, bist
> Du eine Gefahr für Deine Umgebung,
Das bezweifle ich.
> deren Umfang ausschließlich von dem
> Gefahrenpotential dessen, womit man Dich herumspielen läßt,
:-)
>> It is easier to fit the specification to a program than vice versa?
>
> Entweder das Programm ist eine Übersetzung der Spezifikation in eine
> andere Sprache oder Du hast einen schrecklichen Fehler gemacht, der
> sich auch mit 400t glue code im Nachhinein nicht mehr wird
> reparieren lassen.
Sorry, entweder Du traeumst oder Du bist einer von denen, die immer auf
Anhieb korrekte, der Spezifikation entsprechende Software schreiben
koennen. Wieviele Fehler hast Du im Durchschnitt pro Tausend Zeilen
Code?
BTW, auch die Spezifikation kann falsch sein bzw. Inkonsistenzen haben.
Beim MultOS-CA hat man 38 Fehler aus der Spezifikationsphase erst in
der Kodierphase gefunden und einen waehrend der Operation.
>> Und Leute, die sich ein klein wenig mit diesen Methoden beschaeftigt
>> haben, wissen, dass die SPARK-Annotations nicht den ausfuehrenden
>> Code darstellen. Ja, es ist redundant, nachdem der Examiner
>> festgestellt hat, dass beides korreliert.
>
> Lediglich wird von dem nicht erwartet, tatsächlich alle Fehler zu
> finden, sondern bloß alle möglichen Fehler.
Richtig.
> Der Rest wird dann wieder dem Programmierer überlassen.
Natuerlich.
> Falls man dem vorher nicht zutrauen
> konnte, faktisch korrekten Code zu schreiben (insofern möglich), warum
> sollte er es hinterher plötzlich können?
Weil Menschen Fehler machen. Aber das solltest Du wissen.
>> Du stimmst mir also zu, dass Fehler im Quellcode wesentlich schwerer
>> zu finden sind als im Zuge einer formalen Beschreibung?
>
> Wie käme ich denn dazu? Wegen einer formalen Beschreibung ohne Fehler
> bekomme ich keinen Quelltext ohne Fehler,
In SPARK hast Du sehr gute Chancen dazu.
> und (zum 1000x): Ein Programm ist bereits eine formale Beschreibung.
LOL
Ein formale Beschreibung, deren Konsistenz Du bitte *wie* nachweist?
Durch Code-Reviews durch andere Programmierer, die Du hier
offensichtlich als unfaehig hinstellst?
>> >> "Ein Programm mit mehr als fünfhundert Zeilen besteht aus sauber
>> >> getrennten Subsystemen/ Modulen, die ausschließlich über
>> >> definierte Interfaces kommunizieren und deren Interna unterhalb
>> >> einer prozeduralen Spezifiaktion des Interfaces lokalisiert
>> >> bleiben und jeder einzelne dieser Teile ist klein genug, damit man
>> >> ihn separat debuggen kann."
>> >> (<87n0lxjr...@winter.inter-i.wohnheim.uni-mainz.de>)
>> >>
>> >> So die Theorie und in den vielen Faellen mag das stimmen. Laut Rod
>> >> (und ich glaube da einfach mal seiner Erfahrung) findet man die
>> >> meisten Fehler aber, wenn man diese einzelnen Unit zusammenfuegen
>> >> will, also letztendlich im Interface. Das ist im uebrigen auch
>> >> meine Erfahrung.
>> >
>> > Das ist eine groteskte Horrortheorie,
>>
>> Diese Theorie stammt von Dir, danke.
>
> Warum sollte ich mich denn vollkommen widersinnig auf meinen Text
> beziehen anstelle auf Deinen?
Weil ich auf Deinen Text bezogen "So die Theorie" schrieb.
>> Oder meintest Du eher:
>>
>> IEEE Software Vol. 19, No. 1, Jan/Feb 2002:
>>
>> "Traditionally critical-systems testings is very expensive. A reason
>> for this is that testing occurs several times: we test indivisual
>> units, integrate them and test the integration, and then the system
>> as whole. Our experience with previous safety-critical projects
>> suggests that this approach is inefficient and particularly that unit
>> testing is ineffective because most errors are interface errors, not
>> internal errors in units.
>
> Bei allen Dingen, mit denen ich praktisch zu tun habe, und dazu gehört
> Quellcode anderer Leute mit dazu, verhält sich das genau umgekehrt, dh
> der Code tut nicht das, was das Interface angeblich bereitstellt.
Dann solltest Du die Leute grundsaetzlich wegen Unfaehigkeit feuern.
Oder was genau ware es noch mal, was Du oben aussagen wolltest?
Unfaehige Programmierer?
>> > deren Implikationen ausschließlich besagen, daß die Resultate
>> > lebensgefährlich sein werden.
>>
>> Interessant. Wie kommst Du darauf?
>
> Ich denke nicht, daß ich das Dir in einem Usenet-angemessenen Rahmen
> erklären kann, aber jedenfalls würde ich nie so wahnsinnig sein, mein
> Leben einem Computerprogramm anzuvertrauen, auf das diese Aussage
> zutrifft, falls ich nicht ohnehin Hazard spiele.
Irgendwie habe ich jetzt was nicht ganz begriffen. Die Nutzung formaler
Verifikationstechniken impliziert Lebensgefaehrlichkeit des Produkts?
Oder meintest Du, wenn die Lebensgefaehrlichkeit des Produkts durch
formale Methoden bewiesen ist?
Ansonsten, steige bitte nie wieder in ein Flugzeug, vor allem nie weider
in eine Boeing. Das ist lebensgefaehrlich. Die Software haben nicht nur
unfaehige Idioten geschrieben, die zu bloed sind, Integer-Ueberlaeufe
schon im Source zu erkennen, sondern diese Software ist auch noch
zertifiziert.
>> Ich bin immer noch nicht ganz dahintergekommen, was Du mit
>> Spielzeugsprache meinst.
>
> ZB eine ohne dynamische Speicherverwaltung
Brauche ich wirklich selten. Und in Embedded Systems- bzw.
Safety-Critical-Umgebungen will man das auch nicht. Es wird Dir in den
seltensten Faellen gelingen, nachzuweisen, dass Deine Techniken nicht
zu Speicherfragmentierung und/oder Memory-Leaks fuehren.
> und ohne Rekursionen.
Der SPARK-Examiner selbst ist in SPARK geschrieben. Und ja, der Parser
ist statisch verifiziert und benutzt weder Rekursion noch dynamischen
Speicher. Rod war natuerlich durchaus der Meinung, dass das nicht sehr
einfach war.
> Insbesondere letzteres mutet abstrus an, denn gerade
> rekursive Algorithmen kann man oft einfach durch Induktion beweisen.
Auch deren Stackverbrauch, bevor die Runtime-Umgebung ein Storage_Error
ausloest (oder halt nicht)?
>> Eine Sprache, die es einfacher macht, korrekten Code zu schreiben,
>> weil das dann ja jedes Kind tun kann?
>
> Wie bereits erwähnt: Ich möchte nicht mein Leben einem Programm von
> jemandem anvertrauen, dem es «kompliziert» erscheint,
> integer-Überläufe im Quelltext sinnvoll zu behandeln
Falls Du das auf mich beziehst: Beispiele sind naturgemaess stark
vereinfacht.
> und der ein
> Spezialtool braucht, um potentielle zu finden.
Wenn Du das so meinst. Demzufolge sollten sicherheitskritische Programme
in moeglichst schwierigen, unsicheren Sprachen geschrieben werden,
damit da auch ja nur die absolut fehlerfrei arbeitende Elite daran
arbeitet?
Oder was wolltest Du sagen?
> Dazu gibt es zuviele esoterische Fehlermöglichkeiten.
Eben diese versucht das Tool zu finden, indem es *alle* Moeglichkeiten
durchgeht. Ein gegebenes Register hat nur eine endliche Zahl von
Bitmustern.
>> Dein Problem, ich schreibe keine Software, um mit Compiler und
>> Debugger zu kaempfen, ich schreibe Software, um etwas zum Laufen zu
>> bekommen.
>
> Vermutlich wäre «davonlaufen» anzuraten.
Kaum. Das interessante ist, dass es in der Mehrzahl der Faelle zum
Run-Once-Never-Touch-Again-Syndrom kommt. Debugger brauche ich sehr
selten.
>> >> Das einzige, was Dir fehlt, sind gotos (braucht
>> >> man die?)
>> >
>> > «Man» benutzt sie ständig, was vom Compiler mehr oder minder hinter
>> > einem Feigenblatt verborgen wird.
>>
>> *Das* weiss ich selbst.
>
> Warum fragst Du dann?
Weil es eine Frage nach den expliziten gotos war, nicht nach
irgendwelchen Kontrollstrukturen.
> Du weißt sicher auch, daß die meisten
> Kontrollstrukturen prinzipiell redundant sind und der Bequemlichkeit/
> Übersichtlichkeit halber verwendet werden.
Ja.
> ----------------------
> p = pacct->gr_mem;
> while (1) {
> if (!*p) break;
> if (strcmp(*p, user->pw_name) == 0) {
> if (argv[1]) log_access(user->pw_name, argv +
> 1, argc - 1); goto found;
> }
>
> ++p;
> }
>
> setuid(uid);
> }
>
> found:
> execve(COMMAND, argv, env);
> perror("execve");
> ----------------------
Warum nicht so (den Rest nach dem goto-Label spare ich mir mal),
ungefaehr zumindest:
for i in P'Range loop
if (P (i) = NULL) then
Set_UID (uid);
exit;
end if;
if (P (i) = User.PW_Name) then
if (Argument (1) /= "") then
Log_Access (User.PW_Name, Argument (1), Argument_Count);
exit;
end if;
end if;
end loop;
Die zwei Exits sind etwas unschoen, aber ich denke, ich habe sowohl Dein
break als auch Dein goto ordentlich umgesetzt. Schlimmer sieht es
jedenfalls erst einmal auch nicht aus. Habe ich was uebersehen?
Zugegeben, zu den Parametern zu Log_Access gibt es keine direkte
Entsprechung, da Argument () halt eine einen String zurueckliefernde
Funktion ist und nicht irgendeine Adresse auf irgendwelchen Speicher,
der zufaelligerweise die Kommandozeile beinhaltet.
> Für goto gilt das desgleichen.
Ja. Wer hatte das gleich noch mal bewiesen, als die goto-befuerworter
das anzweifelten?
> Das Gegenteil von A ist !A und nicht B. Es bringt nichts, die Adressen
> wegzuabstrahieren,
Aber sicher bringt das etwas.
> also wozu tun?
Deswegen:
|void something (char* blabla)
vs.
|procedure Something (BlaBla : in Char_Array);
vs
|procedure Something (Blabla : out Char_Array);
Jetzt versuche mal, den drei Funktionen eine Nullzeiger zu uebergeben
und bei der C-Variante zu erzaehlen, ob blabla veraendert wird.
Manchmal sind Abstraktionen der bessere Weg.
Vinzent.
--
The world is an 8000 mile in diameter spherical pile of shit.
Vinzent Hoefler
> Vinzent Hoefler <JeLlyFish...@gmx.net> writes:
>> Rainer Weikusat wrote:
>> > Stefan Nobis <ste...@snobis.de> writes:
>> >> Ist C also bloatig? Nein? Wo genau ist dann die Grenze von
>> >> sinnvollen Abstraktionen?
>> >
>> > Es ging um notwendige Abstraktionen.
>>
>> Wo genau ist die Grenze zwischen sinnvoll und notwendig?
>
> Falls ich concurrency brauche (oder auch nur benutzen möchte), brauche
> ich notwendigerweise einen Mechanismus dafür.
Allein das Typ- oder Parameteruebergabekonzept ist eine Abstraktion. Und
*die* hilft.
> Sowohl C als auch Ada
> bieten das und in beiden Fällen ist es Bestandteil des
> Laufzeitsystems, falls vorhanden: In Ada deswegen, weil eine konkrete
> Semantik vorgeschrieben ist, in C, weil keine konkrete Semantik
> verboten wird.
Was Dir dazu verhilft, dass Du je nach Zielsystem eine andere Semantik
geboten bekommst.
>> aber
>> bitte:
>>
>> |function Get_Speed (Distance : in Meter;
>> | Time : in Seconds) return Speed;
>>
>> Natuerlich *kann* man in C selbst darauf achten, dass man die
>> Funktion immer mit den richtigen Parametern aufruft und dass der
>> Aufruf dieser Funktion keine Seiteneffekte hat.
>
> Man kann auch stattdessen einen vernünftigen Entwurf machen:
>
> double get_speed(double distance)¹
> {
> static double last_distance = -1;
> static uint32_t last_time = 0;
Vernuenftig, wenn man nur noch mit einer globalen Zeit arbeitet? Sorry.
Null Punkte.
> Alternativ
>
> struct dist_info {
> uint32_t last_time;
> double last_pos;
> };
>
> double get_speed(struct dist_info *info, double distance)
Besser, aber benoetigt hier schon wieder unsinnigerweise den Einsatz von
Zeigern und in diesem Fall sagt mir das auch Interface nicht, ob
dist_info nicht evt. veraendert werden koennte. Und das Ergebnis von
get_speed kann immer noch einer distance-Variablen zugewiesen werden.
Ehrlich, warum soll ich mir so etwas auf Dauer antun, wenn ich das in
anderen Sprachen viel einfacher und zum Nulltarif haben kann?
> 1) Ein Subsystem ist äquivalent zu einem Objekt, von dem es genau eine
> Instanz gibt. Aus dem Umkehrschluß folgt außerdem, das
> hemmungsloser Gebrauch globaler Variablen immer noch sehr populär
> ist.
Globale Variablen sind boese. Ja, das ist zu pauschal, ich weiss.
> Wolltest Du jetzt damit andeuten, Du hättest durchaus besseres zu tun,
> als semantisch richtigen Code zu schreiben,
Nein, denn genau darum geht es mir. Ich moechte semantisch korrekten
Code schreiben. Und wenn mich der Compiler auf Tippfehler oder
meinetwegen auch logische Fehler, die immer mal wieder passieren,
hinweist, steigert das meine Produktivitaet, weil ich den Fehler dann
nicht erst Tage spaeter nach drei Naechten debugging finde.
Aber Dir ist sicher noch nie an der falschen Stelle ein Semikolon
abhanden gekommen, oder?
> oder eher, es würde Dich
> übermäßig viel Mühe kosten, die Reihenfolge zweier Parameter zu
> behalten oder zu korrigieren? :->
Tja, *ich* verwechsle z.B. nach wie vor die Parameter bei memcpy (). Ich
kann mir das einfach nicht abgewoehnen. Und ja, es ist tatsaechlich
ziemlich viel Muehe, sich von einem Projekt zum anderen immer die
Reihenfolge irgendwelcher Parameter von Funktionen zu merken, die
andere geschrieben haben. Zumal wenn diese anderen dieses Interface
gelegentlich aendern.
> Ich wage die Behauptung, daß überkomplexe (also -generalisierte :->)
> Interfaces für mehr Fehler verantwortlich sind, als integer-Überläufe,
> sowie, daß diese Fehler außerdem schwerer zu finden sind.
Njet. In C bemerkt man die Ueberlaeufe halt nicht. Und es macht ja auch
nichts, mal fix im Array einen daneben zu greifen, wenn es nicht gerade
segfaultet.
> Das
> Zwei-Parameer-Beispiel ist natürlich etwas konstruiert,
Ok, anderes:
|Mem_Copy (Src => From_This;
| Dest => To_That;)
Da muss ich mir gar keine Gedanken mehr machen. Dort weiss, *dass* es
korrekt ist, ohne in die Deklaration schauen zu muessen.
> aber tools,
> die schlechte Entwürfe einfacher handhabbar machen, halte ich nicht
> für notwendig.
Ganz im Gegenteil. SPARK fordert sogar einen sehr guten Entwurf, weil
sonst der Bedarf an generierten VCs exponentiell ansteigt und Du ewig
und drei Tage auf Deinen Beweis warten kannst.
Vinzent.
Rainer Weikusat
> Rainer Weikusat wrote:
> > Sowohl C als auch Ada bieten das und in beiden Fällen ist es
> > Bestandteil des Laufzeitsystems, falls vorhanden: In Ada deswegen,
> > weil eine konkrete Semantik vorgeschrieben ist, in C, weil keine
> > konkrete Semantik verboten wird.
>
> Was Dir dazu verhilft, dass Du je nach Zielsystem eine andere Semantik
> geboten bekommst.
Ja.
> >> aber
> >> bitte:
> >>
> >> |function Get_Speed (Distance : in Meter;
> >> | Time : in Seconds) return Speed;
> >>
> >> Natuerlich *kann* man in C selbst darauf achten, dass man die
> >> Funktion immer mit den richtigen Parametern aufruft und dass der
> >> Aufruf dieser Funktion keine Seiteneffekte hat.
> >
> > Man kann auch stattdessen einen vernünftigen Entwurf machen:
> >
> > double get_speed(double distance)¹
> > {
> > static double last_distance = -1;
> > static uint32_t last_time = 0;
>
> Vernuenftig, wenn man nur noch mit einer globalen Zeit arbeitet?
Das kommt darauf an, wofür man die verwendet.
> > Alternativ
> >
> > struct dist_info {
> > uint32_t last_time;
> > double last_pos;
> > };
> >
> > double get_speed(struct dist_info *info, double distance)
>
> Besser, aber benoetigt hier schon wieder unsinnigerweise den Einsatz von
> Zeigern
s/un//
> Aber Dir ist sicher noch nie an der falschen Stelle ein Semikolon
> abhanden gekommen, oder?
>
> > oder eher, es würde Dich
> > übermäßig viel Mühe kosten, die Reihenfolge zweier Parameter zu
> > behalten oder zu korrigieren? :->
>
> Tja, *ich* verwechsle z.B. nach wie vor die Parameter bei memcpy ().
Simpel: Andersherum.
Vinzent Hoefler
> Vinzent Hoefler <JeLlyFish...@gmx.net> writes:
>> Rainer Weikusat wrote:
>>
>> > double get_speed(double distance)¹
>> > {
>> > static double last_distance = -1;
>> > static uint32_t last_time = 0;
>>
>> Vernuenftig, wenn man nur noch mit einer globalen Zeit arbeitet?
>
> Das kommt darauf an, wofür man die verwendet.
Sicher. Allerdings entzieht sich meinem Verstaendnis, inwieweit Du hier
eine globale Zeit voraussetzt. Wenn ich das getan haette, hiesse die
Funktion get_current_speed (). :-)
Ohnehin sind Funktionen in SPARK aber seiteneffektfrei. Das waere sie
hier nicht. Wobei das in Hinblick auf C ohnehin eine eher theoretische
Betrachtung ist, weil es die Unterscheidung zwischen Funktion, die
einen Wert zurueckliefert und einer Prozedur, die den Zustand des
Systems aendert, ohnehin nicht wirklich gibt.
>> > Alternativ
>> >
>> > struct dist_info {
>> > uint32_t last_time;
>> > double last_pos;
>> > };
>> >
>> > double get_speed(struct dist_info *info, double distance)
>>
>> Besser, aber benoetigt hier schon wieder unsinnigerweise den Einsatz
>> von Zeigern
>
> s/un//
Nein, dies ist lediglich bedingt durch die Einschraenkung von C, welches
keine Parametermodi kennt. Insofern ist es zwar notwendig, aber
keineswegs sinnvoll.
>> Tja, *ich* verwechsle z.B. nach wie vor die Parameter bei memcpy ().
>
> Simpel: Andersherum.
Und dann habe ich wieder das gleiche Problem. War es nun andersherum
oder nicht?
Aus dem Kopf: 1: source, 2: dest, oder?
Und ja, das ist fehleranfaellig. Schliesslich geht es nicht nur um
memcpy.
Vinzent.
--
All a hacker needs is a tight PUSHJ, a loose pair of UUOs, and a warm
place to shift.
Georg Bauhaus
: denn daf?r ist sie da. Ich mu? allerdings gestehen, Dir nicht ganz
: folgen zu k?nnen.
Ich wollte andeuten, dass es nicht mehr einfach ist, die Bedeutung
einer Hochsparchen-Operation im Detail pruefen oder vorher sagen
zu koennen:
In einem nebenlaeufigen Programm sei '=' im Quellcode angetroffen.
Was genau, im hinblick auf die betroffenen Daten (lhs, rhs),
im Hinblick auf die betroffenen Programm-Teile,
im HInblick auf die Stack-Nutzung,
im Hinblick auf die heap-Nutzung,
im Hinblick auf die waehrend '=' ablaufenden clock ticks,
bedeutet '='?
Faellt es dir hier so leicht, sagen wir innerhalb von 2 min,
diese Angaben fuer einen Echtwelt-Wartungsfall zu machen?
Waere es so falsch, ein tool ein zu setzen, dass ermoeglicht,
einem '=' Beschraenkungen auf zu erlegen, die solche Fragen
leichter und zuverlaessiger zu beantworten erlaubt?
:> Jedes turing-vollstaendige setup koennte Speichersammlung
:> bereitstellen. Wer/was schuetzt die Steuerung des Roentgen-Kastens
:> davor, dass das jemand versehentlich genutzt hat?
: Wovon sprichst Du?
EIn Roentgen-Geraet hat eine Bestrahlungs-Dauer die nicht ueberschritten
werden darf. Sollte in einem Programm garbage collection erlaubt
sein kann dabei Zeit drauf gehen, vielleicht im falschen Moment: der
Bestrahlung. Wenn doch ein tool solchen sonst sinnvollen Sprachgebrauch
an dieser Stelle verhindern hilft, was ist dagegen ein zu wenden?
:> Sicher, aber "compiler" != "man".
: Der Compiler tut aber nichts von alleine.
In der Tat, und er hat eine Menge Pruefroutinen eingebaut,
die waehrend der Uebersetzung Fehler finden helfen. Das muessen
nicht nur die gerade so eben notwendigen sein, die die jeweilige
Sprach-Definition verletzen, sondern das koennen ergaenzende sein,
wie im Fall von lclint (splint). Es ist wohl auch Moeglich, einen
"prover" in diese Kategorie zum Teil ein zu ordnen?
:> Die Behauptungen, die in einem Programm-Quelltext enthalten sind,
:> koennen glaube ich ohne Gesichtsverlust explizit gemacht werden,
: Sie sind es bereits.
Kommt drauf an. Wenn irgendwo long in einem C Programm steht,
ist damit noch nicht gesagt, welche Teilmenge von Zahlen in der
entsprechenden Groesse enthalten sein werden.
: Wenn Du den Quellcode ver?ndern m?chtest, mu?t Du
: den vorher gelesen und verstanden haben.
Wie Alan Turing vorgeschlagen hat, bei groesseren Programmen
helfen Zwischen-Betrachtungen des Bandes und der Zustaende (Beweis:
Begrenztheit menschlichen Denkens). Auch haben wir nicht ohne
Grund Hochsprachen und Inferenzmaschinen. Was spricht gegen eine
Sprache, die es einem tool erlaubt, ueber Algorithmen, die in der Sprache
formuliert sind, korrekte Aussagen zu machen, die ueber die uebliche
compiler-Pruefung hinaus gehen?
(Assertions als Beispiel zur Explizitheit des semantischen
Inhalts eines Programms: Sie sind in einigen Sprachen
mehr, in anderen weniger explizit angebbar. Es sei denn du findest
es vorteilhaft, wenn die Programmierer, sagen wir die von dir
genannten "Engineers", diese Pruefungs-Anweisungen und deren Handling
repetitiv und explizit selbst schreiben, Mechanismen, die sonst in
Sprachen enthalten sind.)
Gruesse, Georg
Georg Bauhaus
: ZB eine ohne dynamische Speicherverwaltung und ohne
: Rekursionen. Insbesondere letzteres mutet abstrus an, denn gerade
: rekursive Algorithmen kann man oft einfach durch Induktion beweisen.
Daran kein Zweifel. Aber, und da glaube ich scheint ein
entscheidendes Misverstaendnis vor zu liegen, es geht bei SPARK
zunaechst um Systeme, bei denen Speicher fuer heutige Verhaeltnisse
abstrus knapp sein kann. So knapp, dass Rekursion (direkte und
indirekte) deswegen (implizit) nicht zugelassen ist, weil im
allgemeinen Fall fuer den Funktions-Aufruf stack-speicher, und
zwar in statisch nicht vorhersagbarer Menge, benoetigt werden wird.
Das ist hier entscheidend.
Es geht u.a. um statische Vorhersagbarkeit des verbrauchten
stack-Speichers: Es muss sicher gestellt sein, dass das Programm,
so wie du auch gefordert hast, nicht an die Decke knallt, sozusagen,
Oder amok laeuft, sondern sich faengt, vorhersagbar verhaelt,
und dafuer muss im allgemeinen Fall Speicher da sein.
Beispiel: Die Steuerung einer automatischen Tuer hat in einem
aussergewohlichen (tolerablen?) Fall jemanden eingeklemmt. Wenn
- ich Rekursion im Steuerprogramm nach belieben erlaube, und
- Funktionen Seiteneffekte zB auf elektrisches Geraet haben duerfen,
dann kaenn es sein, dass kein stack-speicher da ist, um reset-Routinen
aufzurufen. Ich koennte verlangen, dass dann stack speicher fuer
solche Faelle reserviert ist, aber wieviel, wenn rekursion etc
zugelassen ist? Ich koennte verlangen, dass der Aufrufstapel einfach
abgeraeumt wird, aber habe ich dann noch hinreichend Information
ueber der Zustand von Variablen, die den Zustand externer GEraete
aufgezeichnet haben? Alles in statisch reservierten Variablen
speichern?
Auswege sind offenbar nicht immer leicht zu finden, und ohne
Zweifel ist ein geeigneter System-Entwurf unentbehrlich. Aber
ich weiss immer noch nicht, was gegen den Einsatz eines tools
spricht, dass eine Sprache verarbeitet, die mir beim Umsetzen
eines Entwurfs nach Implementations-Richtlinien "auf die Finger
schaut". Ich denke, es gibt nicht viele Leute, die so gut sind
wie sozusagen ein compiler, runtime-experte, Korrektheits-Pruefer
und "O(f(n))-Beweiser" in einer Person.
Ist zB lint (lclint, splint) ein ebenso verwerfliches Werkzeug?
Gruesse,
Georg
:> Eine Sprache, die es einfacher macht, korrekten Code zu schreiben,
:> weil das dann ja jedes Kind tun kann?
:
: Wie bereits erw?hnt: Ich m?chte nicht mein Leben einem Programm von
: jemandem anvertrauen, dem es ?kompliziert? erscheint,
: integer-?berl?ufe im Quelltext sinnvoll zu behandeln und der ein
: Spezialtool braucht, um potentielle zu finden. Dazu gibt es zuviele
: esoterische Fehlerm?glichkeiten.
:
:> Dein Problem, ich schreibe keine Software, um mit Compiler und
:> Debugger zu kaempfen, ich schreibe Software, um etwas zum Laufen zu
:> bekommen.
:
: Vermutlich w?re ?davonlaufen? anzuraten.
:
:> >> Das einzige, was Dir fehlt, sind gotos (braucht
:> >> man die?)
:> >
:> > ?Man? benutzt sie st?ndig, was vom Compiler mehr oder minder hinter
:> > einem Feigenblatt verborgen wird.
:>
:> *Das* weiss ich selbst.
:
: Warum fragst Du dann? Du wei?t sicher auch, da? die meisten
: Kontrollstrukturen prinzipiell redundant sind und der Bequemlichkeit/
: ?bersichtlichkeit halber verwendet werden.
:
: ----------------------
: p = pacct->gr_mem;
: while (1) {
: if (!*p) break;
: if (strcmp(*p, user->pw_name) == 0) {
: if (argv[1]) log_access(user->pw_name, argv + 1, argc - 1);
: goto found;
: }
:
: ++p;
: }
:
: setuid(uid);
: }
:
: found:
: execve(COMMAND, argv, env);
: perror("execve");
: ----------------------
:
: F?r goto gilt das desgleichen.
:
:> > Obiges gilt entsprechend: Objekte im RAM haben eine Adresse, die die
:> > CPU benutzt, um sie zu adressieren.
:>
:> Und? Deswegen muss ich das Objekt auf Source-Ebene nicht mit seiner
:> Adresse ansprechen.
:>
:> Da kannst Du auch gleich wieder Assembler programmieren.
:
: Das Gegenteil von A ist !A und nicht B. Es bringt nichts, die Adressen
: wegzuabstrahieren, also wozu tun?
:
:> >> Was ich mit SHOLIS meinte: Wenn mit SPARK ein System beschreiben
:> >> kann, welches die sicherheitskritische Software eines Helikopters
:> >> darstellt,
:> >
:> > Es ist ?bewiesen?, da? man so ein System in Visual Basic beschreiben
:> > kann.
:>
:> So, kann man das?
:
: Ja und zwar wegen 'turing vollst?ndig'.
--
---
Microsoft Windows--a fresh perspective on information hiding
Rainer Weikusat
> Rainer Weikusat <weik...@students.uni-mainz.de> writes:
> > Das «Verständnis» sagt per se gar nichts aus. Aber der Quelltext tut
> > das: Er ist eine vollständige Beschreibung dessen, was die Software zur
> > Laufzeit tun wird.
>
> Davon träumst du, oder?
Eine nichtdeterministische Maschine kann ich auch «formal» nicht
«verifizieren». Das sich praktische Vorteile dadurch ergeben, daß die
Semantik unter der Annahme einer deterministischen Maschine bekannt
und sinnvoll ist, sollte nachvollziehbar sein.
> > dem Programmierer überlassen. Falls man dem vorher nicht zutrauen
> > konnte, faktisch korrekten Code zu schreiben (insofern möglich), warum
> > sollte er es hinterher plötzlich können?
>
> Wenn es um kritische Systeme geht, kann man getrost davon ausgehen,
> dass *kein* einziger Mensch jemals korrekten, sprich 100%
> fehlerfreien, Code schreibt.
Gründet sich die Annahme, daß die Mehrzahl aller «kritischen» Systeme
mehr oder minder irreparabel kaputt ist, eigentlich auf praktische
Erfahrungen? Gruselig ...
> Ziel muss es also sein, einerseits Fehler verstärkt zu vermeiden und
> es gibt Möglichkeiten, die (durchschnittliche) Fehlerquote beim
> Programmieren mit diversen Mitteln zu reduzieren. Andererseits
> versucht man möglichst automatisiert Fehler zu finden
«Die Achterbahn des Schreckens, Teil II». Ist Dir klar, das jede
automatisch verhinderte «Fehlerklasse» ein weiterer kludge ist, der
um einen mittlerweile bekannten möglichen Fehler herumwürgt?
> > Wegen einer formalen Beschreibung ohne Fehler
> > bekomme ich keinen Quelltext ohne Fehler, und (zum 1000x):
>
> Natürlich nicht.
>
> > Ein Programm ist bereits eine formale Beschreibung.
>
> Aber auf einem völlig anderen Abstraktionsniveau. Auf diese Weise
> bekomme ich etliche neue Fehlerquellen.
Zwischenschritt eliminieren ;-).
> > > Eine Registermaschine ist auch turing-vollstaendig. Warum also C?
>
> > C-Programme beschreiben normalerweise Registermaschinen.
>
> So ein Quark. C basiert noch nicht einmal auf einer klaren
> Maschinenbeschreibung (wie z.B. Lisp) und noch viel weniger
> beschreiben C Programme eine Registermaschine (welchen Sinn sollte das
> auch machen) -- du selbst hast doch gesagt, Quelltext beschreiben, was
> zur Laufzeit passiert. Wie sollen sie außerdem auch noch Maschinen
> beschreiben?
Offensichtlich kann man jedes Programm in einer imperativen
Programmiersprache auch als spezialisierten IC realisieren. Ein
Programm ist eine virtuelle Maschine, die auf einer etwas
allgemeineren simuliert wird.
> [Spielzeugsprache]
> > ZB eine ohne dynamische Speicherverwaltung und ohne
> > Rekursionen. Insbesondere letzteres mutet abstrus an, denn gerade
> > rekursive Algorithmen kann man oft einfach durch Induktion beweisen.
> [...]
> > Wie bereits erwähnt: Ich möchte nicht mein Leben einem Programm von
> > jemandem anvertrauen, dem es «kompliziert» erscheint,
> > integer-Überläufe im Quelltext sinnvoll zu behandeln und der ein
> > Spezialtool braucht, um potentielle zu finden. Dazu gibt es zuviele
> > esoterische Fehlermöglichkeiten.
>
> Und eben weil es viele esoterische Fehlermöglichkeiten gibt, sollte
> man alle Möglichkeiten, Fehler zu vermeiden, nutzen. Wieso nicht
> gleich eine Sprache, bei der etliche Fehlerklassen (z.B. wilde Zeiger)
> schlicht unmöglich sind?
Weil das praktisch eine non-issue ist und in jedem anderen Fall ist
der Quälcode Sondermüll und gehört als solcher behandelt zu werden.
> Wieso sind einige Abstraktionskonzepte, wie Rekursionen u.a., wichtig
> und gut und andere wieder völlig überflüssig und böse?
Ich hatte nichts von «überflüssig» oder «böse» geschrieben.
> > > Und? Deswegen muss ich das Objekt auf Source-Ebene nicht mit seiner
> > > Adresse ansprechen.
>
> > > Da kannst Du auch gleich wieder Assembler programmieren.
>
> > Das Gegenteil von A ist !A und nicht B. Es bringt nichts, die Adressen
> > wegzuabstrahieren, also wozu tun?
>
> Um Fehlerquellen zu vermeiden. Mit Adressen, zumal ihrer
> Repräsentation(!) in C, kann man rechnen,
Das ist bei Werten so üblich.
> mit Referenzen (einer anderen Repräsentation) kann man nicht rechnen
> -- damit sind wilde Zeiger z.B. (nahezu) unmöglich.
Das hat nichts mit «Rechnen» zu tun, sondern damit, ob die abstrakte
Maschine, die von der Sprache beschrieben wird, Referenzen mit
beliebigen Werten gestattet.
Rainer Weikusat
> Rainer Weikusat wrote:
> > Tut mir leid, aber das ist definitiv nicht mehr komisch.
>
> Eben. Aber Deinen Aussagen nach zu urteilen, die darauf schliessen
> lassen, dass Du ausschliesslich dem "faehigen Programmierer" vertraust,
> koennen Deine Massstaebe an Software nicht allzu hoch sein.
Du behauptest das ständig, obwohl ich fortwährend das Gegenteil
schreibe.
> > Das «Verständnis» sagt per se gar nichts aus. Aber der Quelltext tut
> > das: Er ist eine vollständige Beschreibung dessen, was die Software
> > zur Laufzeit tun wird.
>
> Nein, diese Beschreibung ist mitnichten vollstaendig. Was tut das
> System, wenn die Software einen Zeiger dereferenziert, der auf ein
> zufaellig bereits freigegebenes Objekt zeigt?
Wie passiert das ohne im Quellcode auffindbar zu sein?
> Was passiert, wenn mit den Ergebnissen aus uninitialisierten
> Variablen gerechnet wird?
Dann wird mit uninitialsierten Variablen gerechnet. Das konkrete
Ergebnis ist falsch und somit egal.
> Das ganze ist nicht einmal mehr deterministisch, was willst Du da
> mit dem Source anfangen?
Beides korrigieren. Warum?
> Und *Du* kannst bei 100KSLOC *garantieren*, dass keiner dieser Fehler
> auftritt?
Spielt das eine wesentliche Rolle, falls man das muß?
> >> Und es wohl kaum moeglich, ein 100'000 Zeilen-Programm vollstaendig
> >> zu verstehen und garantieren zu koennen, dass es das tut, was es tun
> >> soll, unter allen Umstaenden.
> >
> > Es ist möglich, eine 100.000-Zeilen-Programm so zu konstruieren, daß
> > man keine Einheiten von mehr als maximal tausend Zeilen hat und so,
> > daß diese Einheiten keine internen Abhängigkeiten haben.
>
> Ja. Was nicht heisst, dass es nachher funktioniert.
Falls der Entwurf Müll war, bekommt man ein korrektes Programm, das
Müll tut.
> > Die Grundvoraussetung für das, was ich geschrieben hatte
> > («Tolerabilität von fringe case-Fehlersituationen»), ist, daß das
> > System deswegen nicht Amok läuft, was man durch einen geeigneten
> > internen Aufbau sicherstellt.
>
> Und in SPARK durch den Beweis der Abwesenheit von Laufzeitfehlern
> garantieren kann.
Lies das bitte mal durch
<URL:http://www.freesoft.org/CIE/RFC/1035/43.htm>
und erkläre mir bitte danach, wie eine Überlaufprüfung mir gegen data
corruption, die aufgrund einer verpeilten Implementierung ohne das
höchstwertige Bit im Offset auftritt, falls es für die befragte zone
soviel secondaries gibt, daß in der addtional info section
Rückverweise > 255 vorkommen.
> >> It is easier to fit the specification to a program than vice versa?
> >
> > Entweder das Programm ist eine Übersetzung der Spezifikation in eine
> > andere Sprache oder Du hast einen schrecklichen Fehler gemacht, der
> > sich auch mit 400t glue code im Nachhinein nicht mehr wird
> > reparieren lassen.
>
> Sorry, entweder Du traeumst oder Du bist einer von denen, die immer auf
> Anhieb korrekte, der Spezifikation entsprechende Software schreiben
> koennen. Wieviele Fehler hast Du im Durchschnitt pro Tausend Zeilen
> Code?
Das ist die falsche Frage. «Wie lange dauert es, bis 1000 Zeilen Code
fehlerfrei sind?»
> BTW, auch die Spezifikation kann falsch sein bzw. Inkonsistenzen
> haben.
Das ist dann allerdings Pech, aber auf einer anderen Ebene.
> Beim MultOS-CA hat man 38 Fehler aus der Spezifikationsphase erst in
> der Kodierphase gefunden und einen waehrend der Operation.
Zuviele Details.
> > Wie käme ich denn dazu? Wegen einer formalen Beschreibung ohne Fehler
> > bekomme ich keinen Quelltext ohne Fehler,
>
> In SPARK hast Du sehr gute Chancen dazu.
>
> > und (zum 1000x): Ein Programm ist bereits eine formale Beschreibung.
>
> LOL
>
> Ein formale Beschreibung, deren Konsistenz Du bitte
> *wie* nachweist?
Wem gegenüber?
> >> >> So die Theorie und in den vielen Faellen mag das stimmen. Laut Rod
> >> >> (und ich glaube da einfach mal seiner Erfahrung) findet man die
> >> >> meisten Fehler aber, wenn man diese einzelnen Unit zusammenfuegen
> >> >> will, also letztendlich im Interface. Das ist im uebrigen auch
> >> >> meine Erfahrung.
> >> >
> >> > Das ist eine groteskte Horrortheorie,
> >>
> >> Diese Theorie stammt von Dir, danke.
> >
> > Warum sollte ich mich denn vollkommen widersinnig auf meinen Text
> > beziehen anstelle auf Deinen?
>
> Weil ich auf Deinen Text bezogen "So die Theorie" schrieb.
> > Bei allen Dingen, mit denen ich praktisch zu tun habe, und dazu gehört
> > Quellcode anderer Leute mit dazu, verhält sich das genau umgekehrt, dh
> > der Code tut nicht das, was das Interface angeblich bereitstellt.
>
> Dann solltest Du die Leute grundsaetzlich wegen Unfaehigkeit feuern.
Ich behelfe mir lieber damit, nichts wiederzuverwenden, was trivial
reimplementierbar ist.
> >> > deren Implikationen ausschließlich besagen, daß die Resultate
> >> > lebensgefährlich sein werden.
> >>
> >> Interessant. Wie kommst Du darauf?
> >
> > Ich denke nicht, daß ich das Dir in einem Usenet-angemessenen Rahmen
> > erklären kann, aber jedenfalls würde ich nie so wahnsinnig sein, mein
> > Leben einem Computerprogramm anzuvertrauen, auf das diese Aussage
> > zutrifft, falls ich nicht ohnehin Hazard spiele.
>
> Irgendwie habe ich jetzt was nicht ganz begriffen.
Das, wovon Du redest, würde ich «design flaws» im Interface
nennen. Falls die häufiger sind als Tippfehler, würde ich «Rennt um
euer Leben» als einzige adäquate Reaktion empfehlen.
> Ansonsten, steige bitte nie wieder in ein Flugzeug, vor allem nie weider
> in eine Boeing. Das ist lebensgefaehrlich.
Vermutlich. Aber das kürzlich für den häufigsten Luftfahrtunfall heißt
«CIFT», was für «controlled flight into terrain» steht, dh der Pilot
fliegt gegen den Berg und warum bleibt ein Geheimnis.
> Die Software haben nicht nur unfaehige Idioten geschrieben, die zu
> bloed sind, Integer-Ueberlaeufe schon im Source zu erkennen,
Wenn Du sie so nennen magst.
> >> Ich bin immer noch nicht ganz dahintergekommen, was Du mit
> >> Spielzeugsprache meinst.
> >
> > ZB eine ohne dynamische Speicherverwaltung
>
> Brauche ich wirklich selten. Und in Embedded Systems- bzw.
> Safety-Critical-Umgebungen will man das auch nicht. Es wird Dir in
> den seltensten Faellen gelingen, nachzuweisen, dass Deine Techniken
> nicht zu Speicherfragmentierung und/oder Memory-Leaks fuehren.
Bitte? «Man kann keine Algorithmen schreiben, deren Speicherverbrauch
über die vollständige Laufzeit O(1) ist?», sagen wir mal trivial
dadurch, daß man eine maximale Anzahl an mallocs durchführt und die
allozierten Objekte weiterverwendet. Das gibt dann eine Invariante,
der die Eingabedaten genügen müssen und andernfalls hat man einen
korrigierbaren Ausnahmezustand.
> > und ohne Rekursionen.
>
> Der SPARK-Examiner selbst ist in SPARK geschrieben. Und ja, der Parser
> ist statisch verifiziert und benutzt weder Rekursion noch dynamischen
> Speicher. Rod war natuerlich durchaus der Meinung, dass das nicht sehr
> einfach war.
>
> > Insbesondere letzteres mutet abstrus an, denn gerade
> > rekursive Algorithmen kann man oft einfach durch Induktion beweisen.
>
> Auch deren Stackverbrauch, bevor die Runtime-Umgebung ein Storage_Error
> ausloest (oder halt nicht)?
In Abhängigkeit von den Eingabedaten. Klar. Wieso?
> >> Eine Sprache, die es einfacher macht, korrekten Code zu schreiben,
> >> weil das dann ja jedes Kind tun kann?
> >
> > Wie bereits erwähnt: Ich möchte nicht mein Leben einem Programm von
> > jemandem anvertrauen, dem es «kompliziert» erscheint,
> > integer-Überläufe im Quelltext sinnvoll zu behandeln
>
> Falls Du das auf mich beziehst:
Ich halte Dich eigentlich nicht für ein Programm, lasse mich aber
gerne eines besseren belehren.
> > und der ein Spezialtool braucht, um potentielle zu finden.
>
> Wenn Du das so meinst. Demzufolge sollten sicherheitskritische Programme
> in
Sprachen geschrieben werden, die die verwantwortlichen Autoren auch
beherrschen. Solche Anforderungen sind für Übersetzer(!!)
selbstverständlich und die entwerfen keine «kritischen
Systeme». Welche ist vollkommen wurscht.
[...]
Das ist eine Schleife mit drei Abbruchbedingungen, von denen Du eine
willkürlich im Schleifenkopf positioniert hast. Ich halte das für eine
Verwirrtaktik und brauchst wegen der Zählerei 'grundsätzlich' eine
Überlaufprüfung. Für den Wert gibt es möglicherweise eine konstante
Obergröße, aber keine definierte Länge (... die nicht erst durch
Zählen ermittelt werden müßte).
> > Das Gegenteil von A ist !A und nicht B. Es bringt nichts, die Adressen
> > wegzuabstrahieren,
>
> Aber sicher bringt das etwas.
>
> > also wozu tun?
>
> Deswegen:
>
> |void something (char* blabla)
>
> vs.
>
> |procedure Something (BlaBla : in Char_Array);
>
> vs
>
> |procedure Something (Blabla : out Char_Array);
>
> Jetzt versuche mal, den drei Funktionen eine Nullzeiger zu uebergeben
> und bei der C-Variante zu erzaehlen, ob blabla veraendert wird.
>
> Manchmal sind Abstraktionen der bessere Weg.
Das halte ich für «debatable». Weniger Komplexität ist der bessere
Weg.
Rainer Weikusat
> Rainer Weikusat <weik...@students.uni-mainz.de> wrote:
> : denn daf?r ist sie da. Ich mu? allerdings gestehen, Dir nicht ganz
> : folgen zu k?nnen.
>
> Ich wollte andeuten, dass es nicht mehr einfach ist, die Bedeutung
> einer Hochsparchen-Operation im Detail pruefen oder vorher sagen
> zu koennen:
> In einem nebenlaeufigen Programm sei '=' im Quellcode angetroffen.
> Was genau, im hinblick auf die betroffenen Daten (lhs, rhs),
> im Hinblick auf die betroffenen Programm-Teile,
> im HInblick auf die Stack-Nutzung,
> im Hinblick auf die heap-Nutzung,
> im Hinblick auf die waehrend '=' ablaufenden clock ticks,
> bedeutet '='?
Das ist alles herzlich irrlevant, denn es handelt sich bis auf den
ersten um externe Faktoren (dh Gegenstände einer getrennten
Betrachtung).
> Faellt es dir hier so leicht, sagen wir innerhalb von 2 min,
> diese Angaben fuer einen Echtwelt-Wartungsfall zu machen?
Es sollte.
> :> Jedes turing-vollstaendige setup koennte Speichersammlung
> :> bereitstellen. Wer/was schuetzt die Steuerung des Roentgen-Kastens
> :> davor, dass das jemand versehentlich genutzt hat?
>
> : Wovon sprichst Du?
>
> EIn Roentgen-Geraet hat eine Bestrahlungs-Dauer die nicht ueberschritten
> werden darf. Sollte in einem Programm garbage collection erlaubt
> sein kann dabei Zeit drauf gehen, vielleicht im falschen Moment: der
> Bestrahlung. Wenn doch ein tool solchen sonst sinnvollen Sprachgebrauch
> an dieser Stelle verhindern hilft, was ist dagegen einzuwenden?
«Garbage Collection» und «Echtzeit» dürften sich wohl gegenseitig
ausschließen (nicht notwendigerweise: man kann vermutlich
inkrementelle gc mit festen Zeitgrenzen implementieren).
> :> Die Behauptungen, die in einem Programm-Quelltext enthalten sind,
> :> koennen glaube ich ohne Gesichtsverlust explizit gemacht werden,
>
> : Sie sind es bereits.
>
> Kommt drauf an. Wenn irgendwo long in einem C Programm steht,
> ist damit noch nicht gesagt, welche Teilmenge von Zahlen in der
> entsprechenden Groesse enthalten sein werden.
Für jede Implementierung schon. Gegen Fehlverwendung hilft das
allerdings wenig.
> (Assertions als Beispiel zur Explizitheit des semantischen
> Inhalts eines Programms: Sie sind in einigen Sprachen
> mehr, in anderen weniger explizit angebbar. Es sei denn du findest
> es vorteilhaft, wenn die Programmierer, sagen wir die von dir
> genannten "Engineers", diese Pruefungs-Anweisungen und deren Handling
> repetitiv und explizit selbst schreiben, Mechanismen, die sonst in
> Sprachen enthalten sind.)
Kaum.
Rainer Weikusat
> Rainer Weikusat <weik...@students.uni-mainz.de> wrote:
> : ZB eine ohne dynamische Speicherverwaltung und ohne
> : Rekursionen. Insbesondere letzteres mutet abstrus an, denn gerade
> : rekursive Algorithmen kann man oft einfach durch Induktion beweisen.
>
> Daran kein Zweifel. Aber, und da glaube ich scheint ein
> entscheidendes Misverstaendnis vor zu liegen, es geht bei SPARK
> zunaechst um Systeme, bei denen Speicher fuer heutige Verhaeltnisse
> abstrus knapp sein kann. So knapp, dass Rekursion (direkte und
> indirekte) deswegen (implizit) nicht zugelassen ist, weil im
> allgemeinen Fall fuer den Funktions-Aufruf stack-speicher, und
> zwar in statisch nicht vorhersagbarer Menge, benoetigt werden wird.
> Das ist hier entscheidend.
Die Speichermenge, die benötigt wird, hängt von den Eingabedaten
ab.
> Es geht u.a. um statische Vorhersagbarkeit des verbrauchten
> stack-Speichers: Es muss sicher gestellt sein, dass das Programm,
> so wie du auch gefordert hast, nicht an die Decke knallt, sozusagen,
> Oder amok laeuft, sondern sich faengt, vorhersagbar verhaelt,
> und dafuer muss im allgemeinen Fall Speicher da sein.
>
> Beispiel: Die Steuerung einer automatischen Tuer hat in einem
> aussergewohlichen (tolerablen?) Fall jemanden eingeklemmt. Wenn
> - ich Rekursion im Steuerprogramm nach belieben erlaube, und
> - Funktionen Seiteneffekte zB auf elektrisches Geraet haben duerfen,
>
> dann kaenn es sein, dass kein stack-speicher da ist, um reset-Routinen
> aufzurufen. Ich koennte verlangen, dass dann stack speicher fuer
> solche Faelle reserviert ist, aber wieviel, wenn rekursion etc
> zugelassen ist? Ich koennte verlangen, dass der Aufrufstapel einfach
> abgeraeumt wird, aber habe ich dann noch hinreichend Information
> ueber der Zustand von Variablen, die den Zustand externer GEraete
> aufgezeichnet haben? Alles in statisch reservierten Variablen
> speichern?
Das war doch das projektierte Modell.
> Auswege sind offenbar nicht immer leicht zu finden, und ohne
> Zweifel ist ein geeigneter System-Entwurf unentbehrlich. Aber
> ich weiss immer noch nicht, was gegen den Einsatz eines tools
> spricht, dass eine Sprache verarbeitet, die mir beim Umsetzen
> eines Entwurfs nach Implementations-Richtlinien "auf die Finger
> schaut". Ich denke, es gibt nicht viele Leute, die so gut sind
> wie sozusagen ein compiler, runtime-experte, Korrektheits-Pruefer
> und "O(f(n))-Beweiser" in einer Person.
Man sollte schon wissen, was man für Laufzeitverhalten zusammenbaut.
> Ist zB lint (lclint, splint) ein ebenso verwerfliches Werkzeug?
Wieso verwerflich?
Stefan Nobis
> Stefan Nobis <ste...@snobis.de> writes:
> > Rainer Weikusat <weik...@students.uni-mainz.de> writes:
> > > Das «Verständnis» sagt per se gar nichts aus. Aber der Quelltext tut
> > > das: Er ist eine vollständige Beschreibung dessen, was die Software zur
> > > Laufzeit tun wird.
> > Davon träumst du, oder?
> Eine nichtdeterministische Maschine kann ich auch «formal» nicht
> «verifizieren». Das sich praktische Vorteile dadurch ergeben, daß die
> Semantik unter der Annahme einer deterministischen Maschine bekannt
> und sinnvoll ist, sollte nachvollziehbar sein.
Es wäre schön, wenn du, mal zur Abwechslung, auf die Kernaussagen
eingehen könntest, statt wahllos themenflucht zu begehen.
Wieso schafelst du von nichtdeterministischen Maschinen? Was tut das
zur Sache? Es geht um konkrete, deterministische Rechner, reale
Computer mit Betriebssystemen, vielen Bibliotheken, Laufzeitumgebung
der verwendeten Programmiersprache etc.
Und in diesem Kontext ist der Quelltext eben gerade keine
*vollständige* Beschreibung dessen, was die Software zur Laufzeit tut,
schon allein deswegen, weil der Quelltext gar keine semantische
Beschreibung von aufgerufenen Bibliotheksroutinen oder Syscalls
enthält. Deren Semantik ist aber durchaus wesentlich für das
Laufzeitverhalten eines Programmes.
In einem Bibliotheksaufruf wie "open(...)" steckt natürlich eine
Andeutung, was hier zur Laufzeit passieren *sollte*! Es ist aber keine
*vollstädinge* Beschreibung des Laufzeitverhaltens. Das ist ein sehr
wichtiger Unterschied.
> > > dem Programmierer überlassen. Falls man dem vorher nicht zutrauen
> > > konnte, faktisch korrekten Code zu schreiben (insofern möglich), warum
> > > sollte er es hinterher plötzlich können?
> > Wenn es um kritische Systeme geht, kann man getrost davon ausgehen,
> > dass *kein* einziger Mensch jemals korrekten, sprich 100%
> > fehlerfreien, Code schreibt.
> Gründet sich die Annahme, daß die Mehrzahl aller «kritischen» Systeme
> mehr oder minder irreparabel kaputt ist, eigentlich auf praktische
> Erfahrungen? Gruselig ...
Ich schrieb, dass kein Mensch 100% fehlerfreien Code zu schreiben in
der Lage ist. Das Gegenteil müsstest du mir erstmal beweisen, da es
diverse Studien gibt, die empirisch nachgewiesen haben, dass ab
ca. 30.000 bis 50.000 Zeilen Quelltext garantiert eine gewisse
Mindestzahl an Fehlern vorhanden ist.
Allerding entschuldige ich mich für eine grobe Ungenauigkeit:
Natürlich beziehen sich solche Fehlerbetrachtungen erstmal nur auf
direkt geschriebenen Quelltext, ohne aufwendige(!) Fehlersuche und
Tests. Wenn man also einen Programmierer hinsetzt und Code schreiben
lässt[1], dann wird, je nach Komplexität und Umfang des
Gesamtprojekts, dabei eine gewisse Fehlerquote garantiert
auftreten.
Und solche Fehler eliminiert man eben nur mit sehr aufwendigen (und
leider teuren) Verfahren. Das Genie, dass nur mit Texteditor und
Compiler bewaffnet ohne weitere (technische) Hilfsmittel (von Doku mal
abgesehen :)), fehlerfreie Systeme mit mehreren zehntausend Zeilen
Quelltext erstellen kann, musst du mir echt mal zeigen.
Die kritischen Systeme bekommt man dann eben nur durch sehr formelle
und aufwendige Verfahren doch noch hinreichend fehlerfrei. Das dies,
egal ob Software und/oder elektronik überhaupt im Spiel ist, niemals
in jedem Fall zu 100% gelingt, zeigen die vielen Beispiele von
katastrophalen Fehlern bei kritischen Systemen. Merke: Menschen
produzieren niemals garantiert 100% fehlerfrei Produkte, egal in
welchem Bereich. Menschen machen Fehler und ein Mensch macht auch sehr
häufig denselben Fehler mehrmals.
[1] Den er selbst natürlich nachträglich nochmal lesen und
korrigieren darf und auch einfache, oberflächliche Tests sind noch
erlaubt -- also Compiler mit max. Warnungen, einfache Testläufe mit
aktiven asserts; halt so dass, was üblicherweise vor dem Einchecken in
CVS oder ähnliches gemacht wird.
> «Die Achterbahn des Schreckens, Teil II». Ist Dir klar, das jede
> automatisch verhinderte «Fehlerklasse» ein weiterer kludge ist, der
> um einen mittlerweile bekannten möglichen Fehler herumwürgt?
Könntest du das mal näher ausführen? Ich verstehe nicht, was du
meinst.
Oder spielst du darauf an: Mensch kennt ja die möglichen
Fehlerquellen, also sollte es kein Problem sein, die Fehler zu
vermeiden.
Und du hast ja auch noch nie in deinem Leben einen Fehler ein zweites
Mal begangen, gelle.
Mal konkret: Wie stellst du dir eigentlich die Entwicklung von
z.B. der Steuer-Software der Ariane vor? Auf die Genialität der
Programmierer hoffen, die schon keine Fehler machen oder die zwei, die
doch mal passieren, problemlos während eines kurzen Debuggings finden?
Das ist deine ganze Qualitätskontrolle? Und verlässt dich blind auf
ein Team von vielleicht hundert Programmierern? Du kannst in solchen
Teams für die Qualität und Fehlerfreiheit jedes einzelnen Menschen
garantieren? Wie?
> > Aber auf einem völlig anderen Abstraktionsniveau. Auf diese Weise
> > bekomme ich etliche neue Fehlerquellen.
> Zwischenschritt eliminieren ;-).
Abstraktions- und Kontrollebenen eliminiert. Für die Entwicklung eines
sicheren und robusten LDAP-Servers wahrscheinlich sinnvoll, für obiges
Beispiel der Ariane-Steuerung, zumal bei großen Teams mit den dabei
auftretendem Kommunikationsoverhead und -problemen, halte ich es für
ein sehr großes Problem, diese Zwischenschritte zu eliminieren.
Diese Zwischenschritte erlauben in einem (größeren) Team eine bessere
Kommunikation, da durch eine gemeinsame, formalisierte Sprache erstmal
dafür gesorgt wird, dass auch wirklich alle von derselben Sache
sprechen und dasselbe meinen. Die Quelltextebene wäre hier (bei
komplexen Systemen und größeren Teams) zu sehr mit Details belastet,
so dass der Blick für das Wesentliche zu schnell verloren geht.
> > > C-Programme beschreiben normalerweise Registermaschinen.
> > So ein Quark. C basiert noch nicht einmal auf einer klaren
> Offensichtlich kann man jedes Programm in einer imperativen
> Programmiersprache auch als spezialisierten IC realisieren. Ein
> Programm ist eine virtuelle Maschine, die auf einer etwas
> allgemeineren simuliert wird.
Eine Registermaschine ist ein klar definierter Begriff. Und eine
solche Registermaschine wird durch kein C Programm beschrieben (man
kann aber C Programme in Programme für Registermaschinen übersetzen).
Buzzwords und schwammige Ausdrucksweisen helfen dir da nicht weiter.
Und um in deinem Begriffswirrwarr zu bleiben: Dadurch, dass VM A auf
VM B simuliert wird, ist VM A nicht gleich eine Beschreibung von VM
B.
> > Und eben weil es viele esoterische Fehlermöglichkeiten gibt, sollte
> > man alle Möglichkeiten, Fehler zu vermeiden, nutzen. Wieso nicht
> > gleich eine Sprache, bei der etliche Fehlerklassen (z.B. wilde Zeiger)
> > schlicht unmöglich sind?
> Weil das praktisch eine non-issue ist und in jedem anderen Fall ist
> der Quälcode Sondermüll und gehört als solcher behandelt zu werden.
Ah! Verstehe. Also ist nichts gegen möglichst viele Fehlerquellen in
einer Sprache einzuwenden, weil ja gute Programmierer nicht auf solch
dumme Fallen reinfallen und keine Probleme damit haben, jegliche
Fehler zu vermeiden.
Wo bitte waren doch gleich diese absolut fehlerfreien Programme, die
es ja deiner Aussage nach offensichtlich geben muss. Denn gute
Programmierer machen ja keine Fehler.
Alle deine nicht-trivialen Programme sind völlig fehlerfrei? Da wurde
noch nie ein Fehler in einem deiner Programme gefunden, nachdem du sie
für den produktiven Einsatz freigegeben hattest? Alle Achtung, ich bin
sehr beeindruckt (oder schreibst du nur sehr kleine Programme).
Bleibt nur die Frage wie viele solcher Genies es gibt, die fehlerfrei
programmieren können. Ob die Anzahl reicht, um den realen Bedarf an
Software zu decken? Ich habe da so meine Zweifel.
Und für alle die armen, im Grunde unfähigen Programmierer, die eben
doch ab und zu mal einen Fehler im Quelltext machen, den sie nicht
alleine finden, gibt es eben Hilfen, die bestimmte, typische Fehler zu
vermeiden helfen.
Ich für meinen Teil habe auch kein Problem damit, zuzugeben, dass ich
niemals fehlerfrei arbeite, dass ich nicht perfekt bin und daher immer
wieder mal auf Hilfe (von anderen Menschen oder von Werkzeugen)
angewiesen bin, um meine Fehlerquote zu reduzieren. Und ich vermute,
dies trifft auf viele Menschen in allen Tätigkeitsbereichen zu.
Langsam frage ich mich ernsthaft, wie dein Menschenbild aussieht.
> > Wieso sind einige Abstraktionskonzepte, wie Rekursionen u.a., wichtig
> > und gut und andere wieder völlig überflüssig und böse?
> Ich hatte nichts von «überflüssig» oder «böse» geschrieben.
Nicht wörtlich, aber deine Aussagen suggerierten dies. So hälst du es
für überflüssig und sinnlos, Speicheradressen zu abstrahieren und
z.B. das Rechnen und beliebige Manipulieren von diesen zu verbieten,
da ja gute Programmierer all die offensichtlichen Fehlerquellen leicht
vermeiden können und daher (zumindest in diesem Punkt) niemals Fehler
begehen.
Genau solche Mechanismen sind Abstraktionskonzepte und neben anderen
Aspekten helfen sie (evtl.) auch Fehlerquellen zu vermeiden (was ja
richtige Programmierer niemals nötig hätten).
> > Um Fehlerquellen zu vermeiden. Mit Adressen, zumal ihrer
> > Repräsentation(!) in C, kann man rechnen,
> Das ist bei Werten so üblich.
Bei Konstanten nicht.
> > mit Referenzen (einer anderen Repräsentation) kann man nicht rechnen
> > -- damit sind wilde Zeiger z.B. (nahezu) unmöglich.
> Das hat nichts mit «Rechnen» zu tun, sondern damit, ob die abstrakte
> Maschine, die von der Sprache beschrieben wird, Referenzen mit
> beliebigen Werten gestattet.
Nein, das hat damit zu tun, dass der Ausdruck "Referenz"
i.a. impliziert, dass es sich um etwas relativ konstantes handelt,
d.h. man kann immer nur ein existierendes Objekt referenzieren und
nicht eine beliebige Speicheradresse (es sei denn, diese wäre ein
zulässiges Objekt, was jedoch in den meisten Sprachen, die solche
Abstraktionskonzepte bieten, nicht der Fall ist).
Referenzen können also sehr wohl beliebige Werte annehmen, jedoch muss
dieser Wert zu einem exitierenden, gültigen (dereferenzierbaren)
Objekt gehören.
--
Stefan.
Stefan Nobis
> > > Das «Verständnis» sagt per se gar nichts aus. Aber der Quelltext tut
> > > das: Er ist eine vollständige Beschreibung dessen, was die Software
> > > zur Laufzeit tun wird.
> > Nein, diese Beschreibung ist mitnichten vollstaendig. Was tut das
> > System, wenn die Software einen Zeiger dereferenziert, der auf ein
> > zufaellig bereits freigegebenes Objekt zeigt?
> Wie passiert das ohne im Quellcode auffindbar zu sein?
Falsche Frage! Du hast behauptet, der Quelltext sei eine
*vollständige* Beschreibung dess, was die Software zur Laufzeit tun
wird. Was also tut die Software bei einem solchen Fehler? Du kannst
das nicht ausschließlich aus dem Quelltext heraus beantworten, weil du
die exakte Semantik bestimmter Bibliotheksfunktionen kennen musst?
Richtig. Also kann der Quelltext keine *vollständige* Beschreibung des
Laufzeitverhaltens sein.
> > Und *Du* kannst bei 100KSLOC *garantieren*, dass keiner dieser Fehler
> > auftritt?
> Spielt das eine wesentliche Rolle, falls man das muß?
Wenn ein solcher Fehler u.U. Menschenleben kosten kann, spielt es eine
sehr große Rolle, ob du die Fehlerfreiheit garantieren kannst. Ganz
besonders, wenn du als Entwickler persönlich für alle Folgen der von
dir gemachten Fehler verantwortlich gemacht wirst.
> Das ist die falsche Frage. «Wie lange dauert es, bis 1000 Zeilen Code
> fehlerfrei sind?»
Nein, du stellst hier die falsche Frage. Woher weißt du, dass in
deinem Quelltext keine weiteren Fehler sind? Wagst du es wirklich,
Software für kritische Systeme zu schreiben und für jeden auftretenden
Fehler persönlich zu haften?
Wenn jemals in einem der von dir geschriebenen Programme ein Fehler
auftauchte/gefunden wurde, nachdem du das Programm für den
Produktionsbetrieb freigegeben hattest, solltest du ganz schnell mal
von deinem hohen Ross 'runterkommen.
> > Ein formale Beschreibung, deren Konsistenz Du bitte
> > *wie* nachweist?
> Wem gegenüber?
Den Angehörigen des Opfers deiner Fehler... und dem Staatsanwalt, der
dich wegen fahrlässiger Tötung anklagt.
> Bitte? «Man kann keine Algorithmen schreiben, deren Speicherverbrauch
> über die vollständige Laufzeit O(1) ist?», sagen wir mal trivial
> dadurch, daß man eine maximale Anzahl an mallocs durchführt und die
> allozierten Objekte weiterverwendet. Das gibt dann eine Invariante,
Und? Damit hast du effektiv eine statische Speicherverwaltung und der
Kern der dynamischen Speicherverwaltung, nämlich die
Unvorhersehbarkeit des notwendigen Speichers, bleibt außen vor.
Dann kann man aber eigentlich auch gleich auf die mallocs
verzichten. :)
> Sprachen geschrieben werden, die die verwantwortlichen Autoren auch
> beherrschen. Solche Anforderungen sind für Übersetzer(!!)
Wobei du unter "beherrschen" offensichtlich verstehst, dass man keine
Fehler macht (die man nicht trivial in ein paar Stunden debugging
garantiert findet und eliminiert).
Das ist eine reichlich naive (oder ziemlich arrogante) Sichtweise.
> > Manchmal sind Abstraktionen der bessere Weg.
> Das halte ich für «debatable». Weniger Komplexität ist der bessere
> Weg.
It depends?!
--
Stefan.
Georg Bauhaus
: ['=' bedeutet?]
: Das ist alles herzlich irrlevant, denn es handelt sich bis auf den
: ersten um externe Faktoren (dh Gegenst?nde einer getrennten
: Betrachtung).
Fuer SPARK ist das genau nicht eine getrennte Betrachtung,
sondern wesentliches Kriterium. Ermoeglicht u.a. durch eine
entsprechend eingeschraenkte und ergaenzte Sprache.
:> Faellt es dir hier so leicht, sagen wir innerhalb von 2 min,
:> diese Angaben fuer einen Echtwelt-Wartungsfall zu machen?
: Es sollte.
Tat es mal?
:> Kommt drauf an. Wenn irgendwo long in einem C Programm steht,
:> ist damit noch nicht gesagt, welche Teilmenge von Zahlen in der
:> entsprechenden Groesse enthalten sein werden.
: F?r jede Implementierung schon. Gegen Fehlverwendung hilft das
: allerdings wenig.
Richtig, aber es ist moeglich
a/ Sprachen zu verwenden, die den Typ-Bereich zahlgenau angeben,
und pruefen,
b/ Teile der Implementierungs-Abhaengigkeiten im quellcode zu
behandeln, so das ein Implementierungs-Wechsel keine manuelle
Neuerstellung von Programmteilen erfordert.
c/ Sprachen/tools zu verwenden, die, an Z spezifikationen angelehnt,
versuchen, Fehlverwendungen zu verhindern,
:> (Assertions als Beispiel zur Explizitheit des semantischen
:> Inhalts eines Programms: Sie sind in einigen Sprachen
:> mehr, in anderen weniger explizit angebbar. Es sei denn du findest
:> es vorteilhaft, wenn die Programmierer, sagen wir die von dir
:> genannten "Engineers", diese Pruefungs-Anweisungen und deren Handling
:> repetitiv und explizit selbst schreiben, Mechanismen, die sonst in
:> Sprachen enthalten sind.)
: Kaum.
Wenn "kaum" sich auf "vorteilhaft finden" bezieht, kann ich davon
ausgehen, dass dir Vor/Nachbedingungen, (In)Varianten, als Sprach-
Bestandteil wuenschenswert erscheinen?
Gruesse,
Georg
Rainer Weikusat
> Rainer Weikusat <weik...@students.uni-mainz.de> writes:
> > > > Das «Verständnis» sagt per se gar nichts aus. Aber der Quelltext tut
> > > > das: Er ist eine vollständige Beschreibung dessen, was die Software
> > > > zur Laufzeit tun wird.
>
> > > Nein, diese Beschreibung ist mitnichten vollstaendig. Was tut das
> > > System, wenn die Software einen Zeiger dereferenziert, der auf ein
> > > zufaellig bereits freigegebenes Objekt zeigt?
>
> > Wie passiert das ohne im Quellcode auffindbar zu sein?
>
> Falsche Frage! Du hast behauptet, der Quelltext sei eine
> *vollständige* Beschreibung dess, was die Software zur Laufzeit tun
> wird. Was also tut die Software bei einem solchen Fehler?
Sie enthält ihn. Wahlweise bekomme ich eine exception, überschreibe
die Interruptvektorentabelle, erhälte den Wert 0 etc pp.
> Du kannst das nicht ausschließlich aus dem Quelltext heraus
> beantworten, weil du die exakte Semantik bestimmter
> Bibliotheksfunktionen kennen musst. Richtig. Also kann der Quelltext
> keine *vollständige* Beschreibung des Laufzeitverhaltens sein.
Er enthält keine vollständige Beschreibung aller konkreten Ereignisse,
die das Programm auslösen kann. Das ist aber nicht dasselbe.
> > > Und *Du* kannst bei 100KSLOC *garantieren*, dass keiner dieser Fehler
> > > auftritt?
>
> > Spielt das eine wesentliche Rolle, falls man das muß?
>
> Wenn ein solcher Fehler u.U. Menschenleben kosten kann, spielt es eine
> sehr große Rolle, ob du die Fehlerfreiheit garantieren kannst.
Suche bitte via google nach 'Therac-25' für einen kurzen Überblick,
welche Todesfolgen durch software malfunction den (US-amerikanischen)
Regulierungsbehörden anscheinend noch genügen, bloß Nachbesserungen zu
fordern.
> > Das ist die falsche Frage. «Wie lange dauert es, bis 1000 Zeilen Code
> > fehlerfrei sind?»
>
> Nein, du stellst hier die falsche Frage. Woher weißt du, dass in
> deinem Quelltext keine weiteren Fehler sind?
Nein, die Frage wäre, woher *Du* das wissen kannst, falls die Quellen
von mir sind.
> Wagst du es wirklich, Software für kritische Systeme zu schreiben
> und für jeden auftretenden Fehler persönlich zu haften?
Dafür, daß keine Katastrophen stattfinden in jedem Fall bzw dafür, daß
dokumentiert ist, welche Katastropen stattfinden könnten.
> Wenn jemals in einem der von dir geschriebenen Programme ein Fehler
> auftauchte/gefunden wurde, nachdem du das Programm für den
> Produktionsbetrieb freigegeben hattest, solltest du ganz schnell mal
> von deinem hohen Ross 'runterkommen.
Der letzte, an den ich mich erinnern könnte, der nicht aufgrund
unbekannter externer Faktoren auftrat, wie Fehlfunktionen anderer
Programme, liegt schon ein paar Jährchen zurück.
NB: Irgendwelche Dinge, die ich ggf mit labels wie 'alpha' oder 'beta'
veröffentliche, gehören da nicht dazu.
> > > Ein formale Beschreibung, deren Konsistenz Du bitte
> > > *wie* nachweist?
>
> > Wem gegenüber?
>
> Den Angehörigen des Opfers deiner Fehler... und dem Staatsanwalt, der
> dich wegen fahrlässiger Tötung anklagt.
Beide sind nicht qualifiziert, einen solchen Nachweis zu verstehen,
obwohl sie das lernen könnten (Faustregel: Wer etwas nicht
grundsätzlich allgemeinverständlich erklären kann, hat auch keinen Durchblick).
> > Bitte? «Man kann keine Algorithmen schreiben, deren Speicherverbrauch
> > über die vollständige Laufzeit O(1) ist?», sagen wir mal trivial
> > dadurch, daß man eine maximale Anzahl an mallocs durchführt und die
> > allozierten Objekte weiterverwendet. Das gibt dann eine Invariante,
>
> Und? Damit hast du effektiv eine statische Speicherverwaltung und der
> Kern der dynamischen Speicherverwaltung, nämlich die
> Unvorhersehbarkeit des notwendigen Speichers, bleibt außen vor.
Nein, damit habe ich effektiv eine Speicherverwaltung, die im
Rahmen konstanter Limits operiert.
> Dann kann man aber eigentlich auch gleich auf die mallocs
> verzichten. :)
>
> > Sprachen geschrieben werden, die die verwantwortlichen Autoren auch
> > beherrschen. Solche Anforderungen sind für Übersetzer(!!)
>
> Wobei du unter "beherrschen" offensichtlich verstehst, dass man keine
> Fehler macht (die man nicht trivial in ein paar Stunden debugging
> garantiert findet und eliminiert).
Man kann Programme so schreiben, daß das geht, wenn man sich selber
auf die Finger haut, bevor das der Compiler tut.
> > > Manchmal sind Abstraktionen der bessere Weg.
>
> > Das halte ich für «debatable». Weniger Komplexität ist der bessere
> > Weg.
>
> It depends?!
Dem würde ich nicht zustimmen: Ich halte eine simplere Lösung immer
für besser (wohlgemerkt: eine Lösung, keine Annäherung).
Rainer Weikusat
> Rainer Weikusat <weik...@students.uni-mainz.de> writes:
> > Stefan Nobis <ste...@snobis.de> writes:
> > > Rainer Weikusat <weik...@students.uni-mainz.de> writes:
> > > > Das «Verständnis» sagt per se gar nichts aus. Aber der Quelltext tut
> > > > das: Er ist eine vollständige Beschreibung dessen, was die Software zur
> > > > Laufzeit tun wird.
>
> > > Davon träumst du, oder?
>
> > Eine nichtdeterministische Maschine kann ich auch «formal» nicht
> > «verifizieren». Das sich praktische Vorteile dadurch ergeben, daß die
> > Semantik unter der Annahme einer deterministischen Maschine bekannt
> > und sinnvoll ist, sollte nachvollziehbar sein.
>
> Es wäre schön, wenn du, mal zur Abwechslung, auf die Kernaussagen
> eingehen könntest, statt wahllos themenflucht zu begehen.
>
> Wieso schafelst du von nichtdeterministischen Maschinen? Was tut das
> zur Sache? Es geht um konkrete, deterministische Rechner, reale
> Computer mit Betriebssystemen, vielen Bibliotheken, Laufzeitumgebung
> der verwendeten Programmiersprache etc.
>
> Und in diesem Kontext ist der Quelltext eben gerade keine
> *vollständige* Beschreibung dessen, was die Software zur Laufzeit
> tut,
Doch. Falls da drinsteht 'Software macht syscall #6 mit folgenden
Argumenten .. .. ..', dann tut sie genau das. 'man abstraction'.
> > > Wenn es um kritische Systeme geht, kann man getrost davon ausgehen,
> > > dass *kein* einziger Mensch jemals korrekten, sprich 100%
> > > fehlerfreien, Code schreibt.
>
> > Gründet sich die Annahme, daß die Mehrzahl aller «kritischen» Systeme
> > mehr oder minder irreparabel kaputt ist, eigentlich auf praktische
> > Erfahrungen? Gruselig ...
>
> Ich schrieb, dass kein Mensch 100% fehlerfreien Code zu schreiben in
> der Lage ist. Das Gegenteil müsstest du mir erstmal beweisen, da es
> diverse Studien gibt, die empirisch nachgewiesen haben, dass ab
> ca. 30.000 bis 50.000 Zeilen Quelltext garantiert eine gewisse
> Mindestzahl an Fehlern vorhanden ist.
Eine Statistik ohne statistisch abgesicherte Datenbasis ist Müll.
> Und solche Fehler eliminiert man eben nur mit sehr aufwendigen (und
> leider teuren) Verfahren. Das Genie, dass nur mit Texteditor und
> Compiler bewaffnet ohne weitere (technische) Hilfsmittel (von Doku mal
> abgesehen :)), fehlerfreie Systeme mit mehreren zehntausend Zeilen
> Quelltext erstellen kann, musst du mir echt mal zeigen.
Das ist eine Frage des investierten Zeitaufwandes.
> > «Die Achterbahn des Schreckens, Teil II». Ist Dir klar, das jede
> > automatisch verhinderte «Fehlerklasse» ein weiterer kludge ist, der
> > um einen mittlerweile bekannten möglichen Fehler herumwürgt?
>
> Könntest du das mal näher ausführen? Ich verstehe nicht, was du
> meinst.
Woher nimmst Du die Gewissheit, daß die Menge möglicher
'Fehlerklassen' endlich ist?
> Oder spielst du darauf an: Mensch kennt ja die möglichen
> Fehlerquellen, also sollte es kein Problem sein, die Fehler zu
> vermeiden.
IdR ist es das auch nicht. Kannst Du Dir vorstellen, warum man
Handwerker drei Jahre lang systematisch üben läßt? Wer tut das bei
Programmierern nach Maßgabe welcher Voraussetzungen?
> Und du hast ja auch noch nie in deinem Leben einen Fehler ein zweites
> Mal begangen, gelle.
>
> Mal konkret: Wie stellst du dir eigentlich die Entwicklung von
> z.B. der Steuer-Software der Ariane vor?
"100 Millionen dressierte Affen".
> Auf die Genialität der Programmierer hoffen,
Herrgott ...
"[...] das Genie, das ausgebildete Kunsttalen, [...]"
(JWG)
> > > Aber auf einem völlig anderen Abstraktionsniveau. Auf diese Weise
> > > bekomme ich etliche neue Fehlerquellen.
>
> > Zwischenschritt eliminieren ;-).
>
> Abstraktions- und Kontrollebenen eliminiert. Für die Entwicklung eines
> sicheren und robusten LDAP-Servers wahrscheinlich sinnvoll, für obiges
> Beispiel der Ariane-Steuerung, zumal bei großen Teams mit den dabei
> auftretendem Kommunikationsoverhead und -problemen, halte ich es für
> ein sehr großes Problem, diese Zwischenschritte zu eliminieren.
Dann bekommt man potentielle Übersetzungfehler. Ob das problematisch
ist, spielt absolut keine Rolle.
> Diese Zwischenschritte erlauben in einem (größeren) Team eine bessere
> Kommunikation, da durch eine gemeinsame, formalisierte Sprache erstmal
> dafür gesorgt wird, dass auch wirklich alle von derselben Sache
> sprechen und dasselbe meinen. Die Quelltextebene wäre hier (bei
> komplexen Systemen und größeren Teams) zu sehr mit Details belastet,
> so dass der Blick für das Wesentliche zu schnell verloren geht.
Dann ist das ein starkes Indiz dafür, daß der Quelltext Müll ist.
> > > > C-Programme beschreiben normalerweise Registermaschinen.
>
> > > So ein Quark. C basiert noch nicht einmal auf einer klaren
>
> > Offensichtlich kann man jedes Programm in einer imperativen
> > Programmiersprache auch als spezialisierten IC realisieren. Ein
> > Programm ist eine virtuelle Maschine, die auf einer etwas
> > allgemeineren simuliert wird.
>
> Eine Registermaschine ist ein klar definierter Begriff. Und eine
> solche Registermaschine wird durch kein C Programm beschrieben (man
> kann aber C Programme in Programme für Registermaschinen
> übersetzen).
>
> Buzzwords und schwammige Ausdrucksweisen helfen dir da nicht weiter.
Mich beschleicht eher das Gefühl, es wäre sinnlos, mit Leuten zu
diskutieren, denen so elementare Konzepte nicht vertraut sind.
> Und um in deinem Begriffswirrwarr zu bleiben: Dadurch, dass VM A auf
> VM B simuliert wird, ist VM A nicht gleich eine Beschreibung von VM
> B.
Eine grandios sinnlose Aussage. Bitte behaupte nicht, die wäre von
mir.
> Bleibt nur die Frage wie viele solcher Genies es gibt, die fehlerfrei
> programmieren können. Ob die Anzahl reicht, um den realen Bedarf an
> Software zu decken? Ich habe da so meine Zweifel.
Weil vor jedem Computer einer sitzt, der sich nicht damit auskennt,
und alle anderen deswegen wegbeißt, weil er dafür toll den Chef
belabern kann (der auch keinen Plan von der Materie hat) handelt es
sich um eine vollkommen hypothetische Fragestellung: Niemand würde so
jemanden jemals ein Programm schreiben lassen.
> > > Wieso sind einige Abstraktionskonzepte, wie Rekursionen u.a., wichtig
> > > und gut und andere wieder völlig überflüssig und böse?
>
> > Ich hatte nichts von «überflüssig» oder «böse» geschrieben.
>
> Nicht wörtlich, aber deine Aussagen suggerierten dies.
Dein Problem.
> > > Um Fehlerquellen zu vermeiden. Mit Adressen, zumal ihrer
> > > Repräsentation(!) in C, kann man rechnen,
>
> > Das ist bei Werten so üblich.
>
> Bei Konstanten nicht.
Ach, die Summe zweier Konstanter Zahlen ist nicht berechenbar?
> > > mit Referenzen (einer anderen Repräsentation) kann man nicht rechnen
> > > -- damit sind wilde Zeiger z.B. (nahezu) unmöglich.
>
> > Das hat nichts mit «Rechnen» zu tun, sondern damit, ob die abstrakte
> > Maschine, die von der Sprache beschrieben wird, Referenzen mit
> > beliebigen Werten gestattet.
>
> Nein, das hat damit zu tun, dass der Ausdruck "Referenz"
> i.a. impliziert, dass es sich um etwas relativ konstantes handelt,
> d.h. man kann immer nur ein existierendes Objekt referenzieren und
> nicht eine beliebige Speicheradresse (es sei denn, diese wäre ein
> zulässiges Objekt, was jedoch in den meisten Sprachen, die solche
> Abstraktionskonzepte bieten, nicht der Fall ist).
>
> Referenzen können also sehr wohl beliebige Werte annehmen, jedoch muss
> dieser Wert zu einem exitierenden, gültigen (dereferenzierbaren)
> Objekt gehören.
Also können sie *keine* beliebigen Werte annehmen.