PawelG

Poniżej znajdziesz niewielki program.

1. Czy potrafisz odgadnąc co ten program robi i sformułować odpowiednie twierdzenie?
2. Czy potrafisz je udowodnić?
3. Czy potrafisz podać dowód w którym posługujesz sie wyłącznie aksjomatami rachunku programów (alias AL), aksjomatami liczb naturalnych i regułami wnioskowania rachunku programów. Tak by czytelnik Twojego dowodu mógł zweryfikowac kazdy krok Twego rozumowania?

program PawelG;   (*  autor Paweł Gburzyński, 1983,   *)    
  var A: arrayof integer; 
  var n, k,   j, licz: integer ;  
  unit DrukujA:  procedure;  
     var j: integer 
  begin 
     for j := 1 to n do write(A[j]) od; 
     writeln  
  end DrukujA;  
  -----   
  unit F: procedure;
     var i: integer;  
  begin 
     if k=n+1 then  
          call DrukujA;  licz := licz+1  
     else  
        for i:= 1 to n  
        do  
          if A[i]=0 then  
             A[i] := k; k := k+1;  
             call F;             
             k := k-1; A[i]:=0  
          fi;  
        od;  
     fi;
        return
  end F;  
begin  
  readln(n);  
  array A dim(1:n);  
  for j := 1 to n do A[j] := 0 od;  
  k :=1;
  licz:=0;  
  call F;  
  writeln(``Bywaj``)  
end PawelG