ЖИ бағдарламалардың дұрыстығын дәлелдеуді үйреніп жатыр. Біз НМУ-де бұл мәселемен 1990 жылы айналыстық.

Robinhood инвестициялық финтех-платформасының бас директоры әрі Harmonic компаниясының негізін қалаушылардың бірі Влад Тенев екі жылдан кейін барлық бағдарламалық код формалды верификациядан, яғни оның белгіленген талаптарға сәйкестігін математикалық тұрғыдан дәлелдеуден өтетін болады деп мәлімдеді.

Harmonic компаниясы осы бағытта Aristotle жүйесін дамытып жатыр. Ол ЖИ-ді бағдарламалар мен аппараттық шешімдердің дұрыстығын математикалық тұрғыдан дәлелдеуге қолданады.

Осы жаңалықты оқып отырып, студенттік шағым есіме түсті.

1990 жылы Новосибирск мемлекеттік университетінде (НМУ) Валерий Александрович Непомнящийдің жетекшілігімен осы тақырыпты зерттей бастадым. Ол кезде 1988 жылы жарық көрген «Прикладные методы верификации программ» кітабын оқыдым. Кітапты Валерий Александрович О. М. Рякинмен бірлесіп, академик А. П. Ершовтың редакциясымен жазған.

Осы материалды дайындау барысында Валерий Александровичтің 2021 жылы өмірден өткенін білдім. Ұстазымды алғыс сезімімен еске аламын.

Бағдарламалардың дұрыстығын математикалық тұрғыдан дәлелдеуді біз сол кездің өзінде үйрендік. Ал ЖИ пайда болғалы не өзгерді?

Банк арқылы ақша аударуды мысалға алайық.

Сіз 10 мың теңге аудардыңыз делік. Қосымша тұрып қалды да, сіз батырманы қайта бастық. Бірақ ақша шоттан бір-ақ рет алынуы керек.

Бағдарламаны тестілеу кезінде әзірлеушілер түрлі жағдайларды қайталайды: батырманы қайта басу, байланыстың үзілуі, бірнеше сұраудың бір мезгілде келуі. Осы жағдайларда бағдарламаның дұрыс жұмыс істейтінін тексереді.

Ал формалды верификация бұдан да қатаң міндет қояды: нақты сипатталған шарттар орындалған кезде бір төлемнің екі рет есептен шығарылмайтынын математикалық тұрғыдан дәлелдеу.

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

Алайда мұндай дәлелді құрастыру қажет. Талаптарды нақты тұжырымдап, бағдарламаның әрекетін сипаттап, аралық тұжырымдарды анықтау керек. Мұның бәрі уақыт пен жоғары біліктілікті талап етеді. Непомнящий мен оның әріптестері сол кездің өзінде осы жұмысты автоматтандырумен айналысқан.

Бүгінде не өзгерді?

ЖИ дәлелдерді іздеуге көмектеседі. Ол пайымдау мен дәлел құрастырудың түрлі нұсқаларын ұсынады, ал арнайы формалды механизм олардың математикалық тұрғыдан дұрыстығын тексереді. Қате дәлелдер қабылданбайды.

Aristotle жүйесі бастапқы бағдарламалық кодпен тікелей жұмыс істейді. Жүйе тексеруге болатын қасиеттерді ұсынады, олардың қайсысын дәлелдеуге мүмкіндік болғанын, қайсысы дәлелденбей қалғанын және нәтиже қандай бастапқы жорамалдарға сүйенетінін көрсетеді. Инженер ұсынылған қасиеттерді де, сол жорамалдарды да тексеруі керек.

Қазіргі уақытта Harmonic C тіліндегі бағдарламалар мен Verilog тіліндегі аппараттық сипаттамаларды қолдайтынын мәлімдейді. Мұның ықтимал нәтижесі — формалды верификацияны бағдарламалық жасақтама әзірлейтін командалардың кеңірек қолдануына жол ашу.

Дегенмен, екі жыл ішінде «барлық кодты» тексеру туралы уәдеге сақтықпен қараған жөн. Теневтің өзі бұл технология біртіндеп тарайтынын айтады: алдымен аса маңызды жүйелердің кодынан басталып, кейін басқа бағдарламаларға қолданыла бастайды.

Мұнда бір маңызды мәселе бар.

Банк аударымына қайта оралайық. Белгілі бір функцияның нақты шарттарда ақшаны екі рет есептен шығармайтынын дәлелдеуге болады. Бірақ бұл ақшаның дұрыс алушыға жіберілетініне кепілдік бермейді.

Математикалық дәлел тек өзіне қойылған сұраққа жауап береді. Егер талаптар толық тұжырымдалмаса, математикалық тұрғыдан мінсіз дәлелдің өзі бастапқы міндетті қате қоюдан сақтай алмайды.

Сондықтан қандай талаптардың маңызды екенін және тексеру аясынан тыс не қалғанын түсіну әлі де адамның міндеті.

1990 жылы біз бағдарламаның дұрыстығын дәлелдеуге болатындай етіп, мәселені дұрыс қоюды үйрендік. Бүгінде ЖИ дәлелдің өзін табуға көмектеседі. Бірақ қандай қасиеттердің шынымен маңызды екенін анықтау бұрынғыдай адамның жауапкершілігінде қалады.

Дереккөздер:

Влад Теневтің мәлімдемесі — X

Harmonic — Aristotle: бағдарламалар мен аппараттық шешімдерді верификациялау

Техникалық құжаттама — Aristotle: C тіліндегі бағдарламаларды верификациялау

Непомнящий мен Рякиннің кітабы — Мәскеу мемлекеттік техникалық университетінің каталогы

Даурен Керейбаев - www.linkedin.com/in/dauren-kereibayev-59169461

REAL DIGITAL бас редакторы