Formalisierung VL 13 Flashcards
Welche Informationen aus dem Interface einer objektorientierten Software sind formal beschrieben, welche informal?
Interfaces sind nur semi-formale Spezifikationen. Die Signaturen sind formal festgelegt, aber es fehlt die Semantik der Implementationen. Wir können die Semantik lediglich in
Form von Kommentaren angeben
(also nur informell).
Erläutere die Schwierigkeit bei der Prüfung der Korrektheit von Software, wenn keine formale Spezifikation vorliegt.
- Korrektheit von Software steht immer in Relation mit ihrer Spezifikation
- formaler Nachweis der Erfüllung schwierig
- dafür muss aber formale Spezifikation definiert sein
Wozu sollte man die Semantik von Programmen spezifizieren?
- Verhalten eines Programms lässt sich statisch feststellen, ohne es auszuführen
- Korrektheit nachweisbar
- > Semantik syntaktisch beschreiben
- > auf formale Ausdrücke Ableitungsregeln anwenden, um Aussagen des Programms zu beweisen
Was ist denotationale Semantik?
Die Wirkungsweise eines Programms wird als partielle Abbildung eines Speicherzustandes in einen anderen verstanden.
Sei Z die Menge aller möglichen Speicherzustände. Die Wirkung, die eine Anweisung A auf einen Zustand hat, ist formal gesprochen eine Abbildung
f[A]: Z->Z
Was ist operationale Semantik?
Ein konkretes Programm durch ein semantisch gleiches aber abstraktes Programm ersetzen
Was ist axiomatische Semantik?
Nenne die Bestandteile eines abstrakten Datentyps
ADT ist eine Zusammenfassung von Wertebereichen und Operationen zu einer Einheit
Ein ADT besteht aus:
- Typen
- Funktionen
- Axiomen
- Vorbedingungen
