- Алдыңғы сабақта біз мынандай тезисті алға тартқан болатынбыз: Егер S конструкцияның предикаттар түрлендірушісін білсек онда S конструкциясының семантикасын жеткілікті жақсы білеміз. Басқаша айтқанда кез келген R соңғы шарты боиынша сәикес келетін мынандай әлсіз алғы шартты шығарып алатын ережені білу керек: Бұл алғы шартпен сипатталатын бастапқы жағдайда іске қосылған жүйе дұрыс аяқталуы, әрі R соңғы шартын қанағаттандыратын жағдайда қалуы керек.
Қысқасы, берілген S және R үшін WP(S,R)-ді қалай шығарып аламыз.
Жақсы анықталған программалаутілдерінің бірінде жазылған программаны предикаттар түрлендірушісін білсек, онда жеткілікті жақсы білетін конструкция ретінде қарастыруға болады.
Әрбір мұндай программа жақсы анықталған программалау тілінде жазылған өзінің текстімен беріледі.
Нақты бір конструкцияның (программманың) предикаттар түрлендірушісімен берілсе, ал программалар тілінің семантикалық мінездемесін осы тілде жазылған кез келген программаға предикаттар түрлендірушісін сәйкес қоюға мүмкіндік беретін ережелер жиыны ретінде қарастырамыз. Мұндай көзқарас тұрғысынан программаны сәйкес предикаттар түрлендірушісінің коды ретінде қарастыра аламыз.
- Өткен сабақта 4 қасиетке ие қарапайым предикаттар түрлендірушіге мысалдар келтірейік.
- МЫСАЛ: Кез келген R соңғы шарты үшін WP(S,R)=R орындалатын S cконструкциясы берілген. Бұл конструкцияны барлық программистер біледі, әрі ұнатады, оларға бұл ”бос оператор” атымен белгілі.
Бұл конструкцияға “өткізу” деп атау береміз. Демек өткізу операторының семантикасы былай анықталады:
WP(өткізу,R)=R барлық R соңғы шарттар үшін, сонымен, біз қайсыбір программалау тілін анықтадық: бұл операторлы тіл, бұл тілде тек бір ғана конструкцияны бейнелеуге болады, ол да болса “қандай болса сол күйін қалдыру”-ды ғана істей алады. (яғни ештеңе істемейді).
- МЫСАЛ: Келесі бір предикаттар түрлендірушісі R соңғы шартына тәуелді болмайтын (қатысы жоқ) тұрақты әлсіз шартқа әкеледі.
БізT және F, 2 предикат-тұрақтыларға иеміз.
[T қарастырылатын жағдайлар кеңестігінің барлық нүктесінде ақиқат болатын предикат ; оған толық жағдайлар жиыны сәикес келеді.]
Алайда, барлық R үшін WP(S,R)=F болатын S конструкциясы барлық керекті қасиеттерді қанағаттандырады. Бұл операторға да “қабылдау” деген ат берейік. “Қабылдау” операторының семантикасы былайша беріледі:
WP (қабылдау,R)=F кез келген R соңғы шарты үшін [ F- бос жиын, барлық жағдайлар кеңістігінде жалған болатын, орындалмайтын предикат].
Бұл оператор “қалай болса сол күйінде қалдыруды” да істей алмайды. “Қабылдамау” конструкциясын іске қоссақ, сол замат тоқтайды, яғни ақырғы жағдайына да жете алмайды.
Біз енді 2 операторлы программалау тіліне иеміз. Бірі “өткізу”, бірі “қабылдамау”. Бұл тілдің синтаксистік формальді түрде анықтамай кетуімізге болмайды.
Бұны біз Бэкустің нормаль формалары жүйесінде береміз: (өткен нормаль сабақтардан белгілі)
<оператор>:= өткізу½қабылдамау.
Былай оқылады: синтакстистік категорияның операторы деп аталатын элементі (< >), өткізу не (1) қабылдау деп анықталады (: :=)
- Меншіктеу операторы.
- Конструкциялар композициясы.
- Келесі бір предикаттар түрлендірушісі (анағұрлым қызғылықты) мынаған негізделеді: R соңғы шартының формальді өрнегінде қайсыбір айнымалының әрбір енуін (яғни осы айнымалы кездескен сайын ) қайсы бір өрнекпен (не тұрақтымен) ауыстырып отырады.
Егер R предикатына х айнымалының барлық енуін қайсібір (Е) өрнегімен ауыстырылып отырса, онда бұл түрлендірудің нәтижесін
REx арқылы белгілейміз. [Мұндай түрлендіру 1-4 қасиеттерді қанағаттандырады].
Бұл предикаттар түрлендірушісі “меншіктеу операторы” деп аталынады және ол мыналарды анықтауы керек:
- Ауыстырылатын айнымалы атауы;
- Предикаттар түрлендірушісіне сәйкес келетін ереже – ауыстыру
екендігі;
- Осы айнымалының соңғы шарттағы барлық енуін ауыстыратын
өрнек;
Егер х айнымалысы (Е) өрнегімен ауыстырылуы керек болса, онда бұл оператордың жазбаша көрінісі мынадай болады:
х:=Е
Бұл оператордың семантикасы былай анықталады:
wp(“x:=E”,R)=RE®x
Бэкустың нормал формаларын пайдаланып, тілдің формальді синтаксисін кеңейтеміз:
<оператор>::= өткізу½қабылдау½ <меншіктеу операторы >
<меншіктеу операторы>::=<айнымалы>:=<өрнек>
соңғы қатарды былай оқу керек: “ меншіктеу операторы” деп аталатын синтаксистік категория элементі “айнымалы” деп аталатын синтаксистік категория элементімен, одан кейін келетін меншіктеу белгісі “ :=”, одан соң “өрнек” деп аталатын синтаксистік категория элементі ретінде анықталады.
Мысал:WP (“a:=7”, a=7) = {7=7}
WP (<<a:=2*b+1>>, a=13)={2*b+1=13}={b=6}
WP (<<a:=a-b>>,a>b)={a-b>b}={a>2*b}.
Барлық R үшін WP(S,R)=T болатын конструкцияның болуы мүмкін емес, өйткені ол1-қасиетті жоққа шығарар еді
- 2 операторлы тілге қарағанда меншіктеу операторымен толықтырылғанпрограммалау тіліміз әлдеқайда бай көрінеді.
Сонда да ол жеткілікті емес: бізге анағұрлым күрделі программалар конструкциялар құру керек. Күрделі конструкциялар құру үшін былайша бейнеленген схемадан пайдаланамыз:
<конструкция>::=<жай конструкция>½<мына түрдегі жазбаны дұрыс композициясы:<конструкция>>
Бұл схема бізге пайдалы болу үшін, екі шарт орындалуы керек:
-біз “жай конструкцияларға”ие болуымыз керек,
-“дұрыс композициялар ”құрылатынын білуіміз керек.
Алдыңғы ендірілген операторларды жай конструкциялар ретінде алуға болады.
Бұл конструкциялардан жаңа конструкция құрылуы мүмкін. Жаңа конструкция құрамы объект (конструкциялар композициясы) ретінде қарастырылады. Композиция бүтіннің қасиеттері, бөліктерінің қасиеттеріненқалай келіп шығатынын анықтауы керек.
Жаңа композиция (жаңа функция) алудың қарапайым әдістерінің бірі –берілген 2 конструкцияның “функционалдық композициясы”, яғни бір функцияның (конструкцияның) мәні 2-ші функцияның аргументі ретінде алынады. Мұндай предикаттартүрлендірушісіне сәйкес келетін құрама объекті “S1; S2” деп белгілеуге келісілген. Анықтаймыз:
WP(<<S1;S2>>,R)=WP(S1,WP(S2,R))
S1және S2 1-н қасиеттеріне ие екендігінен n S1;S2n үшін жоғарыда анықталған предикаттар түрлендірушісі осы 4 қасиетке ие деп ұйғаруға болады.
[ мысалы S1және S2 үшін 1- ші қасиет орындалсын.
WP (“S1,F)=F және WP (S2,F)=F
Жоғарыдағы анықтамадағы R- ң орнына F- і қойып ұйғарамыз:
WP(“S1;S2”,F) = WP(S1,WP(S2,F))=WP(S1,F)=F
Қалған 3 қасиетін де осылай тексеруге болады.]
“S1;S2” құрама конструкциясы мына ережемен орындалады: ”алдымен S1 констукциясын іске қосу, оның жұмысы аяқталған соң S2 іске қосу”
Мысал: Айталық “S1;S2” мынадай болып берілсін
А:=a+b; B:=a*bn және соңғы шарт ретінде қайсы бір R(a,b) предикаты табылсын. Мұндай жағдайда:
WP(S2, R(a,b))=WP(“b:=a*b”, R(a,b))=R(a, a*b) және
WP(nS1;S2n,R(a,b))=WP(S1,WP(S2,R(a,b)))=
=WP(S1,R(a,a*b))
=WP(“a:=a+b”, R(, a*b))
=R(a+b,(a+b)*b)
[Осындай жолмен көптеген жай операторлар да, құрама операторлар да ендіріледі, олардың барлығын қарастырып отырмаймыз.]