Interpretation von Zusicherungen

24/05/2013 - 11:24 von Georg Bauhaus | Report spam
Moin,

wenn ein Programmtext Anweisungen zum Überprüfen von Annahmen
enthàlt, bspw. assert() in C, DbC in Eiffel, gleichartige
Ergànzungen in Java usw, dann sind diese Überprüfungen
i.d.R. schaltbar. In C mit dem Pràprozessor, in Eiffel
per Konfiguration usw. Sind sie "logischer" Bestandteil
des Programms?

Eine Interpretation der übersetzen Programme lautet,
dass zwei Programme mit je unterschiedlichem Verhalten
entstehen, wenn die Überprüfungen an- bzw. ausgeschaltet
sind. Eine andere Interpretation lautet, konzeptionell sind
die Überprüfungen vom "eigentlichen" Programm getrennt,
denn sie müssten nicht einmal vom selben Prozessor
durchgeführt werden, sondern könnten auf einer "monitoring
hardware" laufen, hàtten also auf das "eigentliche"
Programm höchstens die eine Wirkung: es geregelt anzuhalten,
wenn eine Überprüfung fehl schlàgt.(*)

Gibt es Gründe, die eine oder andere Interpretation
für richtig oder falsch zu erklàren, insbesondere insofern
Überprüfungen die Entwicklung des Quelltextes durch Programmierer
betreffen, die ihre Annahmen so formal dokumentieren und weiteren
Überlegungen zugànglich machen?

__
(*)Die mir etwas schlicht, formal-mechanisch erscheinende
Einschàtzung der übersetzten Programme nach ihrem
Verhalten in einer gegebenen Implementierung einmal
ausgenommen; sie würde eben davon ausgehen, dass eine
Überprüfung den Programmetext so àndert, wie jede andere
Änderung am "eigentlichen" Programm, also die Frage
in Frage stellen. Ebensowenig hilfreich -- mit Bezug auf
das Entscheidende, nàmlich das Entwickler-Verhalten -- wàre
das triviale Ergebnis, dass die Wirkung des einen oder
anderen Programms etwa mit oder ohne assert() eine andere
ist, was nicht in Frage steht.
 

Lesen sie die antworten

#1 Stefan Reuther
24/05/2013 - 19:27 | Warnen spam
Georg Bauhaus wrote:
Eine Interpretation der übersetzen Programme lautet,
dass zwei Programme mit je unterschiedlichem Verhalten
entstehen, wenn die Überprüfungen an- bzw. ausgeschaltet
sind. Eine andere Interpretation lautet, konzeptionell sind
die Überprüfungen vom "eigentlichen" Programm getrennt,
denn sie müssten nicht einmal vom selben Prozessor
durchgeführt werden, sondern könnten auf einer "monitoring
hardware" laufen, hàtten also auf das "eigentliche"
Programm höchstens die eine Wirkung: es geregelt anzuhalten,
wenn eine Überprüfung fehl schlàgt.(*)

Gibt es Gründe, die eine oder andere Interpretation
für richtig oder falsch zu erklàren, insbesondere insofern
Überprüfungen die Entwicklung des Quelltextes durch Programmierer
betreffen, die ihre Annahmen so formal dokumentieren und weiteren
Überlegungen zugànglich machen?



Ich würde sagen, da wird's langsam philosophisch: ist ein Stück
Programmcode, das im aktuellen Programm aus $grund keine Wirkung hat,
Teil des Programms? Die Frage kann man ja nicht nur für assert stellen,
sondern auch für Code, der in #ifdef __BIG_ENDIAN__ eingeschlossen ist.
Für Funktionen, die gerade nicht aufgerufen werden. Für pragmas, die mit
dem aktuellen Compiler keine Wirkung haben.

Ich sehe die Assertions schon als Programmteil, allerdings als einen,
den auszuwerten der Compiler nicht verpflichtet ist. Genauso, wie ein
C-Compiler nicht verpflichtet ist, irgendwelchen Sinn in die Schlüssel-
worte 'register', 'volatile' oder 'restrict' zu interpretieren.

(In langen Nàchten tràume ich allerdings von Compilern, die mir sagen,
"wenn du hier x reinsteckst, verletzt du vier Stackframes weiter unten
eine Zusicherung").


Stefan

Ähnliche fragen