Adott BR bizonyitasi rendszer es BR_{sec} a bizonyitasi rendszerben levezetheto formulak halmaza. - A BR bizonyitasi rendszer megbizhato, ha (\forall \fi,\fi\in BR_{sec}) => \fi = "true". - A BR bizonyitasi rendszer teljes, ha (\forall\fi,\fi\in BR \and \fi="true") => \fi \in BR_{sec}. -=- A Hoare modszer teljessegi tetele. Adva S(x,y) strukturalt program, S(x,y) tetszoleges reszprogramja: s(x,y). Felteves: {Q(x) \and y=I_S(x)} s(x,y) {Q(x) \and y=O_S(x)} = "true", ahol f_s(x, I_S(x))=O_S(x). Allitas. Minden ilyen tulajdonsagu s(x,y) resz - programra vonatkozo fenti tetel, A Hoare-modszer segitsegevel levezetheto. -=- Megjegyzes. Nyilvan: {Q(x)\and y=x} S(x,y) {Q(x)\and y=O_s(x)}="true", azaz P(x):Q(x)\and y=x; R(x,y):Q(x) \and y=O_s(x); {P(x)} S(x,y) {R(x,y)} = "true". -=- Bizonyitas. (parcialis helyesseg) Az alapstrukturak egymasba skatulyazasanak szama szerinti teljes indukcioval. -=- Alapeset. s(x,y) = y <- g(x,y) A tetel: {Q(x) \and y=I_s(x)} y <-g(x,y) {Q(x) \and y=O_s(x)} = "true", -=- Q(x) \and y=I_s(x) => Q(x) \and g(x,y)=O_s(x) ----------------------------------------------------------- {Q(x) \and y=I_s(x)} y <- g(x,y) { Q(x) \and y=O_s(x)} -=- Indukcio. Tegyuk fel, hogy "k" melysegu egymasva skatulyazas eseten a tetel igaz es bizonyitsuk "k+1"-re is. Harom eset: - a k+1. struktura egy szekvencia; - a k+1. struktura egy felteteles elagazas; - a k+1. struktura egy iteracio. -=- a.) A k+1. struktura egy szekvencia: s(x,y) = s_1(x,y) ; s_2(x,y); A program fuggvenyek: f_s_1(x,y), f_s_2(x,y). Indukcios feltevesunk: {Q(x) \and y=I_s_1(x)} s_1(x,y) {Q(x) \and y=O_s_1(x)}, {Q(x) \and y=I_s_2(x)} s_2(x,y) {Q(x) \and y=O_s_2(x)}, tetelek helyessege Hoare modszerrel bebizonyithatoak. azaz O_s_1(x)=f_s_1(x,I_s_1(x)), es O_s_2(x) = f_s_2(x,I_s_2(x)). A szekvencia szemantikaja alapjan: I_s(x) = I_s_1(x), es O_s_1(x) = I_s_2(x) es O_s_2(x) = O_s(x); ezert f_s(x, I_s(x)) = f_s_2(x,f_s_1(x, I_s_1(x))). -=- {Q(x)\and y=I_s_1(x)} S_1(x,y){Q(x)\and y=O_s_1(x)}, {Q(x)\and y=I_s_2(x)} S_2(x,y){Q(x)\and y=O_s_2(x)}, ---------------------------------------------------- {Q(x)\and y=I_s(x)}S_1(x,y);S_2(x,y){Q(x)\and y=O_s(x)} -=- b.) a k+1. struktura egy felteteles elagazas: s(x,y) = if \alpha(x,y) then S_1(x,y) else S_2(x,y) fi, Indukcios feltevesunk szerint: {Q(x) \and y=I_s_1(x)}S_1(x,y){Q(x)\and y=O_s_1(x)}, {Q(x) \and y=I_s_2(x)}S_2(x,y){Q(x)\and y=O_s_2(x)}, tetelek helyessege Hoare modszerrel bebizonyithatok. (Q(x)\and y=I_s(x,y) \and\alpha(x,y)) => (Q(x)\and y=I_s_1(x,y)), (Q(x)\and y=I_s(x,y) \and~\alpha(x,y)) => (Q(x)\and y=I_s_2(x,y)), masreszt (Q(x)\and y=I_s(x,y)\and \alpha(x,y))=>O_s(x)=O_s_1(x), (Q(x)\and y=I_s(x,y)\and ~\alpha(x,y))=>O_s(x)=O_s_2(x), -=- Q(x)\and y=I_s(x,y) \and \alpha(x,y)) => (Q(x) \and y=I_s_1(x,y)), (Q(x)\and y=I_s(x,y) \and ~\alpha(x,y)) => (Q(x) \and y=I_s_2(x,y)), {Q(x)\and y=I_s_1(x))} S_1(x,y){Q(x)\and y=O_s_1(x)}, {Q(x)\and y=I_s_2(x)}S_2(x,y) {Q(x)\and y=O_s_2(x)}, (Q(x)\and y=O_s_1(x)) => y=O_s(x), (Q(x)\and y=O_s_2(x)) => y=O_s(x), ------------------------------- {Q(x)\and y=I_s(x)} if \alpha (x,y)) then S_1(x,y) else S_2(x,y) fi {Q(x) \and y=O_s(x)}. -=- c.) k+1. struktura egy iteracio: s(x,y) = while \alpha(x,y) do A(x,y) od. {Q(x) \and y=I_A(x)}A(x,y){Q(x)\and y=O_A(x)} mar bizonyithato a Hoare modszerrel. Legyen A(x,y) programfuggvenye: f_A(x,y). A tetel, amely bizonyithato: {Q(x) \and y=I_A(x)} y<-f_A(x,y) {Q(x) \and y=O_A(x)}. -=- Jeloles: k=0 => h(x,y,k) = y. k>0 => h(x,y,k) = f_A(x, f_A(x, ...(f_A(x,y)))); 1 2 ... k -=- Az iteracio szemantikajat leiro invarians: I(x,y,k):Q(x)\and y=h(x,I_A(x),k) \and f_s(x,y) = f_s(x, I_s(x)). -=- A bizonyitando tetelek: (Q(x) \and y=I_s(x)) => I(x,y,0); {I(x,y,k) \and \alpha(x,y)} A(x,y) {I(x,y,k+1) }; (I(x,y,k) \and ~\alpha(x,y)) => (Q(x) \and y=O_s(x)). -=- 1. tetel (Q(x) \and y=I_s(x)) => I(x,y,0), (Q(x) \and y=I_s(x)) => (Q(x) \and y=I_A(x) \and f_s(x,y) = f_s(x, I_s(x))), ami trivialis. -=- 2. tetel. {I(x,y,k) \and \alpha(x,y)} A(x,y) { I(x,y,k+1)}, az ertekadas kovetkeztetesi szabalya alapjan: (I(x,y,k) \and \alpha(x,y)) => I(x,f_A(x,y), k+1), (Q(x)\and y=h(x,I_A(x), k)\and f_s(x,y) = f_s(x, I_s(x)) \and \alpha(x,y)) => (Q(x) \and f_A(x,y)=h(x, I_A(x), k+1) \and f_s(x, f_A(x,y)) = f_s(x,I_s(X)). -=- 3. tetel. (I(x,y,k) \and ~\alpha(x,y)) => (Q(x) \and y=O_s(X)), azaz (Q(x) \and y=h(x,I_A(x), k) \and f_s(x,y) = f_s(x,I_S(x)) \and ~alpha(x,y)) => (Q(x) \and y=O_S(x)). Mivel ~\alpha(x,y) eseten f_s(x,y)=y, masreszt a definicio alapjan f_s(x,I_s(x)) = O_s(x). -=- Q(x) \and y=I_s(x) => I(x,y,0); {I(x,y,k) \and \alpha(x,y)} A(x,y) { I(x,y,k+1) }; I(x,y,k) \and ~\alpha(x,y) => Q(x) \and y=O_s(x). --------------------------------------------------- {Q(x) \and y=I_s(x)} while \alpha(x,y) do A(x,y) od {Q(x) \and y=O_s(x) }. -=- Adva d_s=(A, F, E_a); absztrakt specifikacio d_c=(C,G,E_c); konkret specifikacio. A={A_0, A_1, ..., A_n}; F={f_0, f_1, ..., f_m}; C={C_0, C_1, ..., C_n}; G={g_0, g_1, ..., g_m}; E_a = {..., e_a_i(..., f_j(a), ...; a), ...}; E_c={...., i_c_i(..., g_j(c), ...;c), ...}; A reprezentacios fuggveny: \fi: C-> a=A, f_0=\fi(g_0), (\forall f_c\inF_c)(\forall c\in C)((f_c(\fi(c))=\fi(g_c(c)). -=- Altalanos formaban az azonos jelentes: e_a_i(..., f_j(\fi(c)), ...;\fi(c)) = e_c_i(..., g_j(c), ...;c). A helyesseg definiciojat szimulacio alapjan definialtuk: (\forall f_s\in F_s)(\forall c\in C)(f_s(\fi(c)) =\fi(g_s(c))). -=- Az azonos jelentes: - "Algebrai - algebrai" eset: f_s(f_c(\fi(c)) = f_c(f_s(\fi(c))) \triplaegyenlo g_s(g_c(c)) = g_c(g_s(c)). - "Kulso felulet - kulso felulet" eset: (pref_i(\fi(c)) \and postf_i(\fi(c),\fi(c')))\triplaegyenlo(preg_i(c)\and postg_i(c,c')).