Kettos specifikacio.
	Adott d_a=(A,F,E_a);  d_c=(C, G, E_);
		A_0={a|I_a(a)}; C_0={c|I_c(c)};
abrazolas: \fi : C_0 -> A_0;

-=-

E_a={..., f_s(f_c(a))=h(a),....,I_a(f_c(a))="false" => f_c(a)="undefined"};

E'_a= {...., {y=f_c(a)} z=f_s(y) {z=h(a)}, ..., {I_a(f_c(a))} z=f_c(a) {I_a(z) \and z=f_c(a)}};

-=-

E'_a= {..., {y=f_c(a)\and I_a(a)} z=f_s(y) {z=h(a)\and I_a(a)},...,
{I_a(f_c(a))\and I_a(a)} z=f_c(a) {I_a(z)\and z=f_c(a) \and I_a(a)}};
azaz
	E'_a={..., {pre_f_i(a)} a'=f_i(a) {post_f_i(a,a')}, ...};

-=-
	a=\fi(c);
-=-

E_c = {..., g_s(g_c(c))=h_c(c),...,I_c(g_c(c)) = "false" => g_c(c) = "undefined"};
E_c = {..., pre_g_i(c)} c'=g_i(c) {post_g_i(c,c')},...};
E_c = {..., Q_g_i, ...};

-=-

Ha bebizonyitjuk, hogy
1) I_c(c) => I_a(\fi(c));
2) post_g_0(c) => I_c(c);
3) post_g_0(c) => post_f_0(\fi(c));
4) I_c(c) \amd pre_f_i(\fi(c)) => pre_g_i(c);
5) I_c(c) \and pre_f_i(\fi(c)) \and post_g_i(c,c') \and I_c(c') => post_f_i(\fi(c), \fi(c'));
akkor a d_c konkret specifikacio a d_a absztrakt specifikacio szerint helyes.

-=-

Ha a kovetkezo tetelek teljesulnek:
1. (\forall c \in C) (I_c(c) => I_a(\fi(c));
2. {"true"} Q_0 {post_f_0(\fi(c)) \and I_c(c)};
3. (\forall f_i\in F): {pre_f_i(\fi(c)) \and I_c(c)} Q_i {post_f_i(\fi(c), \fi(c')) \amd I_c(c')};
ahol 2. es 3. teljes helyessegi tetelek, akkor a d_c konkret specifikacio a d_a absztrakt
specifikacio szerint helyes.

-=-

Adott S determinisztikus program:
Tranzakcios diagram: (L, R, s, t);

	s: u<-f;
	({s,t},P(s, "true" -> (u <- f), t)}, s, t);

	       /-\"true" -> (u<-f)   /-\
	       |s|------------------>|t|
               \-/                   \-/
(az s-et es a t-t be kell karikazni)

-=-

S: S_1;S_2;
({s, r, t}, {(s, "true" -> (u<- f_s_1), r), (r, "true" -> (u<- f_s_2), t)}, s, t);
-=-
          "true" -> (u<-f_s_1)      "true" -> (u<-f_s_2)
	s ---------------------> r ------------------------> t

(s, r es t be van karikazva)

-=-
               S_1T		S_2T
	s     		r			t

(s, r es t be van karikazva, r S_2T t egy kozos teglalapban van, aminek alanyulik
az s S_1T teglalapja)

-=-

S: if \alpha then S_1 else S_2 fi;
({s, t}, {(s, \alpha -> (u<-f_s_1), t), (s, ~\alpha -> (u<-f_s_1), t)}, s, t);

Q-diagram: Q=(Q_s, Q_t);
                      Q_s
                /----s----\
                |         |
\alpha -> f_S_1 |         | ~\alpha -> f_S_2
                |         |
		\--->t<---/
		       Q_t

(s es t be van keretezve)

		 S_1T

	s		 t

		 S_2T

(s es te be van keretezve; s, t es S_2T egy kozos konkav bigyoval be van keretezve,
es ez ala nyulik S_1T, s es t bekeretezett konkav bigyoja)

-=-

Adott {\fi} S{\pszi} parcialis helyessegi tetel.
Adott az S program ST = (L, T, s, t) tranzakcios diagramja, es Q diagramja,
amelyrol bebozonyitottuk, hogy induktiv.
Ha bebizonyitjuk, hogy a Q-diagram a (\fi, \pszi) specifikacio szerint konzisztens, azaz
	\fi => Q_s; Q_t => \pszi;
akkor az S program a (\fi, \pszi) specifikacio szerint parcialisan helyes.

-=-

A program befejezodesenek (konvergens tulajdonsaganak) bizonyitasa.
	\fi - konvergencia bizonyitasa.

-=-

Alapfogalom.
Jol rendezett halmaz.
Legyen W egy halomaz es <:WxW beinaris relacio. A < relaciot rendezonek mondjuk, ha
tetszoleges a, b, c \in W -re:
 - irreflexiv: a < a ="false".
 - asszimetrikus: a<b ="true" => b<a="false".
 - tranzitiv: (a<b = "true") \and (b<c="true") => a<c="true".
A parcialisan rendezett (W, <) halmazt jol rendezettnek nevezzuk, ha nem letezik vegtelen
 ... < w_2 < w_1 < w_0, sorozat, w_i\in W, eseten.

-=-

\fi - konvergencia bizonyitasanak Floyd-fele modszere.

Allitas:
Adott a P program PT =(L, R, s, t) tranzakcios diagramja es \fi.
1) Keszitsuk el PT alapjan a kovergencia bizonyitasahoz szukseges Q-diagramot.
2) Bizonyitsuk be, hogy Q-diagram induktiv es \fi=> Q_s.
3) Valasszunk meg egy (W, <) jol rendezett halmazt es a 
   \ro=(\ro_l|l\in L}, fuggvenyhalmazt, ahol p_l:\SZIGMA -> W,
   minden l\in L eseten.
4) Bizonyitsuk be, hogy \ro_l definialva van: Q_l(\szigma) => \ro_l\in W.
5) Mutassuk ki, hogy (\forall(l, \alpha->f, l')\in R)(Q_l(\szigma)\and\alpha(\szigma)=>\ro l'(f(\szigma))<\ro l(\szigma).
Ha ezeket bebizonyitottuk, akkor a P program \fi-konvergens.

-=-

Bizonyitas:
\nu: <s, \szigma_0> -> <l_1, \szigma_1> -> ...;
Q induktivitasabol kovetkezik, hogy Q invarians. Ha \fi => Q_s, akkor
\ro_s(\szigma_0), \ro_l_1(\szigma_1), ... definialva van es minden <l, \szigma> -> <l', \szigma'>
tranzakciora	\ro_{l'}(f(\szigma))<\ro_l(\szigma).
Igy W jol-rendezettsegebol kovetkezik, hogy a vegrehajtas veges.

-=-

Vegrehajtasi (runtime) hibamentesseg.
Tekintsuk az S programnak azokat a vegrehajtasait:
\nu: <s, \szigma_0> -> <l_1, \szigma_1> -> ...;
amelyekre \fi(\szigma_0)="true".
Ha nincs olyan vegrehajtas, amelynek soran valamely cimkenel a
szoba joheto tranzakciok kozott letezik olyan, amely nincsen
definialva, akkor azt mondjuk, hogy az S program a \fi input
specifikacio mellett mentes a vegrehajtasi hibatol.

-=-

Vegrehajtasi hibamentesseg bizonyitasa:
Adott a P program PT=(L, R, s, t) tranzakcios diagramja es \fi.
Keszitsuk el annak Q-diagramjat. Ha minden l\in L eseten az osszes
(l, \alpha->f, l') tranzakcional Q_l(\szigma)\and(\alpha(\szigma)=>
pre_f(\szigma), akkor a P program mentes a vegrehajtasi hibatol.

-=-

P program tejes-helyessegenek bizonyitasa.

Adott a P program es annak (\fi, \pszi) specifikacioja.
	- Konstrualjuk meg a P programhoz a vele szemantikailag ekvivalens PT diagramot.
	- Keszitsuk el a Q diagramot.
	- Bizonyitsuk be, hogy a P program parcialisan helyes az adott specifikacio szerint.
	- Bizonyitsuk be, hogy a P program kovergens.
	- Bizonyitsuk be, hogy a P program mentes a vegrehajtasi hibatol.
Akkor a P program a (\fi, \pszi) specifikacio szerint teljesen helyes.