[Java] Verifikation von einem kleinen Programm

Dieses Thema im Forum "Programmierung & Entwicklung" wurde erstellt von riverlove, 18. November 2007 .

  1. 18. November 2007
    Verifikation von einem kleinen Programm

    Hey.. habe mehrere aufgaben letzte woche erhalten und darunter ist eine verifikation mit dem hoale kalkül.. ich verstehe es einfach nich :/ habe das jetzt mehrere stunden angeschaut aber irgendwie steckt für mich nich wirklich sinn dahinter. behindert ist das.

    und zwar ist das programm:
    Code:
    Gegeben sei folgendes JAVA-Programm P, welches f¨ur eine Eingabe n ∈ IN =
    {0, 1, 2, . . .} die Summe Pn
    j=1 j2 berechnet:
    i = n;
    res = 0;
    while (i > 0) {
    res = res + i ∗ i;
    i = i − 1;
    }
    
    die aufgabe dazu:
    Code:
    Vervollständigen Sie die Verifikation des Algorithmus P im Hoare-Kalkül, indem
    Sie die unterstrichenen Teile ergäanzen. Hierbei dürfen zwei Zusicherungen
    nur dann direkt untereinander stehen, wenn die untere aus der oberen folgt.
    Hinter einer Programmanweisung darf nur eine Zusicherung stehen, wenn dies
    aus einer Regel des Hoare-Kalküls folgt. Kennzeichnen Sie ihre benutzte Invariante
    deutlich.
    
    Also paar notizen erstmal.. eingabe= n; ausgabe = res; Vorbedingung = n >= 0; Nachbedingung= res = Summe von j=1 bis n für j^2

    ahhh behindert. hilfeee

    hab mal angefangen:
    Code:
    [RIGHT]< n >= 0 >
    <n >= 0 und n = n>
    [/RIGHT]
    i = n;
    [RIGHT]<n >= 0 und i = n >[/RIGHT]
    
    so weiter komm ich nicht :/ verstehe das einfach nich

    kann jemand das? ich glaub wenn man da durchblickt ist das noch nich mal schwierig.. ^^
    danke bw ist selbstverständlich
     
  2. Video Script

    Videos zum Themenbereich

    * gefundene Videos auf YouTube, anhand der Überschrift.