Лекция: 45 сағат С¤Ж: 45 саѓат обс¤Ж: 45 саѓат Барлыќ саѓат саны: 135 саѓ Ќорытынды баќылау: емтихан 2 семестр


Лекция 6 Таќырыбы: Семантика мінездемелері



бет7/31
Дата24.04.2016
өлшемі1.97 Mb.
#79257
түріЛекция
1   2   3   4   5   6   7   8   9   10   ...   31

Лекция 6

Таќырыбы: Семантика мінездемелері.





  1. Жүйеге қойылатын соңғы шарт пен алғы шарт.

  2. Жүйе семантикасы.

1. Егер біз ең үлкен ортақ бөлінгішті таба алатын машина құрғымыз келсе, онда машинаның соңғы жағдайы



x=EOБ(x,y) (1)

шартын қанағаттандыру керек деп талап етеміз. (Алдын қарастырған машина үшін x=EOБ(x,y) шарты да орындалу керек болады. Өйткені ойын x=y шарттарда аяқталатын еді. X-тің мәнін жауап ретінде қабылдаймыз деп шешсек, онда бұл шартты талап етпеуге болады).

(1) шартын соңғы шарт деп атаймыз. Бұлай аталудың себебі бұл шарт жүйенің жұмысы аяқталған кезегі жағдайына қойылады. Соңғы шартты көптеген мүмкін болған жағдайлар қанағаттандыру мүмкін. Бұл жағдайда бұлардың барлығы бірдей қанағаттанарлы деп есептелінсін, сондықтан соңғы жағдайды бастапқы жағдайға тәуелді бір мәнді функция болсын деп талап етуде негіз жоқ.

Бұл машинаны жауап алу үшін қолданар болсақ (Мысалы: x және y мәндер үшін (1) шартын қанағаттандыратындай етіп соңғы жағдайға жетуін қалаймыз), онда сәйкес бастапқы жағдайлар жиынын дәлірей, жүйенің жұмысын міндетті түрде дұрыс аяқталуына әкелетін әр жүйенің соңғы жағдайы соңғы шартты қанағаттандыратындай бастапқы жағдайда жиынын анықтау дұрыс болар еді.

Картондағы евклид ойыны үшін мысал келтірелік: (1) соңғы шартын қанағаттандыратын ақырғы жағдайы бар болады деп сендіре аламыз.

ЕОБ(x,y)=ЕОБ(X,Y) and (2) шартын қанағаттандыратын кез келген бастапқы жағдай үшін x,y комбинацияларының көп жағдайларда (2) шартты қанағаттандырады.

Дұрыс аяқталу оқиғасына келетін әрі жүйе берілген соңғы шартты қанағаттандыратын ақырғы жағдайда қалатындай барлық бастапқы жағдайда жиынын сипаттайтын шарт “Соңғы шартқа сәйкес келетін әлсіз алғы шарт ” деп аталынады. (“Әлсіз”деп атауымыздың себебі, шарт қаншалықты әлсіз болса, көбірек жағдайлар оны қанағаттандыра алады. Біз қалап отырған соңғы жағдайға әкелетін барлық мүмкін болған бастапқы жағдайларда сипаттауға тырысамыз).

Егер жүйені (машина, конструкция)-S арқылы, ал соңғы шартты – R арқылы белгілеп алсақ онда бұларға сәйкес келетін алғы шартты былай белгілейміз:

WP(S,R)

(Weakest pre-condition ағылшын сөзінің бас әріптерін тереміз).



Егер бастапқы жағдайда WP(S,R) шартын қанағаттандырса онда конструкция ақыр соңында R-дің ақиқат болғандығын көрсетеді.
2. S конструкциясының қалай жұмыс істейтіні бізге белгілі деп есептейміз. Егер кез келген соңғы шарт R үшін сәйкес келетін алғы шарт WP(S,R) шығарып алатын болсақ осылайша бұл конструкцияның біз үшін нелер істей алатынын ұқсақ бұл “оның семантикасы” деп аталады.

Бұл жерде мына нәрсені айта кету керек: Мүмкін болған соңғы шарттардың жиыны өте үлкен, сондықтан әр біріне сәйкес келетін алғы шарттарымен қоса таблицалық түрде қамти шолу мүмкін емес.

Сондықтан, берілген конструкцияның семантика анықтамасы басқаша жолмен, яғни кез келген берілген R соңғы шарт үшін әлсіз алғы шартты WP(S,R) қалай шығару керектігін ережелер түрінде береді.

Нақты S конструкциясы үшін, соңғы шартты білдіретін берілген R предикатор бойынша сәйкесінше әлсіз алғы шартты білдіретін WP(S,R) предикатын шығару ережесі n предикаттары түрлендіруші деп аталады.

S конструкциясының семантикасы деген уақытта осы конструкция предикаттарының түрлендірушісі туралы сөз барады.

Лекция 7

Тақырыбы: Предикат түрлендірушісінің қасиеттері



1. Қасиет1. Қасиет2

2. Қасиет 3

3. Қасиет 4,4’
1. R соңғы шартының функциясы бетінде қарастырылатын предикаттар түрлендірушісімен бірнеше анықталған қасиеттерге ие.

Қасиет 1. Кез келген S конструкциясы үшін

WP (S,F)=F

Айталық, бұл теңдік орындалмасын. Мұндай WP (S,F) шартын қанағаттандыратын ең болмаса бір жағдай табылар еді. Бұл жағдайда S конструкциясының бастапқы жағдайы ретінде аламыз. Анықтамаға сәйкес S-і іске қосу F предикатын қанағаттандырады соңғы жағдайға әкеледі. Бірақ бұл жерде қарама-қайшылық туады, F предикатының анықтамасы бойынша F-і қанағаттандыратын жағдай жоқ, осылайша (4) қатынасты дәлелдейді.

Қасиет 2. Кез-келген S конструкциясы және барлық жағдайлар үшін (5) Q=>R қатынасы орындалатын Q, R соңғы шарттары үшін мына қатынас орындалады.

WP(S,Q)=> WP(S,R) (6)


Шындығында, WP(S,Q) –і үшін қанағаттандыратын кез келген бастапқы жағдайда жүйе жұмысының ақырғы жағдайы үшін анықтама бойынша Q орындалады. (5) қатынасын ескерсек R-ң де орындалатындығы келіп шығады. Демек, берілген бастапқы жағдай бір мезгілде WP(S,R) шартын да қанағаттандыратын болады, (6)-да көрсетілгендей қасиет-2 бұл монотондық қасиет.
2. Қасиет 3. Кез келген S конструкциясы және Q және R соңғы шарттар үшін WP(S,Q) and WP(S,R) = WP(S,Q and R) (7) ќатынасы орындалады. [and = ]

Жағдайлар кеңестігінің кез келген нүктесінде (7) –ң сол жағынан оң жағы келіп шығады, өйткені WP(S,Q) және WP(S,R) –ді қанағаттандыратын кез келген бастапқы жағдайлар үшін Q және R-ді қанағаттандыратын жағдайдың болатындығын білеміз. Одан әрі анықтамаға сәйкес барлық жағдайлар үшін



(Q and R)=>Q

ќасиет 2-ні ескеріп барлық жағдайлар үшін WP(S,Q and R )=> WP(S,Q)

дәл осылай барлық жағдайлар үшін WP(S,Q and R )=> WP(S,R) бола алады. Бірақ A=>B және A=>C болса, онда A=>(B and C) деуімізге болады. Сондықтан жағдайлар кеңіәстігінің кез келген нүктесінде (7) –ң оң жағынан сол жағы келіп шығады. Екі жақта барлық жерде бірінен - бірі келіп шығатындықтан олар тең болу керек. Осылай 3-қасиет дәлелденеді.


3. Қасиет 4. Кез келген S конструкциясы үшін және кез келген Q және R соңғы шарттар үшін (WP(S,Q or R )=> WP(S,R))=> WP(S,Q or R ) (8) қатынасы барлық жағдайлар үшін ақиқат болады.

Анықтамаға сәйкес барлық жағдайлар үшін WP(S,Q )=> WP(S,Q or R) дәл осылай WP(S,R )=> WP(S,Q or R) барлық жағдайда A=>C және B=>C үшін (A or B)=>C деуге болады. Осылай (8) қатынастың ақиқат екендігі дәлелденеді.

Қасиет 4. Кез келген детерминерленген S конструкциясы кез келген Q және R соңғы шарттар үшін

(WP(S,Q ) or WP (S,R))=WP(S,Q or R) (8)

Бұл қатынастың енді оң жағынан сол жағы келіп шығатынын көрсету қажет. WP(S,Q or R ) алғы шартын қанағаттандыратын қайсы бір бастапқы жағдайда қарастырайық, бұл бастапқы жағдайға жалғыз ғана ақырғы жағдай сәйкес келеді. Ол Q- ді R-ді не екеуінде қанағаттандыруы мүмкін, бұдан шығатыны бастапқы жағдай WP(S,Q) –ді не WP(S,R)-ді не екеуінде, яғни ол WP(S,Q) or WP(S,R)-ді қанағаттандыруы керек. Сонымен 4-қасиет дәлелденді. [детерминерленген машина үшін конструкцияны іске қосқанда кейінгі оқиғалар толығымен оның бастапқы жағдайымен анықталады. Бірдей бастапқы жағдайда екі мәрте қайталап іске түсірсек, бірдей оқиғалар жүреді деп айта алмаймыз. Мүмкін болған оқиғалар класының қайсы бір оқиғасы жүреді]. F арқылы жағдайлар кеңестігінің барлық нүктесінде жалған болатын предикатын белгілейміз; ол бос жиынға сәйкес келеді.



Достарыңызбен бөлісу:
1   2   3   4   5   6   7   8   9   10   ...   31




©dereksiz.org 2024
әкімшілігінің қараңыз

    Басты бет