Kurze Frage zum Praktikum1

[fy95olok]

Hi,
ich habe gerade an der Praktikumsaufgabe 1.1 gearbeitet. Im Aufgabenteil e habe ich die Prozedur g implementiert, worauf das Lemma f(x,y) = g(x) oder f(x,y) = g(y) aus der Liste verschwunden ist.

Kann mir jemand sagen warum das passiert? Ich dachte das dieses dann eigentlich grün werden müsste (wenn g(x) richtig implementiert ist).

gruß Flo

[kutschke]

Hallo! Statt "Modify", oder wie das heißt, solltest du "Modify Depending" auswählen, dann sollte es hoffentlich gehen.

[Christoph Walther]

ich habe gerade an der Praktikumsaufgabe 1.1 gearbeitet. Im Aufgabenteil e habe ich die Prozedur g implementiert, worauf das Lemma f(x,y) = g(x) oder f(x,y) = g(y) aus der Liste verschwunden ist.

Vermutlich haben Sie nicht (wie auf dem übungsblatt angegeben) das kommando Change Procedure sondern Modify verwendet. Schauen Sie sich die wirkung dieser kommandos in den unterlagen noch einmal an. Oft ist es so, daß eine prozedur P verändert werden soll, die bereits in anderen programmelementen verwendet wird. Mit anwendung von Modify müssen dann alle programmelemente, die P verwenden, gelöscht werden, da ja nicht garantiert ist, daß nach der modifikation von P die anderen programmelemente noch syntaktisch korrekt sind (man könnte ja weitere parameter hinzufügen oder andere weglassen). Das system löscht aber nur nach bestätigung. Bei Change Procedure kann nur der prozedurrumpf geändert werden, und somit können die verwendenden programmelemente erhalten bleiben. Es gibt auch noch depending versionen von beiden kommandos. Diese beziehen sich auf HPL-beweise, die in jedem fall bei änderung eines programmelements gelöscht werden.

[Flo S]

Also ich habe an dem Aufgabenteil erstmal ewige Zeit probiert, wie das denn überhaupt mit dem Change Procedure gehen soll.
Egal was ich gemacht haben, bei der g war Change Procedure immer ausgegraut und ich konnte es nicht anwählen. Mittels Change Depending hat es dann geklappt.

Bei der Aufgabe 1.3.a) klappt jedoch Change Procedure

[fy95olok]

Jetzt funktioniert es, danke für die schnelle Antwort.

[Christoph Walther]

Also ich habe an dem Aufgabenteil erstmal ewige Zeit probiert, wie das denn überhaupt mit dem Change Procedure gehen soll.
Egal was ich gemacht haben, bei der g war Change Procedure immer ausgegraut und ich konnte es nicht anwählen. Mittels Change Depending hat es dann geklappt.

Man sollte voher schon mal in die manuals schauen, dann geht es mitunter schneller ... .
Wenn ein programmelement im beweis eines anderen programmelements verwendet wird, dann können nur die depending varianten von Change Procedure und Modify ausgeführt werden. Wird dagegen das programmelement in keinem beweis verwendet, so können nur die nicht-depending varianten angewendet werden. Die depending und nicht-depending varianten der kommandos schließen sich also gegenseitig aus. Bei Delete ist das genauso. Aber man muß sich nicht groß darum kümmern - das system meldet ja, welche programmelemente und beweise jeweils gelöscht werden müssen und löscht nichts, bevor der benutzer sein ok gegeben hat.