Axiome aus Prozedurdefinitionen

brotkasten
Windoof-User
Windoof-User
Beiträge: 39
Registriert: 17. Jan 2005 08:20

Axiome aus Prozedurdefinitionen

Beitrag von brotkasten »

Ich habe eine Frage zur Folie 18 im Kapitel 9. Da ist unten das Axiom \(AX_{last}\) gegeben, und zwar als
\(\forall x:list[@T].~last(k)\equiv~if_{@T}\{?\emptyset(k),\dots\}\). Muss ich nicht auf der rechten Seite der
Gleichheit, also im axiomatischen Prozedurrumpf \(R_{last}\) selbst, die Axiome soweit wie möglich benutzen?
Den Teil\(?\emptyset(k)\) hätte ich wahrscheinlich als \(eq_{list[@T]}(tl(k),\emptyset)\) geschrieben. Sollte das
nicht eigentlich so sein? Wäre das vekehrt? Oder ist das einfach egal?

Benutzeravatar
oren78
BSc Spammer
BSc Spammer
Beiträge: 1373
Registriert: 17. Nov 2006 17:47
Wohnort: Darmstadt

Re: Axiome aus Prozedurdefinitionen

Beitrag von oren78 »

also wie ich das verstanden habe schreibst du auf der rechten seite im prinzip nur den proc-body hin
(also nichts weiter als den rumpf deiner prozedur)...die 3 dinge die man beachten muss, hoffe
ich übersehe da nichts sind:
------------------------------------------------------------------------------------------------------------------------------------------
1.) das struct in \(if_{struct} \lbrace \ldots \rbrace\) muss mit den jeweiligen return-value ersetzt werden

2.) gleichheiten (dieser form: \(x = 0\)) wandelst du um in: \(eq_{struct}(x, 0)\) gleichheiten der form: \(?0(x)\) übernimmst du 1:1

3.) falls exceptions auftreten, dann wie's oben auf der folie steht:
------------------------------------------------------------------------------------------------------------------------------------------
Jedes Vorkommen von “*” im Prozedurrumpf wird im Axiom durch
Prozeduraufruf (mit identischer Parameterliste) ersetzt
ansonsten (hoffe ich) heißt es hier copy & paste des rumpfes deiner prozedur ;-)
"Unter allen menschlichen Entdeckungen sollte die Entdeckung der Fehler die wichtigste sein.", Stanisław Jerzy Lec

brotkasten
Windoof-User
Windoof-User
Beiträge: 39
Registriert: 17. Jan 2005 08:20

Re: Axiome aus Prozedurdefinitionen

Beitrag von brotkasten »

Ja, Danke. Ich hätte das gerne nur bestätigt :D
Die Klausur ist ja nicht mehr lange hin, ich habe auch kein Problem damit
das auf die von Dir beschriebene Art und Weise zu lösen (sollte ich zumindest hinbekommen),
nur will ich halt in der Klausur keine Federn lassen ...

Simon Siegler
Computerversteher
Computerversteher
Beiträge: 369
Registriert: 16. Apr 2007 09:12

Re: Axiome aus Prozedurdefinitionen

Beitrag von Simon Siegler »

Das Vorgehen ist in Kapitel 9 beschrieben, auf Folie 14 das allgemeine Prinzip und auf Folie 18 das Vorgehen bei unvollständig definierten Prozeduren.

Antworten

Zurück zu „Archiv“