Modul 7 - Induktion über Herleitung in C (1) - Seite 12

Monster
Neuling
Neuling
Beiträge: 5
Registriert: 11. Feb 2016 13:02

Modul 7 - Induktion über Herleitung in C (1) - Seite 12

Beitrag von Monster » 7. Dez 2017 11:52

Hallo,

im Modul 7, Seite 12, Gliederungspunkt 2, zu r:= steht:

𝑃 (r≔(<𝑋≔𝑎,𝜎>→𝜎 [𝑋\𝑛],(ℋ1))

warum ändert sich hier nicht der Zustand von 𝜎→𝜎' ?

Ich hätte hier 𝑃 (r≔(<𝑋≔𝑎,𝜎>→𝜎' [𝑋\𝑛],(ℋ1)) geschrieben.

Gruß Fedor

Markus Tasch
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 124
Registriert: 11. Sep 2015 10:57

Re: Modul 7 - Induktion über Herleitung in C (1) - Seite 12

Beitrag von Markus Tasch » 7. Dez 2017 13:50

Hallo,

dies entspricht einer Herleitung, die als letzte Kalkülregel die Regel r:= anwendet. Für diese gilt in der Seitenbedingung \sigma'=\sigma[X\n]. Dementsprechend kann \sigma' durch \sigma[X\n] in dem hergeleiteten Urteil ersetzt werden.

Dein Vorschlag würde erlauben, dass im Endzustand alle Variablen beliebig belegt sein können außer X welches mit n belegt sein muss.
Markus Tasch, M.Sc.
Modeling and Analysis of Information Systems
Department of Computer Science, TU Darmstadt
http://www.mais.informatik.tu-darmstadt.de

Antworten

Zurück zu „Archiv“