4. History Rule aus "Behavioral Subtyping Using Invariants and Constraints"

History Rule aus "Behavioral Subtyping Using Invariants and Constraints"

  • ?

    Hallo zusammen,

    nachdem ich mich vor einiger Zeit mit dem Liskov'schen Substitutionsprinzip auseinandergesetzt habe, las ich den Artikel "Behavioral Subtyping Using Invariants and Constraints" von Barbara H. Liskov und Jeannette M. Wing auf http://reports-archive.adm.cs.cmu.edu/anon/1999/CMU-CS-99-156.ps. Für diejenigen, denen das LSP kein Begriff ist, kann Wikipedia einen guten Einblick liefern, http://de.wikipedia.org/wiki/Liskovsches_Substitutionsprinzip.

    Genauer geht es mir bei dem genannten Artikel um die "History Rule", zu der ich einige Fragen habe.

    Im Text finden sich u.a. folgende Angaben, die ich in diesem Zusammenhang für zentral halte:

    http://martinf123.ma.funpic.de/tmp/a.png

    Nun geht es mir um folgende Formel...

    http://martinf123.ma.funpic.de/tmp/b.png

    m.pre und m.post sind Prädikate (im Sinne von Eigenschaften) und P[a/b] steht für das Prädikat P mit jedem Vorkommen von b durch a ersetzt.

    Nun aber zu den Fragen:
    1. Welcher Operator hat eine höhere Priorität, das logische Und oder der Implikationsoperator?
    2. Der Ausdruck im Zähler scheint ein Bool'schen Wert zu besitzen? Genauso scheint das Ergebnis im Nenner ein logischer Wert (wahr oder falsch) zu sein? Wenn aber Zähler und Nenner logische Werte sind, kann doch irgendetwas nicht stimmen, oder wie dividiert man zwei boolesche Werte durcheinander?
    3. Was ist ein Prädikat (im Text "predicate"; als Symbol Phi)? Anscheinend kann es sich ja nicht um ein logischen Wert handeln, oder?
    4. Ist die Syntax P[a/b] verbreitet oder wird das nur per Definition festgelegt?

    Ich bin wie immer um jede Hilfe dankbar... Vlt. kann sich ja sogar jemand den Artikel mal ansehen wenn es die Zeit erlaubt... 🙂

    Grüße Martin

    Anmerkung: Da zurzeit die Möglichkeit, LaTeX zum Setzen von mathematischen Formeln zu verwenden, nicht gegeben ist, habe ich die Formeln als externe Grafiken unter den obigen URIs ausgelagert. Leider war die Umwandlung mit einem Informationsverlust verbunden, weshalb die Qualität nicht berauschend ist.

    0
  • J

    Die Latex-Tags funktionieren zur Zeit leider nicht. Du wirst Dir leider mit ASCII-Grafiken behelfen müssen, oder ein externes Bild verlinken.

    ich vermute aber ich weiß was Dir Bauchschmerzen bereitet. Das ist garkein Bruch, das ist einfach die Notation für eine Schlussregel. http://de.wikipedia.org/wiki/Sequenzenkalk%C3%BCl könnte helfen.

    0
  • ?

    Jester schrieb:

    ich vermute aber ich weiß was Dir Bauchschmerzen bereitet. Das ist garkein Bruch, das ist einfach die Notation für eine Schlussregel. http://de.wikipedia.org/wiki/Sequenzenkalk%C3%BCl könnte helfen.

    Ja stimmt. Damit hast du meine zentrale Frage beantwortet. Vielen Dank für den Hinweis...

    Grüße Martin

    0
  • ?

    Jester, kannst du dir bitte einmal die Formel ansehen und mir vlt. einmal erklären wie ich die Aussage denn zu verstehen habe, da ich den Artikel aus Wikipedia nur teilweise verstanden habe?

    0
  • J

    Wo ich grad dabei bin... da stecken noch ein paar Missverständnisse in Deinen Fragen:

    zu 1) UND bindet normalerweise am stärksten.
    zu 2) Nein, das sind keine boolschen Werte, sondern Schlussregeln. Für die einzelnen Teile dürfen dann Formeln eingesetzt werden und mit Hilfe der Regel daraus neue Formeln abgeleitet werden.

    Etwa so:

    A, A => B
---------
    B

    Die Sachen die da stehen sind nicht per se wahr oder falsch, aber wenn für A und B konkrete Formeln einsetzt und für die das obere wahr ist, dann darfste daraus das ableiten was unten steht.

    1. ein Prädikat ist eine Funktion, die Dir einen Wahrheitswert liefert. Etwa "istGerade" istGerade(2) ist "wahr", istGerade(1) ist "falsch". Das ganze kann natürlich auch mehrstellig sein.

    2. Diese Notation ist glaube ich schon recht verbreitet, ich kann sie mir aber auch nie merken. 😉

    0
  • ?

    Nun kommen zwei weitere Fragen auf...

    a. Wodurch unterscheide ich diese Notation von einem einfachen Bruchstrich? Muss dies dann textuell festgehalten werden?

    b. für welchen Teil kann ich eine Formel einsetzen? Für Phi oder für den ganzen Zähler in dem obigen Beispiel (inklusive der Implikation)? Wie würde soetwas aussehen - wärst du so nett und gibst mir ein Beispiel (nehmen wir als Prädikat x_pre < x_post)?

    Grüße Martin und vielen Dank noch einmal für den sehr hilfreichen Hinweis

    0
  • J

    zu a): aus dem Kontext raus. Wenn es um Logik (und Spezifikationen sind logische Formeln) geht, dann machen Bruchstriche keinen Sinn. Deshalb kommen keine vor.

    b) ist leider ein bißchen schwieriger. Ich muß zugeben, dass ich mit der Notation von denen auch nicht so viel anfangen kann. Ich bin kein Logiker. Nimm Dir mal ein bißchen Zeit und versuch das Papier von vorne zu lesen, da wird die Notation zumindest teilweise erklärt. Ich denke wenn man sich das rausschreibt sind die Chancen das zu verstehen deutlich höher. x_rho ist immer der Vorgängerzustand von x_psi usw.

    0
Anmelden zum Antworten