Blatt 3 Aufgabe 1 Lösungshinweis

Zur besseren Übersicht definieren wir folgende Zusicherung:
S(i) := F(s) <= F(t), 1 <= s < i < t <= max und F(1..i) ist sortiert
Damit ergibt sich:
type Feldtyp is array (1..Max) of Elementtyp;

procedure SORT2 (F: in out Feldtyp) is
   I, J : Integer := 1;
   T: Elementtyp;
begin
    {i = 1}
    {S(i)}
   while I < Max loop
       {i < max und S(i)}
      J := I+1;
       {j = i+1 und S(i)}
       {F(i) <= F(k), i < k < j und S(i)}
      while J <= Max loop
          {j <= max und F(i) <= F(k), i < k < j und S(i)}
         if F(I) > F(J) then
             {F(i) <= F(k), i < k < j und F(i) > F(j) und S(i)}
            T := F(I); F(I) := F(J); F(J) := T;
             {F(j) <= F(k), i < k < j und F(i) < F(j) und S(i)}
             {F(i) < F(k), i < k < j und F(i) < F(j) und S(i)}
         else null;
             {F(i) <= F(k), i < k < j und F(i) <= F(j) und S(i)}
         end if;
          {F(i) <= F(k), i < k < j+1 und S(i)}
         J := J+1;
          {F(i) <= F(k), i < k < j und S(i)}
      end loop;
       {F(i) <= F(k), i < k < j und j > max und S(i)}
       {F(i) <= F(k), i < k <= max und S(i)}         [insb. auch F(i) <= F(i+1)]
       {S(i+1)}
      I := I+1;
       {S(i)}
   end loop;
    {i >= max und S(i)}
    {S(max)}
    {F(1..max) ist sortiert}
end SORT2;

Stefan Lewandowski
Last modified: Tue May 27 14:53:18 CEST 2003