- Егер біз ең үлкен ортақ бөлінгішті таба алатын машина құрғымыз келсе, онда машинаның соңғы жағдайы
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-дің ақиқат болғандығын көрсетеді.
- S конструкциясының қалай жұмыс істейтіні бізге белгілі деп есептейміз. Егер кез келген соңғы шарт R үшін сәйкес келетін алғы шарт WP(S,R) шығарып алатын болсақ осылайша бұл конструкцияның біз үшін нелер істей алатынын ұқсақ бұл “оның семантикасы” деп аталады.
Бұл жерде мына нәрсені айта кету керек: Мүмкін болған соңғы шарттардың жиыны өте үлкен, сондықтан әр біріне сәйкес келетін алғы шарттарымен қоса таблицалық түрде қамти шолу мүмкін емес.
Сондықтан, берілген конструкцияның семантика анықтамасы басқаша жолмен, яғни кез келген берілген R соңғы шарт үшін әлсіз алғы шартты WP(S,R) қалай шығару керектігін ережелер түрінде береді.
Нақты S конструкциясы үшін, соңғы шартты білдіретін берілген R предикатор бойынша сәйкесінше әлсіз алғы шартты білдіретін WP(S,R) предикатын шығару ережесі n предикаттары түрлендіруші деп аталады.
S конструкциясының семантикасы деген уақытта осы конструкция предикаттарының түрлендірушісітуралы сөз барады.