Blatt 1 Aufgabe 6 Lösungshinweis

type Feldtyp is array (1..Max) of Elementtyp;

procedure SORT (F: in out Feldtyp) is
   Weiter: Boolean := True;
   T: Elementtyp;
begin
    {weiter=true}
    {weiter=false => F(1..max) ist sortiert}
   while Weiter loop
       {weiter=false => F(1..max) ist sortiert}
       {true}
      Weiter := False;
      I := 1;
       {weiter=false and i=1}
       {weiter=false => F(1..i) ist sortiert}
      while I < Max loop
          {weiter=false => F(1..i) ist sortiert}
         if F(I) > F(I+1) then
             {weiter=false => F(1..i) ist sortiert}
            Weiter := True;
            T := F(I); F(I) := F(I+1); F(I+1) := T;                  [**]
             {weiter=true and weiter=false => F(1..i) ist sortiert}
             {weiter=false => F(1..i+1) ist sortiert}
         else null;
          {F(i)<=F(i+1) and weiter=false => F(1..i) ist sortiert}
         end if;
          {weiter=false => F(1..i+1) ist sortiert}
         I := I+1;
          {weiter=false => F(1..i) ist sortiert}
      end loop;
       {i>=max and weiter=false => F(1..i) ist sortiert}
       {weiter=false => F(1..max) ist sortiert}
   end loop;
    {weiter=false and weiter=false => F(1..max) ist sortiert}
    {F(1..max) ist sortiert}
end SORT;

Und so sieht das in der Voraberklärungsversion von Lew für Dr. Schmid aus ... :-)

Übungsaufgabe: der Korrektheitsbeweis bleibt gültig, wenn man die Zeile [**] ersatzlos streicht, der Algorithmus also de facto nichts tut. Wie ist das zu erklären?