weiterreichen der Exeption guard an den aufrufer:

Christian_
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 178
Registriert: 10. Apr 2009 16:30

weiterreichen der Exeption guard an den aufrufer:

Beitrag von Christian_ »

Präsensübung 3.3c)

ich habe 2 unterschiedliche Möglichkeiten average(x,y) in Verifun zu schreiben

Code: Alles auswählen

function average(x, y : nat) : nat <=
if{even(plus(x, y)),
   half(plus(x, y)),
   *}
so bekomme ich eine Exeption Guard bei \(exept_{average}[x, y] = if\{even(plus(x, y)), false, true\}\)


wenn ich aber average als

Code: Alles auswählen

function average(x, y : nat) : nat <=
   half(plus(x, y))
schreibe bekomme ich \(exept_{average}[x, y] = false\)


wieso wird bei der 2. Variante die Exeption von half nicht an average weitergegeben?

und warum hat die gleiche Prozedur, die auf unteschiedliche weise implementiert wird verschiedene Exeption Guards
Omnium rerum principia parva sunt. -Cicero

Christoph Walther
Dozentin/Dozent
Beiträge: 86
Registriert: 1. Nov 2005 18:51

Re: weiterreichen der Exeption guard an den aufrufer:

Beitrag von Christoph Walther »

Nach definition der exception-guard ist alles ok: In der zweiten definition von 'average' kommt kein * vor, also ist die exception-guard = 'false'. Trozdem gibt es bei beiden prozeduren stuck-computations: average1(1, 0) =>! average1(1, 0) und average2(1, 0) =>! half(1).

Was Sie mit "weiterreichen der exception" meinen wird auf andere weise festgestellt: Für jede terminierende prozedur f : s1 x ... x sn -> s erzeugt VeriFun eine sogenannte (terminierende) domainprozedur nabla-f : s1 x ... x sn -> bool mit der bedeutung "nabla-f(t1,...,tn) = true <=> die auswertung von f(t1,...,tn) führt nicht zu einer stuck-computation". (nabla = dreieck mit spitze nach unten; wenn man ein prozedur-icon aufklappt, dann sieht man die domainprozedur; domainprozeduren, deren rumpf identisch 'true' sind, werden nicht angezeigt).

Im beispiel gilt nabla-average1(1, 0) = nabla-average2(1, 0) = false (kann man ja im interpreter ausprobieren). Damit weiß man, daß ein average-aufruf mit den argumenten (1, 0) zu einer stuck-computation führt, egal welche implementierung dabei verwendet wurde. Allgemein kann man mit lemma

LEM <= all x, y : nat if{nabla-average(x, y), even(plus(x, y)), ¬ even(plus(x, y))}

beweisen, daß average-aufrufe genau dann zu stuck-computations führen, wenn die summe der argumente ungerade ist.

Antworten

Zurück zu „Archiv“