Informatiker Board | Theoretische Informatik

Informatiker Board » Themengebiete » Theoretische Informatik » Hoare Kalkül

» Hallo Gast [Anmelden|Registrieren]

Letzter Beitrag | Erster ungelesener Beitrag

Druckvorschau | An Freund senden | Thema zu Favoriten hinzufügen

Hoare Kalkül

Autor

Beitrag

« Vorheriges Thema | Nächstes Thema »

JanS
Grünschnabel

Dabei seit: 17.01.2009
Beiträge: 6

Hoare Kalkül

Zitatantwort auf diesen Beitrag erstellen

Hallo
Folgende Aufgabe mit der ich nicht zurecht komme..:

{true}

x=5
res=x*x-6
re=res mod 5

{res=4}

ich kann mit der Vorbedingung nix anfangen bzw weiß nich wie ich die einsetzen soll..

mfg
Jan

17.01.2009 01:48

Nehmen Sie JanS in Ihre Freundesliste auf

kiste
Mitglied

Dabei seit: 06.05.2007
Beiträge: 29

Das heißt einfach das es keine Vorbedingung gibt.
Fange einfach an:
{true}
x = 5
{true ^ x=5} = {x=5}
etc.

17.01.2009 13:27

Nehmen Sie kiste in Ihre Freundesliste auf

JanS
Grünschnabel

Dabei seit: 17.01.2009
Beiträge: 6

wir haben das im Tutorium so aufgeschrieben:

{Nachbed.[Zuweisung]}Anweisung{Nachbed.}
-----------------------------------------------
{Vorbed.}Anweisung{Nachbed.}

Aber das bekomm ich bei der Aufgabe ja nicht in diese Form
bzw hae ich dann drei mal das selbe dastehn..
Und wie schreibe ich die Variable auf die ja erst in einer Zuweisung entsteht?

17.01.2009 14:54

kiste
Mitglied

Dabei seit: 06.05.2007
Beiträge: 29

Es ist ja egal welchen Wert x davor hatte. Du kannst auch x=a für ein bestimmtes a bzw. x=undef. annehmen.

17.01.2009 15:10

JanS
Grünschnabel

Dabei seit: 17.01.2009
Beiträge: 6

1.
{true[x<--5]}x=5{x=5}
---------------------------------
{x=5}x=5{true}

Ist eine notation sinnvoll in der 4 mal das selbe steht? :P

Was ist denn jetzt die nächste nachbedingung??
Abgesehn davon das man auch die Konsequenzregel anwenden könnte.. aber wir solln das mit zwischenschritten machen..

komm da echt nicht weiter.. obwohl es so kompliziert nicht aussieht...

mfg
Jan

18.01.2009 11:50

JanS
Grünschnabel

Dabei seit: 17.01.2009
Beiträge: 6

1
{true[x<--5]}x=5{x=5}
---------------------------------
{x=5}x=5{true}

2
{x=5[res<--x*x-6]}res=x*x-6{res=19}
------------------------------------------------------
{res=5*5-6}res=x*x-6{res=19

3
{res=4[res<--res mod 5]}res=res mod 5{res=4}
-------------------------------------------------------------------
{res mod 5=4}res mod 5{res =4}

ist das der sinn und zweck des hoare kalküls?

18.01.2009 14:15

JanS
Grünschnabel

Dabei seit: 17.01.2009
Beiträge: 6

Hm
Kann mir dss evtl nochmal wer erklären.. ich hab schon alles im internet über hoare gelesen.. aber ich verstehs nich...

18.01.2009 16:06

Baumstruktur | Brettstruktur

Informatiker Board » Themengebiete » Theoretische Informatik » Hoare Kalkül