PawelG: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
 
(Nie pokazano 12 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?
  
−
<math>
+
 
−
  \begin{tabbing}
+
  '''program''' PawelG;   (* autor Paweł Gburzyński, 1983, <ref>Loglan Summer School, 1983, Instytut Informatyki, Uniwersytet Warszawski</ref>  *)  
−
123\=456\=789\=012\=345\=678\=901\=\kill  
+
   '''var''' A: '''arrayof''' integer;  
−
\textbf{program} PawelG;\ \ (* autor Paweł Gburzyński, 1983, \cite{Zabo83}\ \ *)   \+ \\
+
   '''var''' n, k,  j, licz: integer ;   
−
   var A: arrayof integer; \\
+
   '''unit''' DrukujA: '''procedure''';
−
%  const l=1, u=8;  (* \textit{te liczby mozesz zmienic} *)\\
+
       '''var''' j: integer  
−
   var n, k,  j, licz: integer ; \smallskip \\  
+
   '''begin'''
−
   unit DrukujA: \textbf{procedure}; \+ \\
+
       '''for''' j := 1 '''to''' n '''do''' write(A[j]) '''od''';  
−
       var j: integer\- \\
+
       writeln
−
   \textbf{begin} \+ \\
+
   '''end''' DrukujA;   
−
       \textbf{for} j:=1 \textbf{to} n \textbf{do} write( A(j)) \textbf{od}; \\
+
   '''-----''' 
−
       writeln \- \\
+
   '''unit''' F: '''procedure''';
−
   \textbf{end} DrukujA;  \bigskip \\
+
       '''var''' i: integer;
−
   \\ 
+
   '''begin'''
−
   \textbf{unit} F: \textbf{procedure};\+ \\
+
       '''if''' k=n+1 '''then''' 
−
       var i: integer; \- \\
+
           '''call''' DrukujA; licz := licz+1
−
   \textbf{begin} \+ \\
+
       '''else''' 
−
       \textbf{if} k=n+1 \textbf{then} \+ \\
+
         '''for''' i:= 1 '''to''' n
−
           \textbf{call} DrukujA; \ licz := licz+1 \- \\
+
         '''do''' 
−
       \textbf{else} \+ \\
+
           '''if''' A[i]=0 '''then''' 
−
         \textbf{for} i:= 1 \textbf{to} n \\
+
               A[i] := k; k := k+1;
−
         \textbf{do} \+ \\
+
               '''call''' F;            
−
           \textbf{if} A[i]=0 \textbf{then} \+ \\
+
               k := k-1; A[i]:=0
−
               A[i] := k; k := k+1; \\
+
           '''fi''';
−
               \textbf{call} F; \\           
+
         '''od''';
−
               k := k-1; A[i]:=0 \- \\
+
       '''fi''';
−
           \textbf{fi}; \- \\
+
        '''return'''
−
         \textbf{od}; \- \\
+
   '''end''' F;
−
       \textbf{fi};\ \  \textbf{return}\- \\
+
'''begin''' 
−
   \textbf{end} F; \- \medskip \\
+
  readln(n);
−
\textbf{begin} \+ \\
+
   '''array''' A '''dim'''(1:n);
−
readln(n); \\
+
   '''for''' j := 1 '''to''' n '''do''' A[j] := 0 '''od''';
−
   array A dim(1:n); \quad    \\
+
   k :=1;
−
%  l:=lower(A); u:=upper(A); (* Tu l=1 oraz u=n *)\\
+
  licz:=0;
−
   \textbf{for} j := 1 \textbf{to} n \textbf{do} A[j] := 0 \textbf{od}; \\
+
   '''call''' F;
−
   k :=1;\ \ licz:=0; \\
+
   writeln(``Bywaj``)
−
   \textbf{call} F; \\
+
'''end''' PawelG
−
   writeln(''Bywaj``) \- \\
+
 
−
\textbf{end} PawelG \\ 
+
<references/>
−
\end{tabbing} 
+
−
</math>
+

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
Źródło „http://lem12.uksw.edu.pl/index.php?title=PawelG&oldid=2732”