Platon Technologies
not logged in Login Registration
EnglishSlovak
open source software development celebrating 10 years of open source development! Friday, October 16, 2026
[BACK] [TXT][DIR] Up to [Platon] / doc / ztp-zbierka

Diff for doc/ztp-zbierka/04-semantika-programov.tex between version 1.10 and 1.11

version 1.10, 2007/08/06 04:56:50 version 1.11, 2007/08/11 03:20:28
Line 10 
Line 10 
 % 26/02/2003 - created  % 26/02/2003 - created
 %  %
   
 % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.9 2007-07-30 04:55:09 nepto Exp $  % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.10 2007-08-06 04:56:50 nepto Exp $
   
 \chapter{Sémantika programov}  \chapter{Sémantika programov}
   
   \section{Základy sémantiky}
   
 \begin{example} % /* loop(b, S_1, S_2)  \begin{example} % /* loop(b, S_1, S_2)
   
 Uvažujme hypotetický iteratívny príkaz~$\cmd{loop}~(b, S_1, S_2)$  Uvažujme hypotetický iteratívny príkaz~$\cmd{loop}~(b, S_1, S_2)$
Line 399  $$
Line 401  $$
 \begin{array}{rcl}  \begin{array}{rcl}
 \tau^0  & \equiv        & \Omega\\  \tau^0  & \equiv        & \Omega\\
 \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}~[\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}) ~\cmd{fi}\\
 \tau^3  & \equiv        &  \tau^3  & \equiv        &
                 \cmd{if}~ x = 0\\                  \cmd{if}~ x = 0\\
 & &             \cmd{then}~ 0\\  & &             \cmd{then}~ 0\\
Line 412  $$
Line 414  $$
                         \cmd{else}                          \cmd{else}
                         \begin{array}[t]{l}                          \begin{array}[t]{l}
                                 \cmd{if}~                                  \cmd{if}~
                                         \begin{array}[t]{|l|}                                          \left[ \begin{array}[c]{l}
                                                 \cmd{if}~                                                  \cmd{if}~
                                                         \begin{array}[t]{|l|}                                                          \left[ \begin{array}[c]{l}
                                                                 \cmd{if}~ x = 1\\                                                                  \cmd{if}~ x = 1\\
                                                                 \cmd{then}~ 0\\                                                                  \cmd{then}~ 0\\
                                                                 \cmd{else}~ (\cmd{if}~ x = 2 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\                                                                  \cmd{else}~ (\cmd{if}~ x = 2 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\
                                                                 \cmd{fi}                                                                  \cmd{fi}
                                                         \end{array} = 1\\                                                          \end{array} \right] = 1\\
                                                 \cmd{then}~ 0\\                                                  \cmd{then}~ 0\\
                                                 \cmd{else} \perp\\                                                  \cmd{else} \perp\\
                                                 \cmd{fi}                                                  \cmd{fi}
                                         \end{array}  = 0\\                                          \end{array} \right] = 0\\
                                 \cmd{then}~ 0\\                                  \cmd{then}~ 0\\
                                 \cmd{else} \perp\\                                  \cmd{else} \perp\\
                                 \cmd{fi}                                  \cmd{fi}
Line 548  Podľa fixpointovej indukcie stačí dokáza
Line 550  Podľa fixpointovej indukcie stačí dokáza
   
 $$  $$
 \begin{array}{lcl}  \begin{array}{lcl}
         \begin{array}{lcl}          \left( \begin{array}{lcl}
         \cmd{if}~ x = 0\\          \cmd{if}~ x = 0\\
         \cmd{then}~ 0\\          \cmd{then}~ 0\\
         \cmd{else}~(\cmd{if}~[\cmd{if}~ x - 1 \ge 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}] \ge 0          \cmd{else}~(\cmd{if}~[\cmd{if}~ x - 1 \ge 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}] \ge 0
                         ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\                          ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\
         \cmd{fi}          \cmd{fi}
         \end{array}          \end{array} \right)
 & \sqsubseteq &  & \sqsubseteq &
         \begin{array}{l}          \left( \begin{array}{l}
         \cmd{if}~ x = 0\\          \cmd{if}~ x = 0\\
         \cmd{then}~ 0\\          \cmd{then}~ 0\\
         \cmd{else} \perp\\          \cmd{else} \perp\\
         \cmd{fi}          \cmd{fi}
         \end{array}          \end{array} \right)
 \end{array}  \end{array}
 $$  $$
   
Line 839  Podľa fixpointovej indukcie stačí dokáza
Line 841  Podľa fixpointovej indukcie stačí dokáza
   
 $$  $$
 \begin{array}{lcl}  \begin{array}{lcl}
         \begin{array}{lcl}          \left( \begin{array}{lcl}
         \cmd{if}~ x > 0\\          \cmd{if}~ x > 0\\
         \cmd{then}          \cmd{then}
                 \begin{array}[t]{l}                  \begin{array}[t]{l}
Line 850  $$
Line 852  $$
                 \end{array}\\                  \end{array}\\
         \cmd{else}~x\\          \cmd{else}~x\\
         \cmd{fi}          \cmd{fi}
         \end{array}          \end{array} \right)
 & \sqsubseteq &  & \sqsubseteq &
         \begin{array}{l}          \left( \begin{array}{l}
         \cmd{if}~ x > 0\\          \cmd{if}~ x > 0\\
         \cmd{then}~ 0\\          \cmd{then}~ 0\\
         \cmd{else}~ x\\          \cmd{else}~ x\\
         \cmd{fi}\\          \cmd{fi}
         ~\\          \end{array} \right)
         ~\\  
         ~  
         \end{array}  
 \end{array}  \end{array}
 $$  $$
   
Legend:
Removed from v.1.10  
changed lines
  Added in v.1.11
Platon Group <platon@platon.org> http://platon.org/
Copyright © 2002-2006 Platon Group
Site powered by Metafox CMS 		Go to Top