Programmkorrektheitsbeweis: Ein konkretes Beispiel

Aufgabenstellung Es soll ein Programm erstellt werden, das aus einem String mit Zahlen und Vorzeichen eine Real-Zahl macht.Gegebenheiten:
Ein String der +, - und Ziffern enthält. Programmiersprache PASCAL
Struktureller Ablauf

Aufgabenstellung	Es soll ein Programm erstellt werden, das aus einem String mit Zahlen und Vorzeichen eine Real-Zahl macht.Gegebenheiten: Ein String der +, - und Ziffern enthält. Programmiersprache PASCAL

Der Sourcecode	Program StrToReal; Uses Crt; Var Fehler : Boolean; Ende : Boolean; Negativ : Boolean; i : Integer; Str : String; RealZ : Real; Begin ReadLn(Str); RealZ := 0; Fehler := False; Ende := False; Negativ := False; i := 1; while Ende = False do begin If Str[i] In ['0'..'9'] then RealZ := (RealZ * 10) + (Ord(Str[I]) - Ord('0')) else begin if (Str[i] In ['+', '-']) And (i = 1) then begin If Str[i] = '-' then Negativ := True; end else begin Fehler := True; Ende := True; end; end; If i = Ord(Str[0]) then Ende := True; If I < Ord(Str[0]) then i := i + 1; end; If Fehler = False then begin If Negativ = True then RealZ := RealZ *(-1); Writeln(RealZ); ReadLn; end else begin WriteLn('Bitte String ueberpruefen!'); ReadLn; end; end.

Der Sourcecode


	Program StrToReal; 

Uses Crt; 

Var 	
 Fehler         : Boolean; 
 Ende           : Boolean;
 Negativ	: Boolean; 
 i		: Integer; 
 Str 		: String; 
 RealZ		: Real; 

Begin 
  ReadLn(Str);
  RealZ := 0; 
  Fehler := False; 
  Ende := False; 
  Negativ := False; 
  i := 1; 

  while Ende = False do begin 
    If Str[i] In ['0'..'9'] then 
      RealZ := (RealZ * 10) + (Ord(Str[I]) - Ord('0')) 
    else begin
      if (Str[i] In ['+', '-']) And (i = 1) then begin 
        If Str[i] = '-' then 
          Negativ := True; 
      end 
      else begin 
        Fehler := True; 
        Ende := True; 
      end; 
    end;
    If i = Ord(Str[0]) then 
      Ende := True; 
    If I < Ord(Str[0]) then 
      i := i + 1; 
  end; 

  If Fehler = False then begin 
    If Negativ = True then 
      RealZ := RealZ *(-1); 
    Writeln(RealZ); 
    ReadLn; 
  end 
  else begin 
    WriteLn('Bitte String ueberpruefen!'); 
    ReadLn; 
  end; 
end.

	Es besteht auch die Möglichkeit die Anweisungen in Symbole zu schreiben, was jedoch zu einer unnötigen Komplexität und erschwerter Umsetzung führt.