Maude жүйесі: Қайта жазу логикасы және формальды дәлелдеу құралы
Maude system
Maude – қайта жазу логикасын іске асыратын тегін бағдарламалық құрал. Объектілік есептеуге арналған, метапрограммалау мүмкіндігі зор. Онлайн оқулықтар бар.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Мод жүйесі қайта жазу логикасының іске асырылуы болып табылады. Ол жалпы көзқарасымен Джозеф Гогеннің теңдеу логикасын іске асырған OBJ3 жүйесіне ұқсас, бірақ реттік сұрыпталған теңдеу логикасының орнына қайта жазу логикасына негізделген, сондай-ақ рефлексия негізіндегі қуатты метапрограммалауға баса назар аударады. Maude – тегін бағдарламалық қамтамасы, және оқулықтары интернетте қолжетімді. Ол бастапқыда SRI International ұйымда әзірленген, бірақ қазір түрлі зерттеушілердің ынтымақтастығымен дамытылуда.
The Maude system is an implementation of rewriting logic. It is similar in its general approach to Joseph Goguen's OBJ3 implementation of equational logic, but based on rewriting logic rather than order sorted equational logic, and with a heavy emphasis on powerful metaprogramming based on reflection. Maude is free software, and tutorials are available online. It was originally developed at SRI International, but is now developed by a diverse collaboration of researchers.
Кіріспе
Мод C, Java немесе Perl сияқты әдеттегі императивті тілдер шешетін проблемалар жиынтығынан өзгеше проблемаларды шешуге тырысады. Бұл формалды ой-пікір құралы, ол бізге нәрселердің «қалай болуы керек» екенін тексеруге көмектеседі және егер олай болмаса, неге олай емес екенін көрсетеді. Басқаша айтқанда, Мод бізге қандай да бір ұғымды өте абстрактілі түрде формалды түрде анықтауға мүмкіндік береді (құрылымның ішкі өрнегі және т.б. туралы ойланбай), бірақ біздің теориямызға қатысты теңдіктерді (теңдеулер) және оның қандай күй өзгерістерінен өте алатынын (қайта жазу ережелері) сипаттауға болады. Мод модульдері (қайта жазу теориялары) терминдер тілінен және теңдеулер мен қайта жазу ережелерінің жиынтығынан тұрады. Қайта жазу теориясындағы терминдер операторларды (бір немесе бірнеше аргументтерді қабылдайтын және белгілі бір типтегі терминді қайтаратын функциялар) пайдалана отырып құрастырылады. 0 аргумент қабылдайтын операторлар тұрақтылар деп есептеледі, ал олардың терминдер тілі осы қарапайым құрылымдар арқылы құрастырылады. Мод пайдаланушыға операторлардың инфикс, постфикс немесе префикс (дефолтты) пішінде болуын анықтауға мүмкіндік береді, бұл кіріс терминдері үшін орнын толтырушы ретінде астыңғы сызықтарды қолдану арқылы жасалады. Кеміту теңдеулері конгруэнтті және тоқтатылатын деп есептеледі. Қайта жазу ережелерінде мұндай шектеу жоқ. Мод «орындалған» кезде, ол теңдеулер мен қайта жазу ережелеріне сәйкес терминдерді қайта жазады. Мод, егер біздің теңдеулер жинағымыздағы теңдеудің сол жағына қайта жазуға (немесе кемітуге) тырысатын жабық термин сәйкес келсе, терминдерді теңдеулерге сәйкес қайта жазады. Сәйкестік дегеніміз – теңдеудің сол жағындағы айнымалыларды ауыстыру, нәтижесінде термин қайта жазуға/кемітуге тырысатын терминмен толықтай сәйкес келеді. Теңдеулер мен қайта жазу ережелері шартты ережелер де болуы мүмкін, яғни олар терминге қолданылуы үшін белгілі бір шарттарды орындауы керек (қайта жазу ережесінің сол жағына сәйкес келуден басқа). Ережелер Мод жүйесімен «кәдімгідей» қолданылады, яғни сіз бір ереженің екінші ереженің алдында қолданылатынына сенімді бола алмайсыз. Егер теңдеуді терминге қолдануға болады, онда ол әрқашан кез келген қайта жазу ережесінен бұрын қолданылады. Модтың кіріктірілген іздеу функциясы қажетсіз күйлерді іздеп, мұндай күйлерге жету мүмкін еместігін көрсетуге болады. Мод, қайта жазу логикасының рефлексивті қасиеттеріне байланысты, метабағдарламалау арқылы әр қадамда қандай ережелерді қолдану керектігін бақылауға мүмкіндік береді.
Maude sets out to solve a different set of problems than ordinary imperative languages like C, Java or Perl. It is a formal reasoning tool, which can help us verify that things are "as they should", and show us why they are not if this is the case. In other words, Maude lets us define formally what we mean by some concept in a very abstract manner (not concerning ourselves with how the structure is internally represented and so on), but we can describe what is thought to be the equal concerning our theory (equations) and what state changes it can go through (rewrite rules). Maude modules (rewrite theories) consist of a term language plus sets of equations and rewrite rules. Terms in a rewrite theory are constructed using operators (functions taking 0 or more arguments of some sort, which return a term of a specific sort). Operators taking 0 arguments are considered constants, and one constructs their term language by these simple constructs. Maude lets the user specify whether or not operators are infix, postfix or prefix (default), this is done using underscores as place fillers for the input terms. Reduction equations are assumed to be confluent and terminating. Rewrite rules do not have this restriction. When Maude "executes", it rewrites terms according to the equations and rewrite rules. Maude rewrites terms according to the equations whenever there is a match between the closed terms that one tries to rewrite (or reduce) and the left hand side of an equation in our equation set. A match in this context is a substitution of the variables in the left hand side of an equation which leaves it identical to the term that one tries to rewrite/reduce. Equations and rewrite rules can also be conditional rules, which means they have to fulfill some criteria to be applied to the term (other than just matching the left hand side of the rewrite rule). The rules are applied at "random" by the Maude system, meaning that you can not be sure that one rule is applied before another rule and so on. If an equation can be applied to the term, it will always be applied before any rewrite rule. Maude's built in search can look for unwanted states and show that no such states can be reached. Maude has the ability to control what rule applications should be attempted at each step using meta programming, due to the reflective property or rewriting logic.
Қолданылуы
Мод қауіпсіздік протоколдары мен маңызды кодты тексеру үшін қолданылды. Maude жүйесі криптографиялық протоколдардағы қателерді жүйенің не істей алатынын ғана сипаттап, және протоколға жету мүмкін емес жағдайларды (күйлерді немесе терминдерді) іздеу арқылы дәлелдеді. Осылайша протоколдағы қателер анықталады, бұл бағдарламалау қатесі емес, көптеген бағдарламашылардың "сәтті жолмен" жүріп болжай алмайтын жағдайлардың туындауынан болады.
Maude has been used to validate security protocols and critical code. The Maude system has proved flaws in cryptography protocols by just specifying what the system can do, and by looking for unwanted situations (states or terms that should not be possible to reach) the protocol can be shown to contain bugs, not programming bugs but situations happen that are hard to predict just by walking down the "happy path" as most developers do.