Formale Spezifikation

Formale Spezifikation

Eine formale Spezifikation ist die Beschreibung eines Computerprogramms mittels einer Notation, deren Semantik eindeutig definiert ist (einer sogenannten formalen Sprache). Ziel ist die formalisierte, präzise Beschreibung der zu lösenden Aufgabe in einem in sich konsistenten und geschlossenen Modell, um dieses weiterzuverarbeiten.

Mit Hilfe von Zusatzwerkzeugen kann die Einhaltung der Regeln der formalen Sprache und die Integrität des Modells geprüft werden. Weitere Werkzeuge können eine Transformation des Modells in andere formale Sprachen bewirken, z. B. Programmiersprachen, die wiederum mit Compilern in auf Computern ausführbaren Maschinencode übersetzt werden können.

Die Z-Notation ist ein Beispiel für eine formale Spezifikationssprache. Andere sind die Specification Language(VDM-SL) der Vienna Development Method und die Abstract Machine Notation (AMN) der B-Methode.

Weblinks


Wikimedia Foundation.

Игры ⚽ Поможем сделать НИР

Schlagen Sie auch in anderen Wörterbüchern nach:

  • formale Spezifikation — 1. Begriff: Im ⇡ Software Engineering eine Methode der ⇡ Spezifikation, bei der die Aufgaben eines ⇡ Moduls (schwieriger: eines ⇡ Softwaresystems) formal definiert werden, z.B. axiomatisch. 2. Vorteil: Exakte Vorgabe für die ⇡ Implementierung;… …   Lexikon der Economics

  • Formale Methoden — In der Informatik bezeichnet der Begriff der Formalen Methoden eine Vielzahl von natur und ingenieurswissenschaftlichen Techniken zum Modellieren und zur rigorosen Überprüfung von Computersystemen. Formale Methoden basieren in der Regel auf der… …   Deutsch Wikipedia

  • Formale Methode — In der Informatik bezeichnet der Begriff der Formalen Methoden eine Vielzahl von natur und ingenieurswissenschaftlichen Techniken zum Modellieren und zur rigorosen Überprüfung von Computersystemen. Formale Methoden basieren in der Regel auf der… …   Deutsch Wikipedia

  • Formale Verifikation — Verifizierung oder Verifikation (von lat. veritas, Wahrheit und facere, machen) ist der Nachweis, dass ein vermuteter oder behaupteter Sachverhalt wahr ist. Der Begriff wird unterschiedlich gebraucht, je nachdem, ob man sich bei der… …   Deutsch Wikipedia

  • Spezifikation — I. Informatik:Begriff aus dem ⇡ Software Engineering; zahlreiche unterschiedliche Bedeutungen. 1. Phase im Software Life Cycle: (1) Synonym für ⇡ Anforderungsdefinition; (2) Synonym für Entwurf; (3) je nach ⇡ Phasenmodell auch eine Phase mit… …   Lexikon der Economics

  • Befehlssatzarchitektur — Eine Befehlssatzarchitektur (engl. Instruction Set Architecture, kurz: ISA) ist – vereinfacht gesagt – die formale Spezifikation bestimmter Verhaltensweisen eines Prozessors aus Sicht seines Programmierers, auf die sich dieser bei der… …   Deutsch Wikipedia

  • Instruction Set Architecture — Eine Befehlssatzarchitektur (engl. Instruction Set Architecture, kurz: ISA) ist – vereinfacht gesagt – die formale Spezifikation bestimmter Verhaltensweisen eines Prozessors aus Sicht seines Programmierers, auf die sich dieser bei der… …   Deutsch Wikipedia

  • Verifizierung — oder Verifikation (von lat. veritas ‚Wahrheit‘ und facere ‚machen‘) ist der Nachweis, dass ein vermuteter oder behaupteter Sachverhalt wahr ist. Der Begriff wird unterschiedlich gebraucht, je nachdem, ob man sich bei der Wahrheitsfindung nur auf… …   Deutsch Wikipedia

  • Theoretische informatik — Mindmap zu einem Teilbereich der Theoretischen Informatik Die Theoretische Informatik beschäftigt sich mit der Abstraktion, Modellbildung und grundlegenden Fragestellungen, die mit der Struktur, Verarbeitung, Übertragung und Wiedergabe von… …   Deutsch Wikipedia

  • IT-Sicherheitskriterien — Die Deutschen IT Sicherheitskriterien (ITS oder ITSK, auch bekannt als Grünbuch) sind eine 1989/1990 von der Zentralstelle für Sicherheit in der Informationstechnik (heute BSI) erarbeitete Richtlinie für die Bewertung und Zertifizierung von… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”