Hoare Kalkül

[Petzi]

ich hab da ein Bsp da check ich mich net ganz durch

es ist folgendes Bsp gegeben:
P{begin while z>6 do begin z<-z-7;y<-y+5 end;x<-1 end}Q

<- heißt "wird ersetzt duch"

wie geh ich da jetzt vor? wende ich da zuerst die Regel T2 an?
hab k.A. :confused:


MfG Petzi

[patricasso]

Das müsste das Beispiel vom 14.März 2002 sein.

Ich habs so aufgelöst:
I.
P Teilmenge INV [z+y z] [y-z y]
H1----------------------------- ..............................................II.
P{y <- y-z} INV [z+y z] .................................(.INV und B) Teilmenge INV [1 y]
T2-------------------------------------------- ....H1---------------------------
P{begin y <- y-z; z <- z+y end}INV ...................(INV und B) {y <- 1} INV
T3--------------------------------------------------------------------------------
P {begin y <- y-z; while B do y <- 1 end; z <- z+y end} Q

III: ((INV und nonB) Teilmenge Q)

INV ist gegeben mit: y<2 und z=x

Meine Beweise für die einzelnen Ausdrücke dürften falsch sein. Komm nur zu richtigen Behauptungen wenn ich x und y gleich 1 setze und das kommt mir irgendwie komisch vor. Hat hier wer vielleicht die Beweise schon gerechnet?

/edit: die Punktlinien dienen nur zur besseren Lesbarkeit

[Petzi]

@Patricasso

nope, das ist das Beispiel vom 15.Oktober 2001

[outsida]

also ich würd das so auflösen..hoffe das stimmt


(INV^B) › INV[-y+5/y][-z-7/z]
------------------------------------------------
(INV^B){z<-z-7} INV[-y+5/y]
-------------------------------------------------
(P › INV) (INV^B){begin z<-z-7;y<-y+5 end}INV ((INV^NOT B) ›Q)
----------------------------------------------------------------------
P{while z>6 do begin z<-z-7;y<-y+5 end;} Q[-1/x]
-----------------------------------------------------------------------------
P{begin while z>6 do begin z<-z-7;y<-y+5 end;x<-1 end}Q


und dann halt die Beweise für:
(1) (P › INV)
(2) (INV^B) › INV[-y+5/y][-z-7/z]
(3) ((INV^NOT B) ›Q)
die dürften ja dann kein Problem mehr sein