# Begriffserklärung



## PrimeK. (10. Dez 2018)

Hallo zusammen,
kann mir einer von euch erklären was wp-Axiome sind?
MfG
PrimeK.


----------



## mihe7 (10. Dez 2018)

Wofür steht wp?!?


----------



## Xyz1 (10. Dez 2018)

mihe7 hat gesagt.:


> steht wp?


Zustandssemantik: https://books.google.de/books?id=ui...m&hl=de&pg=PA233#v=onepage&q=wp-Axiom&f=false

Ich glaube damit sei "Wissensbasis" gemeint ja.


----------



## mihe7 (10. Dez 2018)

Habs gefunden: https://de.wikipedia.org/wiki/Wp-Kalkül


----------



## Xyz1 (10. Dez 2018)

wp beschreibt eine/die schwächste Vorbedingung einer Invariante --- wenn ich mich nicht ganz täusche kann Wahr immer als Vorbedingung richtig genommen werden...

Anhand von Beispielen wäre das gut zu erklären....

@PrimeK. 
Bzgl Deiner Nachricht von gestern ich schaue später an....


----------



## Xyz1 (10. Dez 2018)

DerWissende hat gesagt.:


> kann Wahr immer als Vorbedingung


Uuppps.... Ich bin mit dem *Hoare-Kalkül* auf dem falschen Dampfer gewesen.


----------



## stg (10. Dez 2018)

Da hast du dich wohl verkalküliert.


----------



## Xyz1 (10. Dez 2018)

stg hat gesagt.:


> Da hast du dich wohl verkalküliert


Ne, eher vorwärts gerechnet.


----------



## PrimeK. (11. Dez 2018)

Erstmal Dankeschön für die Antworten.


DerWissende hat gesagt.:


> Anhand von Beispielen wäre das gut zu erklären....




```
public static int addFifty ( int v ) { 
int res = v + 50; 
return res ; 
}
```
Was wäre hier die Schwächste Vorbedingung und wie kommt man drauf?


----------



## Xyz1 (11. Dez 2018)

PrimeK. hat gesagt.:


> wie kommt man drauf


Nicht nach dem Hoare-Kalklül => rückwärtsrechnen.... oder sollte ich besser rückwärtskalkülieren sagen?


----------



## PrimeK. (11. Dez 2018)

Können Sie vielleicht in einem Beispiel zeigen , bitte.


----------



## Xyz1 (11. Dez 2018)

Neeee, @mihe7 soll das tun.  (Ich muss jetzt weg)


----------



## mihe7 (11. Dez 2018)

PrimeK. hat gesagt.:


> Was wäre hier die Schwächste Vorbedingung und wie kommt man drauf?


Du brauchst eine Nachbedingung. In Deinem Fall müsste man erstmal eine konstruieren, sagen wir mal, dass das Ergebnis <= Integer.MAX_VALUE sein muss.

Jetzt gehst Du rückwärts: res = v+50 <= Integer.MAX_VALUE und damit v <= Integer.MAX_VALUE - 50.


----------



## PrimeK. (11. Dez 2018)

@mihe7 kannst du mir kurz per PN schreiben bitte? (Also wenn es für dich ok ist, natürlich)
Ich will dir kurz die Formel zeigen, die  ich meine.
Ich darf Sie leider nicht posten.


----------



## mihe7 (11. Dez 2018)

PrimeK. hat gesagt.:


> kannst du mir kurz per PN schreiben bitte


Ich weiß gar nicht, wie das hier geht :-o


----------



## PrimeK. (11. Dez 2018)

Hä, echt jetzt?
Links click auf mein name-> Links click auf "Unterhaltung beginnen".


----------



## mihe7 (11. Dez 2018)

Unterhaltung... ah ja.


----------



## Xyz1 (11. Dez 2018)

Ich will auch mit in die Unterhaltung


----------



## PrimeK. (11. Dez 2018)

Ich kann Sie leider nicht einladen, weil die Unterhaltung von @mihe7 begonnen wurde.


----------



## mihe7 (11. Dez 2018)

@DerWissende sorry, war so konzentriert -> jetzt sollte es funktionieren.


----------

