%
% ztp-skuska.03-05-27.tex
%
% Developed by Ondrej Jombik <nepto@php.net>
% Copyright (c) 2003 Platon SDG, http://www.platon.sk/
% Licensed under terms of GNU General Public License.
% All rights reserved.
%
% Changelog:
% 28/05/2003 - created
%

% $Platon$

\documentclass[a4paper,12pt]{article}
\usepackage [slovak]{babel}
\usepackage [latin2]{inputenc}
\usepackage {fontenc}
\usepackage {t1enc}

% use graphics and floating figures
\usepackage {graphicx}
\usepackage {floatflt}

% def
\def\hl#1{\textsc{\small{\small{#1}}}}
\def\cmd#1{{ \bf{#1} }}
\newcommand{\lb}{[\kern-0.6mm [}
\newcommand{\rb}{]\kern-0.6mm ]}
\newcommand{\M}{\mathcal{M}}
\newcommand{\W}{\mathcal{W}}
\DeclareMathSymbol{\UUsum}{\mathop}{symbols}{"74}
\newcommand{\UU}{\UUsum_{0}^{\infty}}

\hyphenation {
roz-ho-do-vať
roz-ho-do-va-ní
}

\begin{document}

\begin{center}
	{\Large \bf Základy teórie programovania}

	skúška, termín 1, 27. mája 2003
\end{center}

{\it Kurzívou sú vyznačené moje poznámky k~príkladom, ktoré však
rozhodne nemusia viesť k zaručene správnym riešeniam.

\hfill \hl{Ondrej Jombík, 30.~mája~2003}}

\begin{enumerate}
	
\item Sformulujte a dokážte tvrdenie o~(ne)rozhodnuteľnosti vlastností
	divergencie a zastavenia \underline{voľných schém} a o~príslušnosti
	štandardnej schémy k~triede voľných schém. \hl{(20b)}

{\it divergencia - rozhodnuteľný (existuje cesta do $\cmd{end}$?);
zastavenie - rozhodnuteľný (existuje v schéme cyklus?); príslušnosť -
nerozhodnuteľný}

\item Uvažujme triedu schém~$\mathcal{L}$ s rozhodnuteľným problémom
	dosiahnuteľnosti príkazu (napr. liberálne schémy).

	Dokážte alebo vyvráťte nasledujúce tvrdenie: Problém či je ľubovoľná
	schéma z~triedy~$\mathcal{L}$ priechodná je rozhodnuteľný.
	\hl{(10b)}

{\it Len na prvý pohľad je tento príklad triviálny. Úvahy:

Majme len štandardné schémy. Tam vieme priechodnosť čiastočne
rozhodovať. Hrán je konečný počet a tak si ich všetky vložíme do
množiny. Začneme prehľadávať do šírky (tak ako zastavenie na
$\mathcal{S}$) a vždy keď prejdeme hranou vyberieme ju z množiny. Až nám
ostane prázdna množina vyhlásime, že schéma je priechodná. Inak
pokračujeme do nekonečna.

Teraz skúmajme, či nám dosiahnuteľnosť príkazu nejako pomôže
pri~rozhodovaní priechodnosti. Ja hovorím, že nie. Ak by do každého
príkazu viedla iba jedna hrana, vedeli by sme, že ak je príkaz
dosiahnuteľný, určite je táto hrana prichodná. Do príkazu však môže
viesť dve alebo viac hrán a my nevieme určiť, ktorou hranou sme do
príkazu prišli (teda ktorá hrana z tých dvoch je priechodná).

Po~písomke sa však ozval jeden expert, ktorý povedal, že prípady, kde
do~príkazu vedie dve alebo viac hrán vie ošetriť takto: ak vedie
do~príkazu~$n$ hrán, ponechá len jednu a zvyšných~$n - 1$ odstráni.
Potom sa spýta na dosiahnuteľnosť príkazu a teda aj priechodnosť
ponechanej hrany. Takto to opakuje pre všetky hrany vedúce do príkazu.
Ak je príkaz vždy dosiahnuteľný, tak aj všetky doňho vedúce hrany sú
priechodné.

Ja ale hovorím, že môže existovať schéma, do ktorej príkazu vedú dve
hrany, pričom obe sú priechodné. Tou druhou sa však prejde len vtedy, ak
sa predtým prešlo prvou:

$$
\begin{array}{rl}
	\cmd{begin}		& [y] := [x]	\\
	1:				& [y] := [y]	\\
	2:				& \cmd{goto}~ 1	\\
\end{array}
$$

V~ tomto prípade sa z~riadku~$2$ na~$1$ prejde až po prejdení
z~$\cmd{begin}$ na~$1$. Lenže ak my hranu z~$\cmd{begin}$ do~$1$
odstránime, algoritmus prehlási, že hrana z~$2$ do~$1$ je nepriechodná!

Ako som vravel, zaujímavý príklad. Môj názor je, že problém je čiastočne
rozhodnuteľný, pričom dosiahnuteľnosť príkazu na to nemá žiadny vplyv.
Veľmi rád sa ale nechám poučiť ak je to inak.}

\item Uvažujme triedu štruktúrovaných schém~$W^b$, obohatenú
	o~booleovské premenné a dobre otypované priradenie do booleovských
	premenných. Ktorú z uvedených konštrukcií je (nie je) možné preložíť
	do \underline{ekvivalentnej} \underline{schémy} z~triedy~$W^b$?
	Zdôvodnite prečo. \hl{(15b)}

$$
\begin{array}{ll}
	W_1:	& \cmd{while}~ b_1 \land b_2 ~\cmd{do}~ S ~\cmd{od}		\\
	W_2:	& \cmd{while}~ b_1 \lor  b_2 ~\cmd{do}~ S ~\cmd{od}		\\
	W_3:	& \cmd{while}~ \lnot b       ~\cmd{do}~ S ~\cmd{od}		\\
\end{array}
$$

{\it Základom je nepomýliť si tento príklad s prekladaním programových
konštrukcií 
do~$\mathcal{W}$. :-)

Preložiť idú všetky. K dispozícii sú totiž aj konštanty $TRUE$ a
$FALSE$, ktoré je možné priradiť do booleovskej premennej. Ak by však aj
tieto konštanty neboli, $W_1$ a $W_2$ by stále preložiť išli len za
pomoci booleovských priradení. Navyše $W_2$ ide preložiť aj
do~$\mathcal{W}$, tzn. nie sú booleovské premenné a priradenia
potrebné.}

\item Definujte význam induktívnej formuly $\{p\} P \{q\}$ a uveďte
	axiómy a inferenčné pravidlá Hoareovského systému pre imperatívny
	programovací jazyk obsahujúci
	\begin{itemize}
		\item[--] priraďovací príkaz,
		\item[--] kompozíciu príkazov,
		\item[--] podmienkový príkaz
			($\cmd{if}~ ... ~\cmd{then}~ ... ~\cmd{else}~ ... ~\cmd{fi}$),
		\item[--] príkaz cyklu
			($\cmd{while}~ ... ~\cmd{do}~ ... ~\cmd{od}$).
	\end{itemize}

	Definujte význam induktívnej formuly $[p] P [q]$ tak, aby
	vyjadrovala \underline{totálnu správnosť programu}. \hl{(15b)}

{\it Čo dodať? Učebné texty má predsa každý\dots}

\item Určite a zdôvodnite, či sú nasledujúce dve inferenčné pravidlá
	\underline{zdravé}.~\hl{(10b)}
$$
\frac
{\{p \land b\}~ S ~\{(p \land \lnot b) \Rightarrow q\}}
{\{p\}~ \cmd{while}~ b ~\cmd{do}~ S ~\cmd{od} ~\{q\}}
$$
$$
\frac
{\{p \land b\}~ S ~\{p \land (\lnot b \Rightarrow q\}}
{\{p\}~ \cmd{while}~ b ~\cmd{do}~ S ~\cmd{od} ~\{q\}}
$$

{\it Väčšine včetne mňa vyšlo, že sú obe nezdravé. Boli však aj takí, čo
vraveli, že druhé je zdravé. Nepočul som však nič o tom, že by niekto
tvrdil, že prvé je zdravé. Počkáme si na výsledky\dots}

\item Na základe Floydovej metódy sformulujte postačujúce podmienky
	\underline{čiastočnej správnosti} schémy~$S$ vzhľadom na vstupnú
	podmineku~$p(x)$ a výstupnú podmienku~$q(x, z)$ a invarianty~$I_i(x,
	\overline{y})$ v~príslušných deliacich bodoch.

$$
\begin{array}{lrl}
S:	& \cmd{begin}	& [y_1, y_2] := [a || x ??, a]					\\
	& 1:			& [y_1] := [g(y_1, y_2)]						\\
	& 2:			& \cmd{if}~ p_1(y_1) ~\cmd{then}~ \cmd{goto}~ 5	\\
	& 3:			& [y_1, y_2] := [f_1(y_1, f_2(y_2)]				\\
	& 4:			& \cmd{goto}~ 1									\\
	& 5:			& [y_2] := [g(y_2, y_1)]						\\
	& 6:			& \cmd{if}~ p_2(y_2) ~\cmd{then}~ \cmd{goto}~ \cmd{end}	\\
	& 7:			& [y_1, y_2] := [g_1(y_1), g_2(y_2)]			\\
	& 8:			& \cmd{goto}~ 1									\\
	& \cmd{end}		& [z] := [g_1(y_1)]								\\
\end{array}
$$

{\it \begin{enumerate}
	\item Nájsť deliace body (doporučujem na riadkoch 2 a 6).
	\item Sformulovať invarianty $I_2$ a $I_6$ (ja som mal $I_2: y_1 =
		g(y_1, y_2)$ a $I_6: y_1 = g(y_1, y_2) \land y_2 = g(y_2,
		y_1)$).

	\item Odvodiť verifikačné podmienky (pre všetky cesty treba odvodiť
		$R_{AB}$ a $r_{AB}$ a potom spolu s invariantami dosadiť do
		všeobecnej rovnice).

	\item Dokázať verifikačné podmienky (v~tomto prípade bude stačiť,
		keď sa prehlási, že dokázaním týchto podmienok dokážeme aj
		čiastočnú správnosť schémy).
\end{enumerate}}

\item Vyjadrite operačnú vstupno-výstupnú sémantiku~$\mathcal{O}$ a
	denotačnú sémantiku~$\mathcal{M}$ jednoduchého imperatívneho jazyka
	so~"štandardnými" príkazmi priradenia, kompozície, vetvenia a
	s~príkazom cyklu
$$
\cmd{loop}~ S_1; ~\cmd{when}~ b ~\cmd{exit}; S_2 ~\cmd{pool}
$$
a zdôvodnite, že platí $\mathcal{M}\lb S \rb\sigma = \mathcal{O}\lb S
\rb\sigma$.~\hl{(20b)}
\newpage

{\it V skriptách je tvrdenie $\mathcal{M}\lb S \rb\sigma =
\mathcal{O}\lb S \rb\sigma$ veľmi podrobne dokázané. Až nato, že ako
cyklus sa používa klasický $\cmd{while}$ a nie uvedený jeden a pol
cyklus. Inak ale ide v podstate o to isté. Lenže na ten jeden a pol
cyklus treba brať pri dokazovaní veľký zreteľ! Dá sa rozložiť pomocou
kompozície na dve časti: $S_1$ a konštrukciu $\cmd{while}~ \lnot b
~\cmd{do}~ S_2; S_1; ~\cmd{od}$. A~to už je viac-menej klasický
$\cmd{while}$, čo sa môže hodiť.}

\item Uvažujme hypotetický iteratívny príkaz~$\cmd{loop}~(b, S_1, S_2)$
	definovaný sémantickou rovnicou

$$
\M\lb \cmd{loop}~(b, S_1, S_2) \rb ~=~ \UU\{\phi_i\}
$$

kde
$$
\begin{array}{rcc @{} c @{} l @{} l}
	\phi_0		& =	& \lambda\sigma	& ~\cdot~	& \perp	&	\\
	\phi_{i+1}	& =	& \lambda\sigma	& ~\cdot~	& \cmd{if}~ \W\lb b \rb\sigma
						& ~\cmd{then}~ \phi_i(\M\lb S_1 \rb\sigma)	\\
				&	&				&			&
						& ~\cmd{else}~ \M\lb S_2 \rb\sigma			\\
\end{array}
$$

Na základe základných príkazov (priradenie, kompozícia, vetvenie a cyklus)
definujte programový segment $S$ taký, že platí

$$
\M\lb \cmd{loop}~(b, S_1, S_2) \rb ~=~ \M\lb S \rb
$$

Tvrdenie dokážte. \hl{(10b)}

{\it Vyriešené v zbierke, hoci z dôkazu nemám veľmi dobrý pocit.}

\item Sformulujte a dokáťe vetu o~\underline{najmenšom pevnom bode}
	funkcionálu (s potrebnými predpokladmi na funkcionál a príslušné
	obory definície a hodnôt).

	Overte a zdôovodnite, či je funkcia~$f$ najmenším pevným bodom
	funkcionálu, zodpovedajúceho rekurzívnej definícii~$\phi$ nad oborom
	prirodzených čísiel.~\hl{(20b)}
$$
\begin{array}{l}
f(x, y):~ \cmd{if}~ x > 0 ~\cmd{then}~ y ~\cmd{else}~ \perp	\\
\phi(x, y) ~\Leftarrow~ \cmd{if}~ x = 0 ~\cmd{then}~ y ~\cmd{else}~
\cmd{if}~ y = 0 ~\cmd{then}~ \phi(x - 1, 1) ~\cmd{else}~ \phi(x - 1,
\phi(x, y - 1))
\end{array}
$$

{\it Ehm\dots Vraj je nato nejaký štandardný postup.}

\item Uvažujme nasledujúce výpočtové pravidlo~SPOS (sekvenčné~POS).
	Pravidlo~SPOS vyberie paralelne najvonkajšejšie výskyty (ako~POS),
	ale "prideľuje" ich na substitúciu postupne zľava-doprava.

	Určite, či je pravidlo SPOS bezpečné (v~jazyku~$L_1$), resp. či je
	korektné. Svoje tvrdenie zdôvodnite. \hl{(15b)}

{\it Čo hovorí? Uráža nás? :-)}
	
\end{enumerate}

\end{document}

% vim: ts=4
% vim600: fdl=0 fdm=marker fdc=3