 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | ||||||||||||||||||||||||||||||||||||||||||||||
| Wissensbrowser starten | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Beispiel: Formale Spezifikation in Z |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Das nachfolgende Beispiel stammt aus einem der meistzitierten Artikel zu formalen Methoden, er wurde 1990 von Anthony Hall (Praxis Critical Systems) geschrieben: Seven Myths of Formal Methods.
In einer Fallstudie haben Hall und seine Mitarbeiter ein System in Z spezifiziert, das eine Menge von Dokumenten und eine Menge von Tasks enthält. Dokumente und Tasks werden in der Spezifikation nicht näher definiert, sie werden lediglich über die Bezeichner DOC und TASK referenziert. Die nachfolgende Abbildung zeigt das Z-Schema TasksAndDocuments, welches das System beschreibt. 
Das P symbolisiert in Z eine Menge. „documents: P DOC“, bedeutet, dass documents eine Menge mit Elementen des Typs DOC ist. TasksAndDocuments besteht aus einer Menge von Tasks und Documents. Der Zuordnungspfeil bei outputTask ordnet jedem DOC einen TASK zu. Es existiert also kein Dokument ohne einen Task, der es produziert hat. Zwei Aussagen verfeinern die Zuordnung weiter, „dom outputTask = documents“ bedeutet: outputTask gilt für alle DOC aus documents. Jedem Dokument wird demnach ein Task zugeordnet. „ran outputTask = tasks“ bedeutet: Jeder Task erzeugt mindestens ein Dokument. Die Informationen aus dem Z-Schema werden zusätzlich über begleitende Texte erläutert und beschrieben. Operationen werden ebenfalls als Z-Schema angegeben. Die Funktion RemoveDocument entfernt ein Dokument. Da jedem Dokument ein Task zugeordnet ist, werden sowohl das Dokument als auch der Task gelöscht, wenn der Task nur dieses Dokument produziert hat. 
Das Delta-Symbol vor TasksAndDocuments gibt an, dass RemoveDocument den Zustand von TasksAndDocuments ändert. Eingabeparameter der Funktion werden über „?“ festgelegt. Das zu entfernende Dokument wird mit dem Eingabeparameter oldDoc festgelegt, sein Datentyp ist DOC. Danach wird angegeben, dass der Eingabeparameter oldDoc sich in TasksAndDocuments befinden muss. oldDoc ist Element von documents. Das Resultat der Funktion wird über die letzte Zeile beschrieben. Dazu wird die geänderte Funktion outputTask’ angegeben, sie entsteht aus outputTask durch Entfernen (hier durch ein spezielles Symbol dargestellt) des Documents oldDoc. Weitere Konsistenzbedingungen werden automatisch sichergestellt: oldDoc wird aus documents entfernt. Der erzeugende Task wird aus tasks entfernt, wenn er kein weiteres Dokument erzeugt. | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
 | Übergeordnet | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| ||||
| Beispiel: Formale Spezifikation... | ||||
| ||||
| ||||
| ||||
| ||||
| Literaturhinweise | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
