Interpretation von Zusicherungen

[Georg Bauhaus]

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.

[Stefan Reuther]

Post by Georg Bauhaus
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

[Lutz Donnerhacke]

Post by Stefan Reuther
(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").

Nimm SPARK.

[Georg Bauhaus]

Post by Lutz Donnerhacke

Post by Stefan Reuther
(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").

Nimm SPARK.

Das hilft nicht in den #hide-Abschnitten.

[Lutz Donnerhacke]

Post by Georg Bauhaus

Post by Lutz Donnerhacke

Post by Stefan Reuther
(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").

Nimm SPARK.

Das hilft nicht in den #hide-Abschnitten.

Natürlich nicht. Damit weißt Du den Compiler ja explizit an, diese Warnungen
zu unterlassen.

[Georg Bauhaus]

Post by Stefan Reuther
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.

Sind Zusicherungen demnach ein Programmteil, der die intendierte
Logik des Programms berührt?

[Stefan Reuther]

Post by Georg Bauhaus

Post by Stefan Reuther
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.

Sind Zusicherungen demnach ein Programmteil, der die intendierte
Logik des Programms berührt?

Der Begriff "Logik" stört mich hier.

Ein Programm in einer Hochsprache besteht ja aus Teilen, die die
Ausführung beeinflussen (operationelle Semantik) und aus Teilen, die nur
Zusatzinformationen darüber geben, und z.B. die von der Sprach-Grammatik
zugelassenen Programme einschränken: auf einem i386-System ist es völlig
egal, ob man 'long' oder 'int' schreibt, der erzeugte Maschinencode ist
derselbe. Dennoch drückt beides Programmlogik aus, im Falle des
Datentyps "für die 'int'-Variable reicht mir der Wertebereich -32767 ..
+32767". Oder eben: "ich gehe davon aus, dass alle Werte in dieser
Variable zwischen -32767 und +32767 liegen werden". Und das ist das
gleiche, was eine Zusicherung ausdrückt: "ich gehe davon aus, dass
dieser Wert hier >= 0 sein wird".

Insofern berührt die Zusicherung schon die Logik des Programms, nicht
aber die operationelle Semantik. Jedenfalls im Idealfall. Praktisch kann
man ja zumindest in C/C++-Assertions allerlei Ferkeleien machen, die
schon dafür sorgen, dass sich das Programm mit aktivierten Zusicherungen
anders benimmt als ohne. 'assert(ack(100,100) > 100)' oder so.


Stefan

[Florian Weimer]

Sind sie "logischer" Bestandteil des Programms?

Ja, schon allein weil diese Asserts nicht immer seiteneffektsfrei
sind.

[Georg Bauhaus]

Post by Florian Weimer

Sind sie "logischer" Bestandteil des Programms?

Ja, schon allein weil diese Asserts nicht immer seiteneffektsfrei
sind.

Einige der genannten Sprachen negieren solche "schlichten" Überlegungen
zu Seiteneffekten, insofern z.B.

- Prädikate ohne Nebenwirkungen vorgeschrieben sind (Eiffel)

- der Entwicklungsprozess (vulgo: Programmierer) vorsieht,
das Programm so zu entwickeln, als ob Zusicherungen an oder
aus sein können.

Mir schweben ein Prozessor (#1) und ein Hilfsprozessor (#2) vor.
#1 rechnet, #2 wertet assert()s aus. Dabei liest #2 Daten von #1,
kann sie aber nicht schreiben. Die einzige mögliche Wirkung wird
sein, dass der Prozessor #2 den Prozessor #1 anhalten kann.

Ein einfaches Beispiel:

fun teile(ganz x, ganz y) is
assert(y > 0)
return x / y
end fun teile

Ziel: Das ganze Programm (das teile() aufruft) soll keine Überprüfung
von y als Bestandteil von teile() nötig machen. Nach diesem Beweis
kann teile() maximal effizient ausgeführt werden.

;;; Assert-Setup in R15, 0 heißt abgeschaltet.
;;; Programm startet auf Prozessor #1.

L1: NOP
#define ASRT #P,M,N=JMP N
JMPZ R15, L2
#define ASRT #P,M,N=TRNSFR #P,M,N

;;; Programm "Teile X in Y Teile".
;;; Es wird vorausgesetzt: Y > 0.
;;; Ergebnis in R0.

L2: LOAD $X,R1 ;X
LOAD $Y,R2 ;Y
ASRT #2,L3,L4
L3: STOPZ R2
NEG R2,R3
STOPNZ R3
L4: DIV R1,R2,R0