 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | ||||||||||||||||||||||||||||||||||||||||||||
| Wissensbrowser starten | ||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Beschriftung sequentieller Programme |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Für eine Übersetzung von Programmen in Kripke Strukturen ist es eine wesentliche Erleichterung, ein beschriftetes Programm vorliegen zu haben, bei dem für jede Anweisung des Programms der Einstiegs- und Ausgangspunkt eindeutig beschriftet ist. Die systematische Durchführung einer solchen Beschriftung wird im folgenden beschrieben.
Um sich nicht auf eine bestimmte Programmiersprache zu beschränken, wird die Beschriftungs-Vorschrift für verschiedene Anweisungsarten definiert, was leicht auf weitere Anweisungsarten übertragen und erweitert werden kann. Ausgehend von einer Anweisung P wird eine beschriftete Anweisung PL folgendermaßen induktiv über die Struktur von P definiert:
Rückkehr zu Modellierung von Programmen | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
| ||||
| ||||
| Beschriftung sequentieller... | ||||
| ||||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
