PawelG: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
 
(Nie pokazano 5 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 2: Linia 2:
 
# Czy potrafisz odgadnąc co ten program robi i sformułować odpowiednie twierdzenie?
 
# Czy potrafisz odgadnąc co ten program robi i sformułować odpowiednie twierdzenie?
 
# Czy potrafisz je udowodnić?
 
# Czy potrafisz je udowodnić?
 +
# 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, <ref>Loglan Summer School, 1983, Instytut Informatyki, Uniwersytet Warszawski</ref>\ \ *)     
+
  '''program''' PawelG;   (* autor Paweł Gburzyński, 1983, <ref>Loglan Summer School, 1983, Instytut Informatyki, Uniwersytet Warszawski</ref> *)     
 
   '''var''' A: '''arrayof''' integer;  
 
   '''var''' A: '''arrayof''' integer;  
 
   '''var''' n, k,  j, licz: integer ;   
 
   '''var''' n, k,  j, licz: integer ;   
 
   '''unit''' DrukujA:  '''procedure''';   
 
   '''unit''' DrukujA:  '''procedure''';   
 
       '''var''' j: integer  
 
       '''var''' j: integer  
    '''begin'''
+
  '''begin'''  
 +
      '''for''' j := 1 '''to''' n '''do''' write(A[j]) '''od''';
 
       writeln   
 
       writeln   
    '''end''' DrukujA;    
+
  '''end''' DrukujA;
    '''unit''' F: '''procedure''';
+
  '''-----''' 
 +
  '''unit''' F: '''procedure''';
 
       '''var''' i: integer;   
 
       '''var''' i: integer;   
    '''begin'''  
+
  '''begin'''  
 
       '''if''' k=n+1 '''then'''   
 
       '''if''' k=n+1 '''then'''   
 
           '''call''' DrukujA;  licz := licz+1   
 
           '''call''' DrukujA;  licz := licz+1   
Linia 28: Linia 31:
 
       '''fi''';
 
       '''fi''';
 
         '''return'''
 
         '''return'''
    '''end''' F;   
+
  '''end''' F;   
'''begin'''   
+
'''begin'''   
 
   readln(n);   
 
   readln(n);   
 
   '''array''' A '''dim'''(1:n);   
 
   '''array''' A '''dim'''(1:n);   
Linia 36: Linia 39:
 
   licz:=0;   
 
   licz:=0;   
 
   '''call''' F;   
 
   '''call''' F;   
   writeln(''Bywaj``)   
+
   writeln(``Bywaj``)   
'''end''' PawelG
+
'''end''' PawelG
  
/references
+
<references/>

Aktualna wersja na dzień 11:36, 23 mar 2020

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, [1]  *)    
  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
  1. Loglan Summer School, 1983, Instytut Informatyki, Uniwersytet Warszawski