Seite 1 von 1

Hausübung 4.2 (b)

Verfasst: 3. Feb 2010 11:34
von s_n
Hi,

Wie behandelt man die Stuck Terme wenn man die Sequenzen bauen will?
Lässt man die weg ?
Ich hab im Skript gesucht und mir die Übungen angeschaut, aber nichts dazu gefunden.

Re: Hausübung 4.2 (b)

Verfasst: 3. Feb 2010 14:59
von -me-
Wie auf Seite 18 von Kapitel 9 steht wird * durch den Prozeduraufruf mit gleichen Parametern ersetzt.

Re: Hausübung 4.2 (b)

Verfasst: 3. Feb 2010 15:36
von Simon Siegler
s_n hat geschrieben: Wie behandelt man die Stuck Terme wenn man die Sequenzen bauen will?
Lässt man die weg ?.
In Aufgabe 4.2 (b) spielen Stuck-Terme keine Rolle. Wie in Teilaufgabe (a) vorzugehen ist, wurde bereits erläutert.

Re: Hausübung 4.2 (b)

Verfasst: 24. Mär 2010 21:40
von s_n
Wie sehen sieht denn die 2. HPL-Sequenz mit der IH aus?
Ich komm einfach auf keine brauchbare Sequenz.

Für die erste habe ich seqI1 = <{?ø(k)}, ø ||- f(k, append(k, l)) = l>

Re: Hausübung 4.2 (b)

Verfasst: 24. Mär 2010 21:49
von robert.n
s_n hat geschrieben:Wie sehen sieht denn die 2. HPL-Sequenz mit der IH aus?
Ich komm einfach auf keine brauchbare Sequenz.
Mein Vorschlag:
\(seq_{I2} = \left\langle \{ ?::(k) \}, \{ \forall l : list[\text{@I}] \;\; f(tl(k), append(tl(k), l)) = l \} \models f(k, append(k, l)) = l \right\rangle\)

Re: Hausübung 4.2 (b)

Verfasst: 24. Mär 2010 22:19
von oren78
robert.n hat geschrieben:
s_n hat geschrieben:Wie sehen sieht denn die 2. HPL-Sequenz mit der IH aus?
Ich komm einfach auf keine brauchbare Sequenz.
Mein Vorschlag:
\(seq_{I2} = \left\langle \{ ?::(k) \}, \{ \forall l : list[\text{@I}] \;\; f(tl(k), append(tl(k), l)) = l \} \models f(k, append(k, l)) = l \right\rangle\)
müsste es nicht:

\(seq_{I2} = \left\langle \{ \neg \emptyset(k) \}, \{ \forall l : list[\text{@I}] \;\; f(tl(k), append(tl(k), l)) = l \} \models f(k, append(k, l)) = l \right\rangle\)

lauten...?

Re: Hausübung 4.2 (b)

Verfasst: 24. Mär 2010 22:42
von Ro-
Edit: ok das stimmte dann natuerlich nicht, wenn das in der MuLoe falsch ist. Zumindest ist es jetzt eindeutig ;)

Re: Hausübung 4.2 (b)

Verfasst: 24. Mär 2010 23:45
von robert.n
Nein, das ist nicht ganz richtig wie es in der MuLö gemacht wurde. In der Aufgabenstellung ist angegeben, dass die Induktion der Relationenbeschreibung von list[@I] folgen soll. Und die sieht nunmal so aus:
\(\large R_{list[@I]} = \begin{align} \{ & \langle \{ ?\emptyset(k) \}, \; \emptyset \} \rangle \\ & \langle \{ ?::(k) \}, \; \{\{k/tl(k)\}\} \rangle \} \end{align}\)

Siehe auch hier: http://www.fachschaft.informatik.tu-dar ... 54#p113054

Re: Hausübung 4.2 (b)

Verfasst: 25. Mär 2010 13:39
von s_n
Warum kommen die anderen Hypothesen "not ?ø(l)" und "eq(hd(l),hd(k))" nicht mit in die Sequenz?

Re: Hausübung 4.2 (b)

Verfasst: 25. Mär 2010 14:39
von Simon Siegler
Wie in Kapitel 6 auf Folie 19 definiert werden die Induktionsformeln aus einer Relationenbeschreibung konstruiert. Dabei werden nur die Hypothesen der Relationenbeschreibung berücksichtigt.