title: Ð­ÐºÑÐ¿ÐµÑÐµÐ¼ÐµÐ½ÑÑ Ñ ÑÐµÐ°Ð»Ð¸Ð·Ð°ÑÐ¸ÐµÐ¹ ÑÐ·ÑÐºÐ° Ð¾Ñ ÑÐ°Ð½ÑÐµÐ¼ÑÑ ÐºÐ¾Ð¼Ð°Ð½Ð´ ÐÐµÐ¹ÐºÑÑÑÑ
title: Ð²ÑÐ¿ÑÑÐºÐ½Ð°Ñ ÐºÐ²Ð°Ð»Ð¸ÑÐ¸ÐºÐ°ÑÐ¸Ð¾Ð½Ð½Ð°Ñ ÑÐ°Ð±Ð¾ÑÐ° Ð±Ð°ÐºÐ°Ð»Ð°Ð²ÑÐ°
titleType: Subtitle
title: Experiments with the implementation of the Dijkstra's guarded command language
Creators: name: Ð¡Ð¾Ð»Ð¾Ð¼Ð°ÑÐ¸Ð½, ÐÐ°ÐºÐ°Ñ
Publisher: name: Ð¡Ð°Ð½ÐºÑ-ÐÐµÑÐµÑÐ±ÑÑÐ³ÑÐºÐ¸Ð¹ Ð¿Ð¾Ð»Ð¸ÑÐµÑÐ½Ð¸ÑÐµÑÐºÐ¸Ð¹ ÑÐ½Ð¸Ð²ÐµÑÑÐ¸ÑÐµÑ ÐÐµÑÑÐ° ÐÐµÐ»Ð¸ÐºÐ¾Ð³Ð¾
Year: 2021
Subjects: ÑÐ°Ð·ÑÐ°Ð±Ð¾ÑÐºÐ° Ð¸Ð½ÑÐµÑÐ¿ÑÐµÑÐ°ÑÐ¾ÑÐ°
ÑÐ·ÑÐº Ð¾Ñ ÑÐ°Ð½ÑÐµÐ¼ÑÑ ÐºÐ¾Ð¼Ð°Ð½Ð´
ÑÐ¾ÑÐ¼Ð°Ð»ÑÐ½Ð°Ñ Ð²ÐµÑÐ¸ÑÐ¸ÐºÐ°ÑÐ¸Ñ Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼
Ð¿Ð¾ÑÐ°Ð³Ð¾Ð²Ð¾Ðµ ÑÑÐ¾ÑÐ½ÐµÐ½Ð¸Ðµ
interpreter development
guarded command language
program formal verification
stepwise refinement

description: Ð Ð´Ð°Ð½Ð½Ð¾Ð¹ ÑÐ°Ð±Ð¾ÑÐµ Ð¸Ð·Ð»Ð¾Ð¶ÐµÐ½ Ð¿Ð¾Ð´ÑÐ¾Ð´ Ðº Ð´Ð¾ÐºÐ°Ð·Ð°ÑÐµÐ»ÑÑÑÐ²Ñ ÐºÐ¾ÑÑÐµÐºÑÐ½Ð¾ÑÑÐ¸ Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼ Ñ Ð¿Ð¾Ð¼Ð¾ÑÑÑ Ð¿Ð¾ÑÑÑÐ¾ÐµÐ½Ð¸Ñ Ð¸Ñ Ð´ÐµÐ½Ð¾ÑÐ°ÑÐ¸Ð¾Ð½Ð½Ð¾Ð¹ ÑÐµÐ¼Ð°Ð½ÑÐ¸ÐºÐ¸ Ð½Ð° Ð¾ÑÐ½Ð¾Ð²Ðµ Ð¾Ð¿ÑÐµÐ´ÐµÐ»ÐµÐ½Ð½Ð¾Ð¹ ÑÐµÐ¼Ð°Ð½ÑÐ¸ÐºÐ¸ Ð¾Ð¿ÐµÑÐ°ÑÐ¾ÑÐ¾Ð² ÑÐ·ÑÐºÐ°. ÐÐ»Ñ ÑÑÐ¾Ð³Ð¾ ÑÐ°ÑÑÐ¼Ð¾ÑÑÐµÐ½ Ð¸ ÑÐµÐ°Ð»Ð¸Ð·Ð¾Ð²Ð°Ð½ ÑÐ·ÑÐº Ð¾ÑÑÐ°Ð½ÑÐµÐ¼ÑÑ ÐºÐ¾Ð¼Ð°Ð½Ð´, Ð¿ÑÐµÐ´Ð»Ð¾Ð¶ÐµÐ½Ð½ÑÐ¹ Ð­. ÐÐµÐ¹ÐºÑÑÑÐ¾Ð¹ Ð² ÑÐ²Ð¾ÐµÐ¼ ÑÑÑÐ´Ðµ "ÐÐ¸ÑÑÐ¸Ð¿Ð»Ð¸Ð½Ð° Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼Ð¸ÑÐ¾Ð²Ð°Ð½Ð¸Ñ". Ð ÐµÐ°Ð»Ð¸Ð·Ð°ÑÐ¸Ñ ÑÐ·ÑÐºÐ° ÑÐ¾ÑÑÐ¾Ð¸Ñ Ð¸Ð· Ð¸Ð½ÑÐµÑÐ¿ÑÐµÑÐ°ÑÐ¾ÑÐ° Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼ Ð¸ Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼Ð½Ð¾Ð³Ð¾ Ð¸Ð½ÑÑÑÑÐ¼ÐµÐ½ÑÐ°, Ð²ÑÐ²Ð¾Ð´ÑÑÐµÐ³Ð¾ Ð¿ÑÐµÐ´ÑÑÐ»Ð¾Ð²Ð¸Ðµ Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼Ñ Ð¿Ð¾ Ð·Ð°Ð´Ð°Ð½Ð½Ð¾Ð¼Ñ Ð¿Ð¾ÑÑÑÑÐ»Ð¾Ð²Ð¸Ñ. Ð¯Ð·ÑÐº ÑÐ½Ð°Ð±Ð¶ÐµÐ½ ÑÑÐµÐ´ÑÑÐ²Ð°Ð¼Ð¸, Ð¿Ð¾Ð·Ð²Ð¾Ð»ÑÑÑÐ¸Ð¼Ð¸ ÑÐ¾ÐµÐºÑÐ¸ÑÐ¾Ð²Ð°ÑÑ ÑÐ»Ð¾Ð¶Ð½ÑÐµ Ð°Ð»Ð³Ð¾ÑÐ¸ÑÐ¼Ñ Ð¼ÐµÑÐ¾Ð´Ð¾Ð¼ Ð¿Ð¾ÑÐ°Ð³Ð¾Ð²Ð¾Ð³Ð¾ ÑÑÐ¾ÑÐ½ÐµÐ½Ð¸Ñ. Ð Ð°ÑÑÐ¼Ð¾ÑÑÐµÐ½Ñ Ð¿ÑÐ¸Ð¼ÐµÑÑ Ð´Ð¾ÐºÐ°Ð·Ð°ÑÐµÐ»ÑÑÑÐ²Ð° ÐºÐ¾ÑÑÐµÐºÑÐ½Ð¾ÑÑÐ¸ Ð½ÐµÐºÐ¾ÑÐ¾ÑÑÑ Ð»Ð³Ð¾ÑÐ¸ÑÐ¼Ð¾Ð² Ñ Ð¿Ð¾Ð¼Ð¾ÑÑÑ ÑÑÐ¾Ð³Ð¾ Ð¸Ð½ÑÑÑÑÐ¼ÐµÐ½ÑÐ°. Ð¯Ð·ÑÐº Ð¾ÑÑÐ°Ð½ÑÐµÐ¼ÑÑ ÐºÐ¾Ð¼Ð°Ð½Ð´ Ð²Ð¼ÐµÑÑÐµ Ñ ÑÐ°Ð·ÑÐ°Ð±Ð¾ÑÐ°Ð½Ð½ÑÐ¼Ð¸ Ð¸Ð½ÑÑÑÑÐ¼ÐµÐ½ÑÐ°Ð¼Ð¸ Ð¿Ð¾Ð´ÑÐ¾Ð´Ð¸Ñ ÐºÐ°Ðº Ð´Ð»Ñ Ð¿Ð¾ÑÑÑÐ¾ÐµÐ½Ð¸Ñ ÐºÐ¾ÑÑÐµÐºÑÐ½ÑÑ Ð°Ð»Ð³Ð¾ÑÐ¸ÑÐ¼Ð¾Ð², ÑÐ°Ðº Ð¸ Ð´Ð»Ñ Ð¸Ñ Ð¿ÑÐ±Ð»Ð¸ÐºÐ°ÑÐ¸Ð¸ Ð²Ð¼ÐµÑÑÐµ Ñ Ð´Ð¾ÐºÐ°Ð·Ð°ÑÐµÐ»ÑÑÑÐ²Ð¾Ð¼ Ð¸Ñ ÐºÐ¾ÑÑÐµÐºÑÐ½Ð¾ÑÑÐ¸. Ð¯Ð·ÑÐº Ð¾ÑÑÐ°Ð½ÑÐµÐ¼ÑÑ ÐºÐ¾Ð¼Ð°Ð½Ð´ ÑÐ¾ÑÑ Ð¸ ÑÐ²Ð»ÑÐµÑÑÑ ÑÐ´Ð¾Ð±Ð½ÑÐ¼ Ð´Ð»Ñ Ð¿ÑÐ¾Ð²ÐµÐ´ÐµÐ½Ð¸Ñ ÑÐ¾ÑÐ¼Ð°Ð»ÑÐ½ÑÑ ÑÐ°ÑÑÑÐ¶Ð´ÐµÐ½Ð¸Ð¹, Ð¾Ð½ Ð½Ðµ ÑÐ½Ð¸Ð¼Ð°ÐµÑ Ñ Ð¿Ð»ÐµÑ Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼Ð¸ÑÑÐ° Ð½ÐµÐ¾Ð±ÑÐ¾Ð´Ð¸Ð¼Ð¾ÑÑÐ¸ Ð¿ÑÐ¾ÐµÐºÑÐ¸ÑÐ¾Ð²Ð°ÑÑ Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼Ð½ÑÐ¹ ÐºÐ¾Ð´, ÑÐ¿ÐµÑÐ¸ÑÐ¸ÐºÐ°ÑÐ¸Ñ Ð¿ÑÐ¾Ð³ÑÐ°Ð¼Ð¼Ñ Ð¸ ÐµÐµ Ð¸Ð½Ð²Ð°ÑÐ¸Ð°Ð½ÑÑ.
description: This work presents an approach to proving the correctness of programs by constructing ther denotational semantics based on defined semantics of language operators. To do this, there was considered and implemented the guarded command language, proposed by E. Dijkstra in his work "A discipline of programming". The implementation of the language consists of a interpreter and a software tool that derives program precondition for a given postcondition and invariants. The language is developed with tools that allow to design complex algorithms using the stepwise refinement method. Some examples of proving the correctness of algorithms are considered. The guarded command language, alongside with the developed tools, is suitable both for building correct algorithms and for publishing them alongside with their correctness proof. Although the guarded command language is convenient for conducting formal reasoning, it does not remove the need to designb the program specification, program code and it's invariants from the programmer shoulders.