This flashcard is just one of a free flashcard set. See all flashcards!
102
100. Zeigen Sie an einem einfachen Beispiel, wie die symbolische Ausführung funktioniert!
* Im Beispiel ist eine Funkltion swap(a,b)=> a==b; b==a gezeigt
* In dem Beispiel (rechts) zur symbolischen Ausführung zu nachstehendem Algorithmus werden
x := x - y; (1)
y := x + y; (2)
x := y - x; (3)
o lateinische Bezeichner (x, y) für die Programmwelt, während
o griechische Bezeichner (
) für die Symbolwelt stehen.
* In dem Beispiel (rechts) zur symbolischen Ausführung zu nachstehendem Algorithmus werden
x := x - y; (1)
y := x + y; (2)
x := y - x; (3)
o lateinische Bezeichner (x, y) für die Programmwelt, während
o griechische Bezeichner (
) für die Symbolwelt stehen. | * Es werden Substitutionen von Variablen durch symbolische Ausdrücke verwaltet. * Es ist zu zeigen, dass ausgehend von der Vorbedingung die Nachbedingung immer erfüllt ist. |  |
