 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Informelle und formale Spezifikation |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
Spezifikationsverfahren lassen sich auf der Grundlage ihrer Formalität grob in drei Klassen einteilen: Informelle, semiformale und formale Verfahren. Die Abbildung gibt einen Eindruck, wie diese Verfahren arbeiten.
Informelle Spezifikation Informelle Techniken haben kein komplettes Regelwerk zur Erstellung von Modellen. Die Ausdrucksmöglichkeiten werden kaum eingeschränkt. Natürliche Sprache und einfache Schaubilder (Box-And-Arrow-Diagramme) sind Beispiele für informelle Spezifikation. Semiformale Spezifikation Semiformale Verfahren haben eine definierte, eindeutige Syntax. Das kann eine grafische Notation sein, mit präzisen Regeln zur Erstellung der Diagramme oder eine textuelle Notation mit ähnlichen Regeln. Diese graphischen und textuellen Verfahren bieten in der Regel eingeschränkte Überprüfungen der Modelle (z.B. einen Syntax-Checker oder einen Simulator). Beispiele für semiformale Sprachen sind UML und ER-Diagramme. Aktuelle Forschungen beschäftigen sich mit der Abbildung von UML auf eine formale Sprache bzw. mit der Formalisierung von UML. Formale Spezifikation Formale Techniken haben eine streng definierte Syntax und Semantik. Darunter befindet sich ein theoretisches Modell. Eine Spezifikation, die in einer mathematischen Notation mit entsprechenden Symbolen ausgedrückt wird, kann mit mathematischen Methoden auf Widersprüche und Vollständigkeit verifiziert werden. Spezifikationssprachen, welche auf der Prädikatenlogik und Mengenlehre beruhen, sind typische Beispiele. Formale Verfahren erlauben die (teil-) mechanische Verifikation von Programmen oder den Beweis bestimmter Modell- oder Programmeigenschaften. Dies ist mit semiformalen und informellen Verfahren kaum möglich. Formale Spezifikationssprachen sind beispielsweise FOCUS, Z, VDM oder B. Auch die CSP und Petri-Netze fallen in diese Kategorie. Formale Spezifikationssprachen decken unterschiedliche Teile des Software-Entwicklungsprozesses ab. Einige Ansätze gehen nicht über eine reine Notation hinaus. Erst über ein Nutzungskonzept und Werkzeuge wird eine formale Spezifikationstechnik praktisch nutzbar. | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren
| ||||||||||||||
|
