Re: Spezifikation von Invarianten (design by contract)
Heinrich Moser
r...@zedat.fu-berlin.de (Stefan Ram) writes:
> Die Zuweisung »v := 2;« ändert normalerweise weder den Zustand
> des Druckers noch den der Variablen »i«. Wenn man das alles als
> Invarianten dieser Operation »v := 2;« auflisten wollte, würde
> man nie fertig werden, da es unermeßlich viele andere Variablen,
> Objekte, Aussagen und Geräte gibt, die Invarianten dieser Operation
> sind.
>
> Wenn man nun (wie in »design by contract«) die Invarianten einer
> Operation angeben will, was gibt man dann an (da man laut meinem
> ersten Absatz anscheinend nicht alle angeben kann)?
Invarianten sind nicht Listen von Variablen, die durch die Operation
nicht beeinflusst werden. Invarianten sind Bool'sche Ausdrücke, die
sowohl vor als auch nach jeder Operation gültig sind und werden daher
nicht pro Operation sondern auf höherer Ebene (zum Beispiel Klasse
oder Modul) definiert. Beispiel:
,----
| Modul Weltwirtschaft
|
| private GeldStefan = 100
| private GeldHeinzi = 100
|
| Operation StefanAnHeinzi(Betrag):
| GeldStefan -= Betrag
| GeldHeinzi += Betrag
|
| Operation HeinziAnStefan(Betrag):
| GeldHeinzi -= Betrag
| GeldStefan += Betrag
`----
"GeldStefan + GeldHeinzi = 200" wäre nun eine gültige Invariante
dieses Moduls. Dein Beispiel mit dem Drucker oder der Variable i ließe
sich gar nicht als Invariante ausdrücken, da die Invariante kein
"vorher" und "nachher" kennt und daher "Zustand vor Operation =
Zustand nach Operation" nicht darstellbar ist.
LG,
Heinzi