* Core features brauchen nicht bercksichtigt werden (sind ja eh immer da)
* Ansonsten hat unser FM leider keine Einschrnkungen
* Schwierig festzulegen, dass das FM fix aber beliebig und gltig ist
* Methode zum Abfragen, ob Feature wahr ist muss pure sein, damit pure Methoden auch verfeinert werden knnen

* Kontrakte von Methoden, die optional sind, aber nicht verfeinert werden:
  - Vorbedingung v wird zu "f(Feature) && v" --> Methode darf nur aufgerufen werden, wenn Feature ausgewhlt ist / alternativ mittels Type-Checking
  - Nachbedingung bleibt identisch
  - Methodenbody bleibt identisch, da Methode ja nur mit erfllter Vorbedingung aufgerufen werden darf

* Felder, die optional sind
  - Zugriff verboten, wenn Feature nicht gewhlt ist, kann mit Type-Checking berprft werden
  - Nur kompliziert durch Kontrakte auszudrcken, z.B. Feld-Zugriffe nur ber Getter/Setter und dann Vorbedingung prfen
  
* Methodenverfeinerungen ohne Kontrakte
  - Es werden wie mit FeatureHouse mehrere Methoden generiert
  - jede Verfeinerung enthlt eine Zeile, die berprft, ob das Feature da ist
	  if (!FeatureModel.f(FeatureModel.BackOut))
    		return validStudent__ExamDB(student);

* Invariante, die optional ist
  - Invariant i wird zu "!f(Feature) || i"
  - muss also von allen Methoden erfllt werden, aber i muss nur gelten, wenn Feature gewhlt ist

* Ina:
  - Sieht man nicht in Key immer den Code?
  - SpecificationExtraction, was ist das?

* Fehler in Fallstudie:
  - Konstruktor von Student kann ohne Vorbedingung die Invariante nicht garantieren
  
* Fehler in Key:
  - Reload von RespectsModifies in Exception-Klasse fr beide Konstruktoren
  
* Schwierigkeiten:
  - Konstruktor von ExamDataBase erfllt Invariante, die Feature enthlt
  - "X --> self = null" bei Methoden die Aufruf zu verfeinerter Methode enthalten

##########################

* Batch-modus fr Key vielleicht nchste Woche


  
15 Seiten Springer

Intro

Background
* FOP
* JML+Key

Specitifation of FOP

Variability Encoding for Specification and Implementation (trennen?)

Evaluation

* ExamDataBase
* BankAccount Example

Conclusion

