Компьютерлік бағдарламаның дұрыстығын тексеру ережелері: Хоар логикасы, программа кодын формалды түрде дәлелдеуге көмектеседі. Бағдарламаның қатесіздігін қамтамасыз етеді.
Хоар логикасы (Флойд-Хоар логикасы немесе Хоар ережелері деп те аталады) – компьютерлік бағдарламалардың дұрыстығын қатаң түрде дәлелдеуге арналған логикалық ережелер жиынтығы бар формалды жүйе. Оны 1969 жылы британдық компьютер ғалымы және логик Тони Хоар ұсынды, ал кейіннен Хоар және басқа зерттеушілер оны жетілдірді. Алғашқы идеялар Роберт В. Флойдтың ағын диаграммалары үшін ұқсас жүйені жариялаған жұмысымен байланысты.
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician Tony Hoare, and subsequently refined by Hoare and other researchers. The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system for flowcharts.
Үш есе көп
Хоар логикасының негізгі ерекшелігі – Хоар үштігі. Үштік кодтың орындалуы есептеу күйін қалай өзгертетінін сипаттайды. Хоар үштігі мынадай формада болады:
The central feature of Hoare logic is the Hoare triple. A triple describes how the execution of a piece of code changes the state of the computation. A Hoare triple is of the form
мұнда және – талаптар, ал – команда. талапты алғы шарт деп, ал – кейінгі шарт деп атайды: алғы шарт орындалғанда команданы орындау кейінгі шартты қамтамасыз етеді. Талаптар – предикат логикасындағы формулалар. Хоар логикасы қарапайым императивті бағдарламалау тілінің барлық құрылымдары үшін аксиомалар мен логикалық қорытындылар ережелерін ұсынады. Хоардың бастапқы мақаласындағы қарапайым тіл ережелеріне қоса, Хоар және көптеген басқа зерттеушілер одан бері басқа тілдік құрылымдар үшін де ережелерді әзірледі. Параллелизм, процедуралар, секірулер және көрсеткіштер үшін ережелер бар.
where and are assertions and is a command. is named the precondition and the postcondition: when the precondition is met, executing the command establishes the postcondition. Assertions are formulae in predicate logic. Hoare logic provides axioms and inference rules for all the constructs of a simple imperative programming language. In addition to the rules for the simple language in Hoare's original paper, rules for other language constructs have been developed since then by Hoare and many other researchers. There are rules for concurrency, procedures, jumps, and pointers.
Ішінара және толық дұрыстығы
Стандартты Хоар логикасын қолдану арқылы тек ішінара дұрыстығын дәлелдеуге болады. Толық дұрыстығын қосымша тоқтату талап етеді, оны жеке немесе While ережесінің кеңейтілген нұсқасымен дәлелдеуге болады. Осылайша, Хоар үштігін түсінудің интуитивті жолы: егер жай-күй орындалу алдында сақталса, онда орындалғаннан кейін де сақталады, немесе орындалу тоқтамайды. Соңғы жағдайда "кейін" деген ұғым болмайды, сондықтан кез келген оператор болуы мүмкін. Шындығында, орындалу тоқтамайтынын көрсету үшін оператор жалған болуы мүмкін. "Тоқтату" осы жерде және мақаланың қалған бөлігінде есептеудің аяқталуын білдіреді, яғни шексіз циклдардың болмауын білдіреді; ол бағдарламаны мерзімінен бұрын тоқтатуға әкелетін орындалу шектерінің бұзылуын (мысалы, нөлге бөлу) білдірмейді. 1969 жылғы мақаласында Хоар тоқтатудың тар ұғымын қолданды, ол орындалу шектерінің бұзылуын да қамтыды, бірақ тоқтатудың кең ұғымын қалауын білдірді, себебі ол нақтылауларды орындалудан тәуелсіз етеді:
Using standard Hoare logic, only partial correctness can be proven. Total correctness additionally requires termination, which can be proven separately or with an extended version of the While rule. Thus the intuitive reading of a Hoare triple is: Whenever holds of the state before the execution of , then will hold afterwards, or does not terminate. In the latter case, there is no "after", so can be any statement at all. Indeed, one can choose to be false to express that does not terminate. "Termination" here and in the rest of this article is meant in the broader sense that computation will eventually be finished, that is it implies the absence of infinite loops; it does not imply the absence of implementation limit violations (e. g. division by zero) stopping the program prematurely. In his 1969 paper, Hoare used a narrower notion of termination which also entailed the absence of implementation limit violations, and expressed his preference for the broader notion of termination as it keeps assertions implementation independent:
Бос мәлімдеме аксиомасының схемасы
Бос оператор ережесі оператор бағдарламаның күйін өзгертпейтінін күзеді, демек, оператордан бұрын рас болған нәрсе, одан кейін де рас болады.
The empty statement rule asserts that the statement does not change the state of the program, thus whatever holds true before also holds true afterwards.