 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Modellierung sequentieller Programme |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Für die Modellierung sequentieller Programme in Form von Kripke-Strukturen wird im folgenden eine Methode beschrieben, bei der eine Übersetzung der Programme in entsprechende logische Formeln stattfindet. Vorausgesetzt wird dabei, dass die Programme bereits nach der Methode zur Beschriftung sequentieller Programme beschriftet sind.
Ähnlich wie bei der Methode zur Beschriftung sequentieller Programme geht man dann auch bei der Übersetzung sequentieller Programme in Logik erster Ordnung induktiv über die Struktur der Programme vor. Zunächst beschreibt man die Startzustände des Programms P mit folgender Formel, wobei pre(V) eine Formel zur Beschreibung der entsprechenden initialen Variablenbelegungen ist: S0(V,pc) ≡ pre(V) ∧ pc = m. Anschließend gibt man die Übersetzungsprozedur für jeden mögliche Anweisungstyp an, wobei same(V) beschreibt, dass die Belegung aller Variablen aus der Menge V durch Ausführung der betrachteten Anweisung nicht verändert wird:
Rückkehr zu Modellierung von Programmen | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
| ||||
| ||||
| Modellierung sequentieller... | ||||
| ||||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
