Opensource.Platon.SK CVS: doc/ztp-zbierka/04-semantika-programov.tex - diff

   Up to  [Platon] / doc / ztp-zbierka
Diff for doc/ztp-zbierka/04-semantika-programov.tex between version 1.6 and 1.7


version 1.6, 2007/07/12 04:29:45
version 1.7, 2007/07/14 06:56:14



Line 10 




Line 10 




 % 26/02/2003 - created
 % 26/02/2003 - created


 %
 %


 
 


 % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.5 2007-07-11 00:44:51 nepto Exp $
 % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.6 2007-07-12 04:29:45 nepto Exp $


 
 


 \chapter{Sémantika programov}
 \chapter{Sémantika programov}


 
 




Line 401  $$




Line 401  $$




 \tau^1  & \equiv        & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}\\
 \tau^1  & \equiv        & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}\\


 \tau^2  & \equiv        & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ ([\cmd{if}~ x = 1 ~\cmd{then}~ 0
 \tau^2  & \equiv        & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ ([\cmd{if}~ x = 1 ~\cmd{then}~ 0


 ~\cmd{else} \perp \cmd{fi}] = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp) ~\cmd{fi}\\
 ~\cmd{else} \perp \cmd{fi}] = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp) ~\cmd{fi}\\


 \tau^3  & \equiv        & x = 0 ~?~ 0 ~:~ ([x = 1 ~?~ 0 ~:~ (x = 2 ~?~ 0 ~:~ \perp)] = 0 ~?~ 0 ~:~ ([[x = 1 ~?~ 0 ~:~ (x = 2
 \tau^3  & \equiv        &


 ~?~ 0 ~:~ \perp)] = 1 ~?~ 0 ~:~ \perp] = 0 ~?~ 0 ~:~ \perp))
                 \cmd{if}~ x = 0\\


 
 & &             \cmd{then}~ 0\\


 
 & &             \cmd{else}


 
                 \begin{array}[t]{l}


 
                         \cmd{if}~ [\cmd{if}~ x = 1 ~\cmd{then}~ 0 ~\cmd{else}~ (\cmd{if}~ x = 2 ~\cmd{then}~ 0


 
                                 ~\cmd{else} \perp \cmd{fi})~\cmd{fi}] = 0\\


 
                         \cmd{then}~ 0\\


 
                         \cmd{else}


 
                         \begin{array}[t]{l}


 
                                 \cmd{if}~


 
                                         \begin{array}[t]{|l|}


 
                                                 \cmd{if}~


 
                                                         \begin{array}[t]{|l|}


 
                                                                 \cmd{if}~ x = 1\\


 
                                                                 \cmd{then}~ 0\\


 
                                                                 \cmd{else}~ (\cmd{if}~ x = 2 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\


 
                                                                 \cmd{fi}


 
                                                         \end{array} = 1\\


 
                                                 \cmd{then}~ 0\\


 
                                                 \cmd{else} \perp\\


 
                                                 \cmd{fi}


 
                                         \end{array}  = 0\\


 
                                 \cmd{then}~ 0\\


 
                                 \cmd{else} \perp\\


 
                                 \cmd{fi}


 
                         \end{array}\\


 
                         \cmd{fi}


 
                 \end{array}\\


 
 & &             \cmd{fi}


 \end{array}
 \end{array}


 $$
 $$


 
 


 Upravme to:
 Dosaďme do $\tau^3$ hodnotu $1$:


 
 


 $$
 $$


 \begin{array}{lcl}
 \begin{array}{lcl}


         \tau^3\{x = 1\} & \equiv & x = 0 ~?~ 0 ~:~ (0 = 0 ~?~ 0 ~:~ ((\perp = 1 ~?~ 0 ~:~ \perp) = 0 ~?~ 0 ~:~ \perp)) \equiv\\
 \tau^3\{x = 1\} &


                                         & \equiv & x = 0 ~?~ 0 ~:~ 0\\
         \equiv &


         \tau^3\{x = 2\} & \equiv & x = 0 ~?~ 0 ~:~ (0 = 0 ~?~ 0 ~:~ ((0 = 1 ~?~ 0 ~:~ \perp) = 0 ~?~ 0 ~:~ \perp)) \equiv\\
                 \cmd{if}~ x = 0\\


                                         & \equiv & x = 0 ~?~ 0 ~:~ 0\\
 & &             \cmd{then}~ 0\\


         \tau^4                  & \equiv & x = 0 ~?~ 0 ~:~ ([x = 1 ~?~ 0 ~:~ 0] = 0 ~?~ 0 ~:~ 0) \equiv\\
 & &             \cmd{else}


                                         & \equiv & x = 0 ~?~ 0 ~:~ 0
                         \begin{array}[t]{l}


 
                                 \cmd{if}~ 0 = 0\\


 
                                 \cmd{then}~ 0\\


 
                                 \cmd{else}~(\cmd{if}~ [\cmd{if} \perp = 1 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}]


 
                                         = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\


 
                                 \cmd{fi}


 
                         \end{array}\\


 
 & &             \cmd{fi}\\


 
 \tau^3\{x = 1\} &


 
         \equiv &


 
                 \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}


 \end{array}
 \end{array}


 $$
 $$


 
 


 Zdá sa, že to už je pevný bod. Overme to:
 Dosaďme do $\tau^3$ tiež hodnotu $2$:


 
 $$


 
 \begin{array}{lcl}


 
 \tau^3\{x = 2\} &


 
         \equiv &


 
                 \cmd{if}~ x = 0\\


 
 & &             \cmd{then}~ 0\\


 
 & &             \cmd{else}


 
                         \begin{array}[t]{l}


 
                                 \cmd{if}~ 0 = 0\\


 
                                 \cmd{then}~ 0\\


 
                                 \cmd{else}~(\cmd{if}~ [\cmd{if}~ 0 = 1 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}]


 
                                         = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\


 
                                 \cmd{fi}


 
                         \end{array}\\


 
 & &             \cmd{fi}\\


 
 \tau^3\{x = 2\} &


 
         \equiv &


 
                 \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}


 
 \end{array}


 
 $$


 
 


 
 Skúsme teraz $\tau^4$:


 $$
 $$


 \begin{array}{rcl}
 \begin{array}{lcl}


 f_P     & \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ ([\cmd{if}~ x = 1 ~\cmd{then}~ 0 ~\cmd{else}~ 0
 \tau^4  &       \equiv  &


 ~\cmd{fi}] = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}) ~\cmd{fi} \equiv\\
         \cmd{if}~ x = 0\\


 & \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}
 & &     \cmd{then}~ 0\\


 
 & &     \cmd{else}~(\cmd{if}~[\cmd{if}~ x = 1 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}] = 0


 
                 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi})\\


 
 & &     \cmd{fi}\\


 
 \tau^4  &       \equiv  &


 
         \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}


 \end{array}
 \end{array}


 $$
 $$


 
 


 Takže naozaj je to pevný bod. Zapíšme ho ešte raz, ale teraz už bez použitia notácie programovacieho
 %Zdá sa, že to už je pevný bod. Overme to:


 jazyka~C:
 %


 
 %$$


 
 %\begin{array}{rcl}


 
 %f_P    & \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ (\cmd{if}~ [\cmd{if}~ x = 1 ~\cmd{then}~ 0 ~\cmd{else}~ 0


 
 %~\cmd{fi}] = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}) ~\cmd{fi} \equiv\\


 
 %& \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}


 
 %\end{array}


 
 %$$


 
 


 
 A to už je pevný bod $f_P$:


 
 


 $$
 $$


 \begin{array}{rcl}
 \begin{array}{rcl}









Legend:


Removed from v.1.6
 


changed lines


 
Added in v.1.7


















Platon Group <platon@platon.org> http://platon.org/
  Up to  [Platon] / doc / ztp-zbierka
-version 1.6, 2007/07/12 04:29:45
+version 1.7, 2007/07/14 06:56:14
 Line 10
 Line 10
 Line 10
  % 26/02/2003 - created
  %
- % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.5 2007-07-11 00:44:51 nepto Exp $
+ % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.6 2007-07-12 04:29:45 nepto Exp $
  \chapter{Sémantika programov}
 Line 401  $$
 Line 401  $$
 Line 401  $$
  \tau^1  & \equiv        & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}\\
  \tau^2  & \equiv        & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ ([\cmd{if}~ x = 1 ~\cmd{then}~ 0
  ~\cmd{else} \perp \cmd{fi}] = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp) ~\cmd{fi}\\
- \tau^3  & \equiv        & x = 0 ~?~ 0 ~:~ ([x = 1 ~?~ 0 ~:~ (x = 2 ~?~ 0 ~:~ \perp)] = 0 ~?~ 0 ~:~ ([[x = 1 ~?~ 0 ~:~ (x = 2
+ \tau^3  & \equiv        &
- ~?~ 0 ~:~ \perp)] = 1 ~?~ 0 ~:~ \perp] = 0 ~?~ 0 ~:~ \perp))
+                 \cmd{if}~ x = 0\\
+ & &             \cmd{then}~ 0\\
+ & &             \cmd{else}
+                 \begin{array}[t]{l}
+                         \cmd{if}~ [\cmd{if}~ x = 1 ~\cmd{then}~ 0 ~\cmd{else}~ (\cmd{if}~ x = 2 ~\cmd{then}~ 0
+                                 ~\cmd{else} \perp \cmd{fi})~\cmd{fi}] = 0\\
+                         \cmd{then}~ 0\\
+                         \cmd{else}
+                         \begin{array}[t]{l}
+                                 \cmd{if}~
+                                         \begin{array}[t]{|l|}
+                                                 \cmd{if}~
+                                                         \begin{array}[t]{|l|}
+                                                                 \cmd{if}~ x = 1\\
+                                                                 \cmd{then}~ 0\\
+                                                                 \cmd{else}~ (\cmd{if}~ x = 2 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\
+                                                                 \cmd{fi}
+                                                         \end{array} = 1\\
+                                                 \cmd{then}~ 0\\
+                                                 \cmd{else} \perp\\
+                                                 \cmd{fi}
+                                         \end{array}  = 0\\
+                                 \cmd{then}~ 0\\
+                                 \cmd{else} \perp\\
+                                 \cmd{fi}
+                         \end{array}\\
+                         \cmd{fi}
+                 \end{array}\\
+ & &             \cmd{fi}
  \end{array}
  $$
- Upravme to:
+ Dosaďme do $\tau^3$ hodnotu $1$:
  $$
  \begin{array}{lcl}
-         \tau^3\{x = 1\} & \equiv & x = 0 ~?~ 0 ~:~ (0 = 0 ~?~ 0 ~:~ ((\perp = 1 ~?~ 0 ~:~ \perp) = 0 ~?~ 0 ~:~ \perp)) \equiv\\
+ \tau^3\{x = 1\} &
-                                         & \equiv & x = 0 ~?~ 0 ~:~ 0\\
+         \equiv &
-         \tau^3\{x = 2\} & \equiv & x = 0 ~?~ 0 ~:~ (0 = 0 ~?~ 0 ~:~ ((0 = 1 ~?~ 0 ~:~ \perp) = 0 ~?~ 0 ~:~ \perp)) \equiv\\
+                 \cmd{if}~ x = 0\\
-                                         & \equiv & x = 0 ~?~ 0 ~:~ 0\\
+ & &             \cmd{then}~ 0\\
-         \tau^4                  & \equiv & x = 0 ~?~ 0 ~:~ ([x = 1 ~?~ 0 ~:~ 0] = 0 ~?~ 0 ~:~ 0) \equiv\\
+ & &             \cmd{else}
-                                         & \equiv & x = 0 ~?~ 0 ~:~ 0
+                         \begin{array}[t]{l}
+                                 \cmd{if}~ 0 = 0\\
+                                 \cmd{then}~ 0\\
+                                 \cmd{else}~(\cmd{if}~ [\cmd{if} \perp = 1 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}]
+                                         = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\
+                                 \cmd{fi}
+                         \end{array}\\
+ & &             \cmd{fi}\\
+ \tau^3\{x = 1\} &
+         \equiv &
+                 \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}
  \end{array}
  $$
- Zdá sa, že to už je pevný bod. Overme to:
+ Dosaďme do $\tau^3$ tiež hodnotu $2$:
+ $$
+ \begin{array}{lcl}
+ \tau^3\{x = 2\} &
+         \equiv &
+                 \cmd{if}~ x = 0\\
+ & &             \cmd{then}~ 0\\
+ & &             \cmd{else}
+                         \begin{array}[t]{l}
+                                 \cmd{if}~ 0 = 0\\
+                                 \cmd{then}~ 0\\
+                                 \cmd{else}~(\cmd{if}~ [\cmd{if}~ 0 = 1 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}]
+                                         = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\
+                                 \cmd{fi}
+                         \end{array}\\
+ & &             \cmd{fi}\\
+ \tau^3\{x = 2\} &
+         \equiv &
+                 \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}
+ \end{array}
+ $$
+ Skúsme teraz $\tau^4$:
  $$
- \begin{array}{rcl}
+ \begin{array}{lcl}
- f_P     & \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ ([\cmd{if}~ x = 1 ~\cmd{then}~ 0 ~\cmd{else}~ 0
+ \tau^4  &       \equiv  &
- ~\cmd{fi}] = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}) ~\cmd{fi} \equiv\\
+         \cmd{if}~ x = 0\\
- & \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}
+ & &     \cmd{then}~ 0\\
+ & &     \cmd{else}~(\cmd{if}~[\cmd{if}~ x = 1 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}] = 0
+                 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi})\\
+ & &     \cmd{fi}\\
+ \tau^4  &       \equiv  &
+         \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}
  \end{array}
  $$
- Takže naozaj je to pevný bod. Zapíšme ho ešte raz, ale teraz už bez použitia notácie programovacieho
+ %Zdá sa, že to už je pevný bod. Overme to:
- jazyka~C:
+ %
+ %$$
+ %\begin{array}{rcl}
+ %f_P    & \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ (\cmd{if}~ [\cmd{if}~ x = 1 ~\cmd{then}~ 0 ~\cmd{else}~ 0
+ %~\cmd{fi}] = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}) ~\cmd{fi} \equiv\\
+ %& \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}
+ %\end{array}
+ %$$
+ A to už je pevný bod $f_P$:
  $$
  \begin{array}{rcl}
 Legend:


Removed from v.1.6
 


changed lines


 
Added in v.1.7
 Legend:


Removed from v.1.6
 


changed lines


 
Added in v.1.7
-Removed from v.1.6
+Added in v.1.7


Copyright © 2002-2006 Platon Group Site powered by Metafox CMS	Go to Top