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

Лекция 13

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

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

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 ағылшын сөзінің бас әріптерін тереміз).

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

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

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

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

Лекция 14

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

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

2. Қасиет 3

3. Қасиет 4,4’

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)

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

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

(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 арқылы жағдайлар кеңестігінің барлық нүктесінде жалған болатын предикатын белгілейміз; ол бос жиынға сәйкес келеді.