{"id":372559,"date":"2024-05-21T05:15:25","date_gmt":"2024-05-21T05:15:25","guid":{"rendered":"http:\/\/savepearlharbor.com\/?p=372559"},"modified":"-0001-11-30T00:00:00","modified_gmt":"2024-05-21T05:15:25","slug":"","status":"publish","type":"post","link":"https:\/\/savepearlharbor.com\/?p=372559","title":{"rendered":"<span>\u0424\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0432\u043e \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a\u0435 ConCert<\/span>"},"content":{"rendered":"<div><!--[--><!--]--><\/div>\n<div id=\"post-content-body\">\n<div>\n<div class=\"article-formatted-body article-formatted-body article-formatted-body_version-2\">\n<div xmlns=\"http:\/\/www.w3.org\/1999\/xhtml\">\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w1560\/getpro\/habr\/upload_files\/583\/0d2\/cbe\/5830d2cbe72802a7fb6cd6daf396041e.png\" width=\"780\" height=\"440\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/583\/0d2\/cbe\/5830d2cbe72802a7fb6cd6daf396041e.png\"\/><\/figure>\n<p>\u0414\u043e\u0431\u0440\u044b\u0439 \u0434\u0435\u043d\u044c! \u041c\u0435\u043d\u044f \u0437\u043e\u0432\u0443\u0442 \u041a\u0438\u0440\u0438\u043b\u043b \u0417\u0438\u0431\u043e\u0440\u043e\u0432, \u044f \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u044e \u043e\u0442\u0434\u0435\u043b \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0445 \u0441\u0438\u0441\u0442\u0435\u043c Positive Technologies. \u0412 \u044d\u0442\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u043c\u044b <a href=\"https:\/\/habr.com\/ru\/companies\/pt\/articles\/786078\/\">\u043f\u0440\u043e\u0434\u043e\u043b\u0436\u0438\u043c \u043e\u0431\u0441\u0443\u0436\u0434\u0430\u0442\u044c <\/a>\u043c\u0435\u0442\u043e\u0434\u044b \u0438 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u044b \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0438 \u0438\u0445 \u043f\u0440\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u043f\u0440\u0438\u043c\u0435\u043d\u0435\u043d\u0438\u0435 \u0434\u043b\u044f \u043f\u0440\u0435\u0434\u043e\u0442\u0432\u0440\u0430\u0449\u0435\u043d\u0438\u044f \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u0435\u0439. \u041c\u044b \u043f\u043e\u0434\u0440\u043e\u0431\u043d\u043e \u043f\u043e\u0433\u043e\u0432\u043e\u0440\u0438\u043c \u043e \u043c\u0435\u0442\u043e\u0434\u0435 \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438, \u0430 \u0442\u043e\u0447\u043d\u0435\u0435, \u043e \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a\u0435 \u0434\u043b\u044f \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u2014 ConCert.<\/p>\n<h2>\u0427\u0442\u043e \u0442\u0430\u043a\u043e\u0435 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f<\/h2>\n<p>\u0424\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u2014 \u044d\u0442\u043e \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u043c\u0435\u0442\u043e\u0434\u044b \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u043e\u0433\u043e, \u0447\u0442\u043e \u043c\u043e\u0434\u0435\u043b\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0437\u0430\u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438, \u0442\u043e \u0435\u0441\u0442\u044c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u043c\u0443 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u044e. \u0421\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0445 \u043f\u043e\u0434\u0445\u043e\u0434\u043e\u0432 \u043a \u043f\u043e\u0441\u0442\u0440\u043e\u0435\u043d\u0438\u044e \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0445 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432 \u0442\u043e\u0433\u043e, \u0447\u0442\u043e \u043c\u043e\u0434\u0435\u043b\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0438\u043b\u0438 \u043d\u0435 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0441\u0432\u043e\u0435\u0439 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438: model checking, \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0439 \u043c\u0435\u0442\u043e\u0434 \u0441 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c \u0441\u0440\u0435\u0434\u0441\u0442\u0432 \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u043b\u0438\u0431\u043e \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c \u0438 \u0434\u0440\u0443\u0433\u0438\u0435.\u00a0<\/p>\n<p>\u041e\u0441\u043d\u043e\u0432\u043d\u043e\u0435 \u043f\u0440\u0435\u0438\u043c\u0443\u0449\u0435\u0441\u0442\u0432\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u044f \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u043c\u0435\u0442\u043e\u0434\u0430 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u043e \u0441\u0440\u0430\u0432\u043d\u0435\u043d\u0438\u044e \u0441 <abbr class=\"habraabbr\" title=\"model checking\" data-title=\"&lt;p>model checking  &lt;\/p>&#187; data-abbr=&#187;\u043f\u0440\u043e\u0432\u0435\u0440\u043a\u043e\u0439 \u043c\u043e\u0434\u0435\u043b\u0435\u0439 &#171;>\u043f\u0440\u043e\u0432\u0435\u0440\u043a\u043e\u0439 \u043c\u043e\u0434\u0435\u043b\u0435\u0439<\/abbr> \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u0443 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u043d\u044b\u0445 \u044f\u0437\u044b\u043a\u043e\u0432 <abbr class=\"habraabbr\" title=\"model checkers\" data-title=\"&lt;p>model checkers&lt;\/p>&#187; data-abbr=&#187;\u0441\u0440\u0435\u0434\u0441\u0442\u0432 \u0442\u0430\u043a\u043e\u0439 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438&#187;>\u0441\u0440\u0435\u0434\u0441\u0442\u0432 \u0442\u0430\u043a\u043e\u0439 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438<\/abbr> \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u044b\u0439 \u043d\u0430\u0431\u043e\u0440 \u043e\u043f\u0435\u0440\u0430\u0442\u043e\u0440\u043e\u0432. \u041e\u043d\u0438 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0442 \u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043b\u0438\u0448\u044c \u043d\u0435\u0431\u043e\u043b\u044c\u0448\u043e\u0435 \u043f\u043e\u0434\u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u044f\u0437\u044b\u043a\u0430, \u043d\u0430 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u043d\u0430\u043f\u0438\u0441\u0430\u043d \u0438\u0441\u0445\u043e\u0434\u043d\u044b\u0439 \u043a\u043e\u0434. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0432 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u0441\u043b\u0443\u0447\u0430\u044f\u0445 \u043c\u043e\u0434\u0435\u043b\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0442\u0440\u0430\u043d\u0441\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u0430 \u0432 \u044f\u0437\u044b\u043a, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0439 \u0432 \u0441\u0440\u0435\u0434\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c, \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u044b\u043c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u043c \u041f\u041e.<\/p>\n<p>\u0410\u043a\u0442\u0443\u0430\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u043f\u043e\u043f\u0443\u043b\u044f\u0440\u043d\u044b\u0435 \u0441\u0435\u0439\u0447\u0430\u0441 \u043f\u043e\u0434\u0445\u043e\u0434\u044b, \u0441\u0432\u044f\u0437\u0430\u043d\u043d\u044b\u0435 \u0441 \u0430\u0443\u0434\u0438\u0442\u043e\u043c \u0438 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435\u043c \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432, \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0442 \u043e\u0431\u043d\u0430\u0440\u0443\u0436\u0438\u0442\u044c \u043e\u0448\u0438\u0431\u043a\u0438, \u043d\u043e \u043d\u0435 \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u044e\u0442 \u0438\u0445 \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0438\u0435. \u0424\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0435 \u043c\u0435\u0442\u043e\u0434\u044b \u0436\u0435 \u043c\u043e\u0433\u0443\u0442 \u043f\u043e\u043c\u043e\u0447\u044c \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0441\u0442\u0440\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b.<\/p>\n<h2>\u0421\u0440\u0435\u0434\u044b \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430<\/h2>\n<p>\u0414\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u041f\u041e \u043e\u0431\u044b\u0447\u043d\u043e \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u0442\u0441\u044f \u0432 \u0441\u0440\u0435\u0434\u0430\u0445 \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0438\u043b\u0438 \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c (\u0442\u0430\u043a\u0436\u0435 \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u043c\u044b\u0445 proof assistants). \u0412 \u0441\u0440\u0435\u0434\u0430\u0445 \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 (Why3, PVS, Z3 \u0438 \u0434\u0440\u0443\u0433\u0438\u0445) \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 (\u0438\u043b\u0438 \u043a\u043e\u043d\u0442\u0440\u043f\u0440\u0438\u043c\u0435\u0440\u044b) \u0433\u0435\u043d\u0435\u0440\u0438\u0440\u0443\u044e\u0442\u0441\u044f \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e SAT- \u0438 SMT-\u0440\u0435\u0448\u0430\u0442\u0435\u043b\u0435\u0439, \u0430 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c \u043d\u0435 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u043d\u0435\u043f\u043e\u0441\u0440\u0435\u0434\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0433\u043e \u0443\u0447\u0430\u0441\u0442\u0438\u044f \u0432 \u0434\u0435\u0434\u0443\u043a\u0446\u0438\u0438. \u041e\u0441\u043d\u043e\u0432\u043d\u043e\u0439 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u043e\u0439 \u0442\u0430\u043a\u043e\u0433\u043e \u043c\u0435\u0442\u043e\u0434\u0430 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u043e\u0441\u0442\u044c \u043a\u043b\u0430\u0441\u0441\u0430 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u0439, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043c\u043e\u0433\u0443\u0442 \u0431\u044b\u0442\u044c \u0434\u043e\u043a\u0430\u0437\u0430\u043d\u044b \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0432 \u0441\u043b\u0443\u0447\u0430\u0435 \u043d\u0435\u0443\u0434\u0430\u0447\u0438 \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0437\u0430\u0447\u0430\u0441\u0442\u0443\u044e \u0442\u0440\u0443\u0434\u043d\u043e \u043f\u043e\u043d\u044f\u0442\u044c, \u0447\u0442\u043e \u043f\u043e\u0448\u043b\u043e \u043d\u0435 \u0442\u0430\u043a \u0438 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043b\u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u0434\u043e\u043a\u0430\u0437\u0443\u0435\u043c\u044b\u043c \u0432 \u043f\u0440\u0438\u043d\u0446\u0438\u043f\u0435.<\/p>\n<p>\u0427\u0442\u043e \u043a\u0430\u0441\u0430\u0435\u0442\u0441\u044f \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u044b\u0445 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432 \u0432 proof assistants (\u043d\u0430\u0438\u0431\u043e\u043b\u0435\u0435 \u043f\u043e\u043f\u0443\u043b\u044f\u0440\u043d\u044b\u043c\u0438 \u0438\u0437 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f Coq, Lean, Isabelle \u0438 \u0441\u0435\u043c\u0435\u0439\u0441\u0442\u0432\u043e HOL), \u0442\u043e \u0442\u0430\u043a\u0438\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0432\u044b\u0440\u0430\u0431\u0430\u0442\u044b\u0432\u0430\u044e\u0442\u0441\u044f \u0432 \u043f\u0440\u043e\u0446\u0435\u0441\u0441\u0435 \u0432\u0437\u0430\u0438\u043c\u043e\u0434\u0435\u0439\u0441\u0442\u0432\u0438\u044f \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430 \u0441 \u043a\u043e\u043c\u043f\u044c\u044e\u0442\u0435\u0440\u043e\u043c (\u0437\u0430\u0447\u0430\u0441\u0442\u0443\u044e \u0447\u0435\u0440\u0435\u0437 IDE). \u041c\u0435\u0436\u0434\u0443 \u0441\u043e\u0431\u043e\u0439 \u0441\u0440\u0435\u0434\u044b \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0440\u0430\u0437\u043b\u0438\u0447\u0430\u044e\u0442\u0441\u044f \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u043c \u0432 \u043d\u0438\u0445 \u044f\u0437\u044b\u043a\u043e\u043c (\u043e\u0431\u044b\u0447\u043d\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u044b\u043c), \u0441\u0442\u0435\u043f\u0435\u043d\u044c\u044e \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0437\u0430\u0446\u0438\u0438, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c \u0438\u043b\u0438 \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0438\u0435\u043c \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432.<\/p>\n<h2>Coq  <\/h2>\n<p>\u0420\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0435\u043c\u044b\u0439 \u0432 \u044d\u0442\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d \u0432 Coq. \u042d\u0442\u043e \u0441\u0440\u0435\u0434\u0430 \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0449\u0430\u044f Gallina \u2014 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e-\u0442\u0438\u043f\u0438\u0437\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u044b\u0439 \u044f\u0437\u044b\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f, \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0449\u0438\u0439 \u0432\u044b\u0440\u0430\u0436\u0430\u0442\u044c \u043a\u0430\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b, \u0442\u0430\u043a \u0438 \u0438\u0445 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430. \u0412 Coq \u0442\u0430\u043a\u0436\u0435 \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u0430 \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0437\u0430\u0446\u0438\u044f \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432 \u0447\u0435\u0440\u0435\u0437 \u0442\u0430\u043a\u0442\u0438\u043a\u0438 \u0438 \u043c\u0435\u0442\u0430\u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0441 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c MetaCoq. \u0412 \u0438\u043d\u0434\u0443\u0441\u0442\u0440\u0438\u0438 Coq \u0431\u044b\u043b \u0443\u0441\u043f\u0435\u0448\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d \u0432 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0435\u043a\u0442\u0430\u0445, \u0432 \u0442\u043e\u043c \u0447\u0438\u0441\u043b\u0435:<\/p>\n<ul>\n<li>\n<p>\u0434\u043b\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 JavaCard;\u00a0<\/p>\n<\/li>\n<li>\n<p>\u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u0433\u043e \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0442\u043e\u0440\u0430 CompCert \u0434\u043b\u044f C;<\/p>\n<\/li>\n<li>\n<p>\u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c\u044b \u043e \u0447\u0435\u0442\u044b\u0440\u0435\u0445 \u043a\u0440\u0430\u0441\u043a\u0430\u0445 \u0438 \u0442\u0435\u043e\u0440\u0435\u043c\u044b \u0424\u0435\u0439\u0442\u0430 \u2014 \u0422\u043e\u043c\u043f\u0441\u043e\u043d\u0430;<\/p>\n<\/li>\n<li>\n<p>\u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0432 \u043f\u0440\u043e\u0435\u043a\u0442\u0435 <a href=\"https:\/\/pruvendo.com\/\">Pruvendo<\/a> \u0438 \u0432 \u043f\u0440\u043e\u0435\u043a\u0442\u0430\u0445 <a href=\"https:\/\/formal.land\/\">Formal Land<\/a> (\u0434\u043b\u044f \u043d\u0435\u0435 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442 \u0442\u0430\u043a\u0436\u0435 \u0438 ConCert).<\/p>\n<\/li>\n<\/ul>\n<h2>\u0424\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a ConCert<\/h2>\n<h3>\u0410\u0440\u0445\u0438\u0442\u0435\u043a\u0442\u0443\u0440\u0430<\/h3>\n<p>\u0424\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u0431\u043e\u0439 \u0441\u043e\u0432\u043e\u043a\u0443\u043f\u043d\u043e\u0441\u0442\u044c \u043c\u043e\u0434\u0435\u043b\u0438 \u0441\u0440\u0435\u0434\u044b \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0432 Coq, \u0430 \u0442\u0430\u043a\u0436\u0435 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u043e\u0432 \u0434\u043b\u044f \u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0438 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0438 \u043a\u043e\u0434\u043e\u0433\u0435\u043d\u0435\u0440\u0430\u0446\u0438\u0438. ConCert \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0434\u0432\u0430 \u043f\u043e\u0434\u0445\u043e\u0434\u0430 \u0434\u043b\u044f \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u043a\u0438 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u044b\u0445 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432: \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u043a\u0430\u043a \u0441\u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u0438\u0441\u0445\u043e\u0434\u043d\u043e\u0433\u043e \u043a\u043e\u0434\u0430 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 \u0432 ConCert, \u0442\u0430\u043a \u0438 \u0438\u0437\u0432\u043b\u0435\u0447\u044c \u043a\u043e\u0434 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u0433\u043e \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0438\u0437 Coq.<\/p>\n<p>\u0421\u043d\u0430\u0447\u0430\u043b\u0430 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u044e\u0442\u0441\u044f \u043d\u0430 \u044f\u0437\u044b\u043a\u0435 Gallina. \u042d\u0442\u043e \u043e\u0431\u044b\u0447\u043d\u044b\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043f\u0440\u0435\u0434\u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0435 \u043f\u0440\u0438\u043c\u0438\u0442\u0438\u0432\u044b \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430, \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u043c\u044b\u0435 \u0438\u043d\u0444\u0440\u0430\u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u043e\u0439 ConCert. \u0417\u0430\u0442\u0435\u043c \u043f\u0438\u0448\u0435\u0442\u0441\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0438 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0438\u043d\u0442\u0435\u0433\u0440\u0430\u0446\u0438\u0438<a href=\"https:\/\/github.com\/QuickChick\/QuickChick\"> QuickChick<\/a> \u043f\u043e\u043b\u0443\u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0442\u0435\u0441\u0442\u0438\u0440\u0443\u044e\u0442\u0441\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u043f\u043e \u043d\u0435\u0439. \u0411\u043e\u043b\u0435\u0435 \u0442\u043e\u0433\u043e, \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0438\u043d\u0444\u0440\u0430\u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u044b ConCert. \u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442 \u043c\u043e\u0434\u0435\u043b\u044c \u0441\u0440\u0435\u0434\u044b \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0434\u043b\u044f \u0440\u0430\u0441\u0441\u0443\u0436\u0434\u0435\u043d\u0438\u0439 \u043e \u0432\u0437\u0430\u0438\u043c\u043e\u0434\u0435\u0439\u0441\u0442\u0432\u0443\u044e\u0449\u0438\u0445 \u043c\u0435\u0436\u0434\u0443 \u0441\u043e\u0431\u043e\u0439 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430\u0445. \u042d\u0442\u043e \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430, \u0432\u044b\u0445\u043e\u0434\u044f\u0449\u0438\u0435 \u0437\u0430 \u0440\u0430\u043c\u043a\u0438 \u043f\u0440\u043e\u0441\u0442\u043e\u0439 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u043e\u0442\u0434\u0435\u043b\u044c\u043d\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430.<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w1560\/getpro\/habr\/upload_files\/f6a\/df6\/e86\/f6adf6e86d628d4a5f02cf372527c1df.png\" alt=\"\u0420\u0438\u0441 1. \u0410\u0440\u0445\u0438\u0442\u0435\u043a\u0442\u0443\u0440\u0430 ConCert  \" title=\"\u0420\u0438\u0441 1. \u0410\u0440\u0445\u0438\u0442\u0435\u043a\u0442\u0443\u0440\u0430 ConCert  \" width=\"1215\" height=\"609\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/f6a\/df6\/e86\/f6adf6e86d628d4a5f02cf372527c1df.png\"\/><\/p>\n<div><figcaption><a href=\"https:\/\/arxiv.org\/pdf\/2203.08016.pdf\">\u0420\u0438\u0441 1. \u0410\u0440\u0445\u0438\u0442\u0435\u043a\u0442\u0443\u0440\u0430 ConCert<\/a>  <\/figcaption><\/div>\n<\/figure>\n<p>\u041f\u043e\u0441\u043b\u0435 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043c\u043e\u0436\u043d\u043e \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0438\u0437\u0432\u043b\u0435\u0447\u0435\u043d\u0438\u044f \u043a\u043e\u0434\u0430 \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u0438\u0441\u043f\u043e\u043b\u043d\u044f\u0435\u043c\u0443\u044e \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044e \u043d\u0430 \u043e\u0434\u043d\u043e\u043c \u0438\u0437 \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u0438\u0432\u0430\u0435\u043c\u044b\u0445 \u044f\u0437\u044b\u043a\u043e\u0432 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432. \u0414\u043b\u044f \u044d\u0442\u043e\u0433\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442\u0441\u044f \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u044b MetaCoq \u0441 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u043c\u0438 \u043e\u043f\u0442\u0438\u043c\u0438\u0437\u0430\u0446\u0438\u044f\u043c\u0438 \u0438 \u043f\u0440\u0435\u0434\u0432\u0430\u0440\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u043e\u0431\u0440\u0430\u0431\u043e\u0442\u043a\u043e\u0439 \u0432 ConCert. \u042d\u0442\u043e \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0438\u0432\u0430\u0435\u0442 \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u0443 \u043a\u043e\u0434\u043e\u0433\u0435\u043d\u0435\u0440\u0430\u0446\u0438\u0438 \u0441 \u0441\u0438\u043b\u044c\u043d\u044b\u043c\u0438 \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u044f\u043c\u0438 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438.<\/p>\n<h3>\u041d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0441\u043e\u0432\u0435\u0442\u043e\u0432 \u043f\u043e \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u0435<\/h3>\n<p>ConCert \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d \u0432 Coq 8.17 \u0438 \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442 MetaCoq \u0438 std++. \u0414\u043b\u044f \u0440\u0430\u0431\u043e\u0442\u044b \u0441 \u0442\u0435\u0441\u0442\u0430\u043c\u0438 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u0430 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 QuickChick. \u0412\u0441\u0435 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0441\u0442\u0438 \u043c\u043e\u0436\u043d\u043e \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u0438\u0442\u044c \u0447\u0435\u0440\u0435\u0437 opam, \u043c\u0435\u043d\u0435\u0434\u0436\u0435\u0440\u0430 \u043f\u0430\u043a\u0435\u0442\u043e\u0432 OCaml:<\/p>\n<p><code>sudo apt install opam<br \/>opam switch create . 4.10.2 --repositories default,coq-released=https:\/\/coq.inria.fr\/opam\/released<br \/> eval $(opam env)<\/code><\/p>\n<p>\u0423\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u0430 ConCert \u0438 \u0435\u0433\u043e \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0441\u0442\u0435\u0439:<\/p>\n<p><code>git clone https:\/\/github.com\/AU-COBRA\/ConCert.git<br \/>cd ConCert<br \/>opam install .\/coq-concert.opam<\/code><\/p>\n<p>\u0421\u0431\u043e\u0440\u043a\u0430 \u043f\u0440\u0438\u043c\u0435\u0440\u043e\u0432 \u0438\u0437 \u0440\u0435\u043f\u043e\u0437\u0438\u0442\u043e\u0440\u0438\u044f:<\/p>\n<p><code>git clone https:\/\/github.com\/AU-COBRA\/ConCert.git<br \/>cd ConCert<br \/> opam install .\/coq-concert.opam --with-test<\/code><\/p>\n<h3>\u041c\u043e\u0434\u0435\u043b\u044c \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0438 \u0441\u0440\u0435\u0434\u044b \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f<\/h3>\n<p>\u041c\u043e\u0434\u0435\u043b\u044c \u0441\u0440\u0435\u0434\u044b \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u043e\u0431\u043b\u0435\u0433\u0447\u0430\u0435\u0442 \u0440\u0430\u0441\u0441\u0443\u0436\u0434\u0435\u043d\u0438\u044f \u043e \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0430\u0445 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u0432\u044b\u0437\u043e\u0432\u043e\u0432 (\u0442\u0440\u0430\u0441\u0441\u044b) \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432. \u0421\u0430\u043c \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 \u0432 \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043a\u0430\u043a \u043f\u0430\u0440\u0430 \u0444\u0443\u043d\u043a\u0446\u0438\u0439: <code>init<\/code> \u0438 <code>receive<\/code>.\u00a0<\/p>\n<pre><code>init : Chain -> ContractCallContext -> Setup -> option State<\/code><\/pre>\n<p>\u0424\u0443\u043d\u043a\u0446\u0438\u044f <code>init<\/code> \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u043f\u0440\u0438 \u0440\u0430\u0437\u0432\u0435\u0440\u0442\u044b\u0432\u0430\u043d\u0438\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0434\u043b\u044f \u0442\u043e\u0433\u043e, \u0447\u0442\u043e\u0431\u044b \u0437\u0430\u0434\u0430\u0442\u044c \u0435\u0433\u043e \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435. \u041f\u0435\u0440\u0432\u044b\u0439 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440 \u0442\u0438\u043f\u0430 <code>Chain<\/code> \u043f\u0435\u0440\u0435\u0434\u0430\u0435\u0442 \u0434\u0430\u043d\u043d\u044b\u0435 \u043e \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0435: \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u0431\u043b\u043e\u043a\u043e\u0432 \u0438 \u043e\u0442\u043e\u0431\u0440\u0430\u0436\u0435\u043d\u0438\u0435 \u0438\u0437 \u0430\u0434\u0440\u0435\u0441\u043e\u0432 \u0432 \u0438\u0445 \u0431\u0430\u043b\u0430\u043d\u0441\u044b. \u041f\u0430\u0440\u0430\u043c\u0435\u0442\u0440 <code>ContractCallContext<\/code> \u043f\u0435\u0440\u0435\u0434\u0430\u0435\u0442 \u0434\u0430\u043d\u043d\u044b\u0435 \u043e \u0442\u0435\u043a\u0443\u0449\u0435\u043c \u0432\u044b\u0437\u043e\u0432\u0435: \u0430\u0434\u0440\u0435\u0441\u0430 \u0432\u044b\u0437\u044b\u0432\u0430\u044e\u0449\u0435\u0433\u043e \u0438 \u0432\u044b\u0437\u044b\u0432\u0430\u0435\u043c\u043e\u0433\u043e \u0438 \u0441\u0443\u043c\u043c\u0443, \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0443\u044e \u0432 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442. <code>Setup<\/code> \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u0431\u043e\u0439 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u044b \u0438\u043d\u0438\u0446\u0438\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438.<\/p>\n<pre><code>receive : Chain -> ContractCallContext -> State -> option Msg -> option (State \u2217 list ActionBody)  <\/code><\/pre>\n<p>\u0424\u0443\u043d\u043a\u0446\u0438\u044f <code>receive<\/code> \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u0434\u043b\u044f \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u0438\u0445 \u0432\u044b\u0437\u043e\u0432\u043e\u0432 \u0438 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u043f\u0440\u0438 \u043a\u0430\u0436\u0434\u043e\u043c \u043e\u0431\u0440\u0430\u0449\u0435\u043d\u0438\u0438 \u043a \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0443. <code>State<\/code> \u2014 \u044d\u0442\u043e \u0442\u0435\u043a\u0443\u0449\u0435\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430. <code>Msg<\/code> \u2014 \u044d\u0442\u043e \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0435\u043c\u044b\u0439 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u0435\u043c \u0442\u0438\u043f \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 (\u0435\u0433\u043e \u0442\u043e\u0447\u043a\u0438 \u0432\u0445\u043e\u0434\u0430). \u0420\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u043e\u043c \u0443\u0441\u043f\u0435\u0448\u043d\u043e\u0433\u043e \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043d\u043e\u0432\u043e\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0438 \u0441\u043f\u0438\u0441\u043e\u043a \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439, \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u043d\u044b\u0439 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0442\u0438\u043f\u0430 <code>ActionBody<\/code>. \u0414\u0435\u0439\u0441\u0442\u0432\u0438\u044f \u043c\u043e\u0433\u0443\u0442 \u0431\u044b\u0442\u044c \u043f\u0435\u0440\u0435\u0432\u043e\u0434\u0430\u043c\u0438 \u0441\u0440\u0435\u0434\u0441\u0442\u0432, \u0432\u044b\u0437\u043e\u0432\u0430\u043c\u0438 \u0434\u0440\u0443\u0433\u0438\u0445 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0438 \u0440\u0430\u0437\u0432\u0435\u0440\u0442\u044b\u0432\u0430\u043d\u0438\u044f\u043c\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432.<\/p>\n<p>\u0422\u0438\u043f <code>Chain<\/code> \u043d\u0435 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u0438, \u0447\u0442\u043e\u0431\u044b \u0441\u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439 \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0435. \u041d\u0430\u043c \u043d\u0443\u0436\u043d\u043e \u0438\u043c\u0435\u0442\u044c \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u043e\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0442\u044c \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044e \u043e \u0442\u0435\u043a\u0443\u0449\u0438\u0445 \u0440\u0430\u0437\u0432\u0435\u0440\u043d\u0443\u0442\u044b\u0445 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430\u0445, \u0430 \u0442\u043e\u0447\u043d\u0435\u0435, \u043e\u0431 \u0438\u0445 \u0444\u0443\u043d\u043a\u0446\u0438\u044f\u0445 \u0438 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f\u0445. \u0414\u043b\u044f \u044d\u0442\u043e\u0433\u043e \u0432\u0432\u043e\u0434\u0438\u0442\u0441\u044f \u0442\u0438\u043f <code>Environment<\/code>, \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u044e\u0449\u0438\u0439 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0432\u0441\u0435\u0433\u043e \u043e\u043a\u0440\u0443\u0436\u0435\u043d\u0438\u044f:<\/p>\n<pre><code>Record Environment :=     { env_chain :> Chain;       env_contracts : Address -> option WeakContract;       env_contract_states : Address -> option SerializedValue; }.<\/code><\/pre>\n<p>\u0421\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u043e\u043a\u0440\u0443\u0436\u0435\u043d\u0438\u044f \u0438\u0437\u043c\u0435\u043d\u044f\u0435\u0442\u0441\u044f \u0432 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u044e\u0442\u0441\u044f \u0432 ConCert \u0442\u0438\u043f\u043e\u043c <code>Action<\/code>:<\/p>\n<pre><code>Record Action := { act_from : Address; act_body : ActionBody; }.<\/code><\/pre>\n<p>\u041a\u043e\u0433\u0434\u0430 <code>receive<\/code> \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u043d\u043e\u0432\u044b\u0439 \u0441\u043f\u0438\u0441\u043e\u043a \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439, \u0441\u0440\u0435\u0434\u0430 \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0434\u043e\u043b\u0436\u043d\u0430 \u0431\u0443\u0434\u0435\u0442 \u043e\u0446\u0435\u043d\u0438\u0442\u044c \u0438\u0445 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442. \u042d\u0442\u0430 \u043e\u0446\u0435\u043d\u043a\u0430 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0435\u0442\u0441\u044f \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043e\u0442\u043d\u043e\u0448\u0435\u043d\u0438\u044f <code>ActionEvaluation<\/code> \u0432 Coq \u0441 \u0442\u0438\u043f\u043e\u043c <code>Environment -> Action-> Environment -> list Action -> Type<\/code>. \u041e\u043d\u043e \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u0432 \u0441\u0435\u0431\u0435 \u0442\u0440\u0435\u0431\u043e\u0432\u0430\u043d\u0438\u044f \u0434\u043b\u044f \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0438 \u0432 \u043e\u043a\u0440\u0443\u0436\u0435\u043d\u0438\u0438 \u0438 \u0435\u0435 \u043f\u043e\u0441\u043b\u0435\u0434\u0441\u0442\u0432\u0438\u044f.<\/p>\n<p>\u0418 <code>receive<\/code>, \u0438 <code>init<\/code> \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u043e\u0431\u044b\u0447\u043d\u044b\u043c\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u044f\u043c\u0438 Coq, \u0447\u0442\u043e \u0434\u0435\u043b\u0430\u0435\u0442 \u0438\u0445 \u0443\u0434\u043e\u0431\u043d\u044b\u043c\u0438 \u0434\u043b\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438. \u041e\u0434\u043d\u0430\u043a\u043e \u043f\u0440\u043e\u0441\u0442\u043e \u0440\u0430\u0441\u0441\u0443\u0436\u0434\u0435\u043d\u0438\u044f \u043e \u0444\u0443\u043d\u043a\u0446\u0438\u044f\u0445 \u043e\u0442\u0434\u0435\u043b\u044c\u043d\u043e\u0433\u043e \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0437\u0430\u0447\u0430\u0441\u0442\u0443\u044e \u043d\u0435\u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e, \u043f\u043e\u0441\u043a\u043e\u043b\u044c\u043a\u0443 \u043c\u043d\u043e\u0433\u0438\u0435 \u0440\u0430\u0437\u0432\u0435\u0440\u043d\u0443\u0442\u044b\u0435 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u044b \u043f\u043e\u0434\u0440\u0430\u0437\u0443\u043c\u0435\u0432\u0430\u044e\u0442 \u0432\u0437\u0430\u0438\u043c\u043e\u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0435 \u0441 \u0434\u0440\u0443\u0433\u0438\u043c\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430\u043c\u0438. \u041e\u0434\u0438\u043d \u0432\u044b\u0437\u043e\u0432 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <code>receive<\/code> \u043f\u043e\u0442\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u043e \u043f\u043e\u0440\u043e\u0436\u0434\u0430\u0435\u0442 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0432\u044b\u0437\u043e\u0432\u043e\u0432, \u0430 \u044d\u0442\u043e \u043c\u043e\u0436\u0435\u0442 \u0441\u043e\u0437\u0434\u0430\u0432\u0430\u0442\u044c \u0441\u043b\u043e\u0436\u043d\u044b\u0435 \u0433\u0440\u0430\u0444\u044b \u0432\u044b\u0437\u043e\u0432\u043e\u0432 \u043c\u0435\u0436\u0434\u0443 \u0440\u0430\u0437\u0432\u0435\u0440\u043d\u0443\u0442\u044b\u043c\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430\u043c\u0438. \u041f\u043e\u044d\u0442\u043e\u043c\u0443 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0442\u044c \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0432\u044b\u0437\u043e\u0432\u043e\u0432 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f. \u0422\u0440\u0430\u0441\u0441\u0430 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f <code>ChainTrace<\/code> \u2014 \u044d\u0442\u043e \u0440\u0435\u0444\u043b\u0435\u043a\u0441\u0438\u0432\u043d\u043e\u0435, \u0442\u0440\u0430\u043d\u0437\u0438\u0442\u0438\u0432\u043d\u043e\u0435 \u0437\u0430\u043c\u044b\u043a\u0430\u043d\u0438\u0435 \u043e\u0442\u043d\u043e\u0448\u0435\u043d\u0438\u044f ChainStep, \u043a\u043e\u0442\u043e\u0440\u043e\u0435, \u043f\u043e \u0441\u0443\u0442\u0438, \u043e\u0442\u0440\u0430\u0436\u0430\u0435\u0442 \u0434\u043e\u0431\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u0431\u043b\u043e\u043a\u0430 \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d, \u0430 \u0432 ConCert \u0438\u043c\u0435\u0435\u0442 \u0442\u0438\u043f<code>ChainState -> ChainState -> Type<\/code>, \u0433\u0434\u0435:\u00a0<\/p>\n<pre><code>Record ChainState := { chain_state_env :> Environment;                        chain_state_queue : list Action; }<\/code><\/pre>\n<h3>\u0422\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432<\/h3>\n<p><abbr class=\"habraabbr\" title=\"PBT, \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\" data-title=\"&lt;p>PBT, \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432&lt;\/p>&#187; data-abbr=&#187;Property-based testing&#187;>Property-based testing<\/abbr> \u2014 \u044d\u0442\u043e \u0442\u0435\u0445\u043d\u0438\u043a\u0430 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u0434\u0430\u043d\u043d\u044b\u0435 \u0433\u0435\u043d\u0435\u0440\u0438\u0440\u0443\u044e\u0442\u0441\u044f \u043f\u0441\u0435\u0432\u0434\u043e\u0441\u043b\u0443\u0447\u0430\u0439\u043d\u044b\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c \u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u044e\u0442\u0441\u044f \u043d\u0430 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0438\u0435 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u043c\u0443 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0443. \u0412 ConCert \u0438\u043d\u0442\u0435\u0433\u0440\u0438\u0440\u043e\u0432\u0430\u043d\u0430 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 PBT QuickChick, \u0431\u043b\u0430\u0433\u043e\u0434\u0430\u0440\u044f \u044d\u0442\u043e\u043c\u0443 \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u0438\u0432\u0430\u0435\u0442\u0441\u044f \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u043e\u0439 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432, \u0430 \u0442\u0430\u043a\u0436\u0435 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432 \u0442\u0440\u0430\u0441\u0441 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f. \u041e\u0431\u0437\u043e\u0440 \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a\u0430 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u043f\u0440\u0438\u0432\u0435\u0434\u0435\u043d \u043d\u0430 \u0440\u0438\u0441\u0443\u043d\u043a\u0435.<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w1560\/getpro\/habr\/upload_files\/7bf\/d5b\/34e\/7bfd5b34edacd918f2f27e0cc33766b3.png\" alt=\"\u0420\u0438\u0441 2. \u0421\u0445\u0435\u043c\u0430 PBT ConCert  \" title=\"\u0420\u0438\u0441 2. \u0421\u0445\u0435\u043c\u0430 PBT ConCert  \" width=\"843\" height=\"814\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/7bf\/d5b\/34e\/7bfd5b34edacd918f2f27e0cc33766b3.png\"\/><\/p>\n<div><figcaption><a href=\"https:\/\/arxiv.org\/pdf\/2208.00758.pdf\">\u0420\u0438\u0441 2. \u0421\u0445\u0435\u043c\u0430 PBT ConCert<\/a>  <\/figcaption><\/div>\n<\/figure>\n<p>\u0415\u0441\u043b\u0438 \u043a\u0440\u0430\u0442\u043a\u043e, \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a PBT \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c. \u041f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c \u043f\u0438\u0448\u0435\u0442 \u0433\u0435\u043d\u0435\u0440\u0430\u0442\u043e\u0440\u044b \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439 \u0442\u0435\u0441\u0442\u0438\u0440\u0443\u0435\u043c\u044b\u0445 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432. \u0413\u0435\u043d\u0435\u0440\u0430\u0442\u043e\u0440\u044b \u2014 \u044d\u0442\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0441\u043e\u0437\u0434\u0430\u044e\u0442 \u043f\u0441\u0435\u0432\u0434\u043e\u0441\u043b\u0443\u0447\u0430\u0439\u043d\u044b\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0437\u0430\u0434\u0430\u043d\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430. \u0420\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u043d\u044b\u0435 \u0433\u0435\u043d\u0435\u0440\u0430\u0442\u043e\u0440\u044b \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442\u0441\u044f \u0434\u043b\u044f \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0441\u043b\u0443\u0447\u0430\u0439\u043d\u044b\u0445 \u0442\u0440\u0430\u0441\u0441 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0441 \u043f\u0441\u0435\u0432\u0434\u043e\u0441\u043b\u0443\u0447\u0430\u0439\u043d\u044b\u043c\u0438 \u0432\u044b\u0437\u043e\u0432\u0430\u043c\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432. \u041f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c \u0442\u0430\u043a\u0436\u0435 \u043d\u0430\u0441\u0442\u0440\u0430\u0438\u0432\u0430\u0435\u0442 \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u0443\u044e \u043a\u043e\u043d\u0444\u0438\u0433\u0443\u0440\u0430\u0446\u0438\u044e \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430, \u0441\u043e\u0441\u0442\u043e\u044f\u0449\u0443\u044e \u0438\u0437 \u0431\u0430\u043b\u0430\u043d\u0441\u043e\u0432 \u0430\u0434\u0440\u0435\u0441\u043e\u0432 \u0438 \u0440\u0430\u0437\u0432\u0435\u0440\u043d\u0443\u0442\u044b\u0445 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432.\u00a0<\/p>\n<p>\u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043f\u0440\u0438\u043c\u0435\u0440 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0442\u043e\u043a\u0435\u043d\u0430 \u0441 \u0442\u0438\u043f\u043e\u043c \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0445 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439:<\/p>\n<pre><code>Inductive Msg :=     transfer of (address * address * nat)   | approve of (address * address * nat).<\/code><\/pre>\n<p>\u0422\u043e \u0435\u0441\u0442\u044c \u0443 \u043d\u0435\u0433\u043e \u0435\u0441\u0442\u044c \u0434\u0432\u0435 \u0442\u043e\u0447\u043a\u0438 \u0432\u0445\u043e\u0434\u0430: \u043e\u0434\u043d\u0430 \u0434\u043b\u044f \u043f\u0435\u0440\u0435\u0434\u0430\u0447\u0438 \u0442\u043e\u043a\u0435\u043d\u043e\u0432 \u043c\u0435\u0436\u0434\u0443 \u0434\u0432\u0443\u043c\u044f \u0437\u0430\u0434\u0430\u043d\u043d\u044b\u043c\u0438 \u0430\u0434\u0440\u0435\u0441\u0430\u043c\u0438 \u0438 \u043e\u0434\u043d\u0430 \u0434\u043b\u044f \u043e\u0434\u043e\u0431\u0440\u0435\u043d\u0438\u044f \u0430\u0434\u0440\u0435\u0441\u0430 \u043d\u0430 \u0440\u0430\u0441\u0445\u043e\u0434\u043e\u0432\u0430\u043d\u0438\u0435 \u0437\u0430\u0434\u0430\u043d\u043d\u043e\u0433\u043e \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u0430 \u0442\u043e\u043a\u0435\u043d\u043e\u0432 \u043e\u0442 \u0438\u043c\u0435\u043d\u0438 \u0434\u0440\u0443\u0433\u043e\u0433\u043e \u0430\u0434\u0440\u0435\u0441\u0430. \u0413\u0435\u043d\u0435\u0440\u0430\u0446\u0438\u044f \u043f\u0441\u0435\u0432\u0434\u043e\u0441\u043b\u0443\u0447\u0430\u0439\u043d\u044b\u0445 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 <code>Msg<\/code> \u0442\u043e\u0433\u0434\u0430 \u0441\u0432\u043e\u0434\u0438\u0442\u0441\u044f \u043a \u0433\u0435\u043d\u0435\u0440\u0430\u0446\u0438\u0438 <code>transfer<\/code> \u0438\u043b\u0438 <code>approve<\/code> \u0438 \u0438\u0445 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u043e\u0432 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0433\u0435\u043d\u0435\u0440\u0430\u0442\u043e\u0440\u043e\u0432 \u0434\u043b\u044f <code>address<\/code> \u0438 <code>nat<\/code>.\u00a0<\/p>\n<p>\u041f\u0440\u0435\u0434\u043f\u043e\u043b\u043e\u0436\u0438\u043c, \u043c\u044b \u0445\u043e\u0442\u0438\u043c \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c, \u0447\u0442\u043e transfer \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e \u043e\u0431\u043d\u043e\u0432\u043b\u044f\u0435\u0442 \u0432\u043d\u0443\u0442\u0440\u0435\u043d\u043d\u0438\u0435 \u0431\u0430\u043b\u0430\u043d\u0441\u044b. \u0412 ConCert \u044d\u0442\u043e \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u043e\u0439 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u0437\u0430\u0434\u0430\u0435\u0442\u0441\u044f \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043f\u0440\u0435\u0434- \u0438 \u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u0439. \u0422\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0442\u0430\u043a\u043e\u0433\u043e \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e <code>QuickChick<\/code> \u043c\u043e\u0436\u0435\u0442 \u0432\u044b\u0433\u043b\u044f\u0434\u0435\u0442\u044c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c:<\/p>\n<pre><code>QuickChick ({{msg_is_transfer}} Token.receive {{transfer_correct}}).<\/code><\/pre>\n<p>\u0412\u044b\u0448\u0435 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d \u043a\u043e\u0434 \u0442\u0435\u0441\u0442\u0430, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u043c\u044b \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c, \u0447\u0442\u043e \u0435\u0441\u043b\u0438 \u0432\u0445\u043e\u0434\u044f\u0449\u0435\u0435 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u2014 transfer, \u0442\u043e \u043f\u043e\u0441\u043b\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438 receive \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0442\u043e\u043a\u0435\u043d\u0430, \u0435\u0433\u043e \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0434\u043e\u043b\u0436\u043d\u043e \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u043e\u0432\u0430\u0442\u044c \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442\u0443 <code>transfer_correct<\/code>, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043c\u044b \u043f\u0438\u0448\u0435\u043c \u0432\u0440\u0443\u0447\u043d\u0443\u044e. \u041f\u043e \u0443\u043c\u043e\u043b\u0447\u0430\u043d\u0438\u044e QuickChick \u0441\u0433\u0435\u043d\u0435\u0440\u0438\u0440\u0443\u0435\u0442 10 000 \u0442\u0435\u0441\u0442\u043e\u0432 \u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442, \u0447\u0442\u043e \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u0443\u0434\u043e\u0432\u043b\u0435\u0442\u0432\u043e\u0440\u044f\u0435\u0442\u0441\u044f \u0432\u043e \u0432\u0441\u0435\u0445 \u0438\u0437 \u043d\u0438\u0445, \u0438\u043b\u0438 \u0441\u043e\u043e\u0431\u0449\u0438\u0442 \u043e \u043a\u043e\u043d\u0442\u0440\u043f\u0440\u0438\u043c\u0435\u0440\u0435. \u041f\u043e\u043b\u0443\u0447\u0435\u043d\u043d\u044b\u0435 \u043a\u043e\u043d\u0442\u0440\u043f\u0440\u0438\u043c\u0435\u0440\u044b \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u043c\u0438\u043d\u0438\u043c\u0438\u0437\u0438\u0440\u0443\u044e\u0442\u0441\u044f \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a\u043e\u043c PBT \u0434\u043b\u044f \u0431\u043e\u043b\u0435\u0435 \u043f\u0440\u043e\u0441\u0442\u043e\u0433\u043e \u043f\u043e\u043d\u0438\u043c\u0430\u043d\u0438\u044f. \u0420\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a\u0438 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0430\u044e\u0442, \u0447\u0442\u043e \u044d\u0442\u0438 \u0442\u0435\u0441\u0442\u044b \u043e\u0431\u044b\u0447\u043d\u043e \u0437\u0430\u043d\u0438\u043c\u0430\u044e\u0442 \u043c\u0435\u043d\u044c\u0448\u0435 \u043c\u0438\u043d\u0443\u0442\u044b.<\/p>\n<h3>\u041f\u0440\u0438\u043c\u0435\u0440 \u043f\u0440\u0438\u043c\u0435\u043d\u0435\u043d\u0438\u044f \u0434\u043b\u044f iToken<\/h3>\n<p>\u0420\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a\u0438 ConCert \u043f\u0440\u043e\u0434\u0435\u043c\u043e\u043d\u0441\u0442\u0440\u0438\u0440\u043e\u0432\u0430\u043b\u0438 \u0443\u0436\u0435 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0431\u043e\u043b\u044c\u0448\u043e\u0435 \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u0441\u043b\u0443\u0447\u0430\u0435\u0432 \u0443\u0441\u043f\u0435\u0448\u043d\u043e\u0433\u043e \u043f\u0440\u0438\u043c\u0435\u043d\u0435\u043d\u0438\u044f \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a\u0430 \u0434\u043b\u044f \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432. \u041a \u043f\u0440\u0438\u043c\u0435\u0440\u0443, <a href=\"https:\/\/arxiv.org\/abs\/2208.00758\">\u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e ConCert \u0431\u044b\u043b\u0438 \u043d\u0430\u0439\u0434\u0435\u043d\u044b \u043d\u043e\u0432\u044b\u0435 \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u0438<\/a> \u0432 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0435<a href=\"https:\/\/github.com\/brave-intl\/basic-attention-token-crowdsale\/blob\/66c886cc4bfb0493d9e7980f392ca7921ef1e7fc\/contracts\/BAToken.sol\"> Basic Authentification Token<\/a>, \u0444\u043e\u0440\u043c\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u0430 DAO Attack, \u0441\u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u043d \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 \u043e\u0431\u043c\u0435\u043d\u043d\u0438\u043a\u0430 Dexter \u043d\u0430 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0435 Tezos, \u0432 \u0440\u0430\u043d\u043d\u0435\u0439 \u0432\u0435\u0440\u0441\u0438\u0438 \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u0442\u043e\u0436\u0435 \u0431\u044b\u043b\u0430 \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u044c.<\/p>\n<p>\u041e\u0441\u0442\u0430\u043d\u043e\u0432\u0438\u043c\u0441\u044f \u043f\u043e\u0434\u0440\u043e\u0431\u043d\u0435\u0435 \u043d\u0430 \u043f\u0440\u0438\u043c\u0435\u0440\u0435 \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u0438 \u0432 Solidity-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0435 \u0442\u043e\u043a\u0435\u043d\u0430 iToken, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043b\u0441\u044f \u043d\u0430 \u043f\u043b\u0430\u0442\u0444\u043e\u0440\u043c\u0435 bZx. \u0423\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u044c \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u043b\u0430\u0441\u044c \u0432 \u043d\u0435\u043f\u0440\u0430\u0432\u0438\u043b\u044c\u043d\u043e\u043c \u0440\u0430\u0441\u043f\u043e\u043b\u043e\u0436\u0435\u043d\u0438\u0438 \u0441\u0442\u0440\u043e\u043a \u043a\u043e\u0434\u0430 \u0438 \u0432 \u0441\u0435\u043d\u0442\u044f\u0431\u0440\u0435 2020 \u0433\u043e\u0434\u0430 \u043f\u043e\u0437\u0432\u043e\u043b\u0438\u043b\u0430 \u0430\u0442\u0430\u043a\u0443\u044e\u0449\u0435\u043c\u0443 \u0443\u043a\u0440\u0430\u0441\u0442\u044c 8 \u043c\u043b\u043d \u0434\u043e\u043b\u043b\u0430\u0440\u043e\u0432.<a href=\"https:\/\/web.archive.org\/web\/20201003015650\/https:\/\/bzx.network\/blog\/incident\"> <\/a><\/p>\n<p>\u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043a\u043e\u0434 \u0441 \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u044c\u044e:<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w1560\/getpro\/habr\/upload_files\/cca\/2e9\/819\/cca2e981982f6fdafe45e1018a5c5bc9.png\" alt=\"\u0420\u0438\u0441. 3. \u0423\u044f\u0437\u0432\u0438\u043c\u044b\u0439 \u043a\u043e\u0434\" title=\"\u0420\u0438\u0441. 3. \u0423\u044f\u0437\u0432\u0438\u043c\u044b\u0439 \u043a\u043e\u0434\" width=\"1565\" height=\"346\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/cca\/2e9\/819\/cca2e981982f6fdafe45e1018a5c5bc9.png\"\/><\/p>\n<div><figcaption>\u0420\u0438\u0441. 3. \u0423\u044f\u0437\u0432\u0438\u043c\u044b\u0439 \u043a\u043e\u0434<\/figcaption><\/div>\n<\/figure>\n<p>\u041b\u043e\u0433\u0438\u043a\u0430 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0431\u044b\u043b\u0430 \u0431\u044b \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0439, \u0435\u0441\u043b\u0438 \u043f\u0435\u0440\u0435\u043c\u0435\u0441\u0442\u0438\u0442\u044c \u0441\u0442\u0440\u043e\u043a\u0443 6 \u043f\u043e\u0441\u043b\u0435 \u0441\u0442\u0440\u043e\u043a\u0438 8. \u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0441\u043b\u0443\u0447\u0430\u0439, \u043a\u043e\u0433\u0434\u0430 <code>_from = _to<\/code>. \u0412 \u044d\u0442\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435 \u043f\u0435\u0440\u0435\u0432\u0435\u0434\u0435\u043d\u043d\u0430\u044f \u0441\u0443\u043c\u043c\u0430 \u0431\u0443\u0434\u0435\u0442 \u0432\u044b\u0447\u0442\u0435\u043d\u0430 \u0438\u0437 \u0431\u0430\u043b\u0430\u043d\u0441\u0430 \u043e\u0442\u043f\u0440\u0430\u0432\u0438\u0442\u0435\u043b\u044f \u0432 \u0441\u0442\u0440\u043e\u043a\u0435 8. \u041e\u0434\u043d\u0430\u043a\u043e \u0432 \u0441\u0442\u0440\u043e\u043a\u0435 9 \u0438\u0441\u0445\u043e\u0434\u043d\u044b\u0439 \u0431\u0430\u043b\u0430\u043d\u0441 \u043e\u0442\u043f\u0440\u0430\u0432\u0438\u0442\u0435\u043b\u044f \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u0434\u043b\u044f \u0434\u043e\u0431\u0430\u0432\u043b\u0435\u043d\u0438\u044f \u043f\u0435\u0440\u0435\u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u0443\u043c\u043c\u044b \u043a \u0431\u0430\u043b\u0430\u043d\u0441\u0443 \u043e\u0442\u043f\u0440\u0430\u0432\u0438\u0442\u0435\u043b\u044f, \u0432 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 \u0447\u0435\u0433\u043e \u043e\u0442\u043f\u0440\u0430\u0432\u0438\u0442\u0435\u043b\u044c \u043f\u0435\u0440\u0435\u0432\u043e\u0434\u0438\u0442 \u0441\u0435\u0431\u0435 \u0432\u0441\u0435 \u0442\u043e\u043a\u0435\u043d\u044b.<\/p>\n<p>\u042d\u0442\u0430 \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u044c \u0431\u044b\u043b\u0430 \u0442\u0430\u043a\u0436\u0435 \u043d\u0430\u0439\u0434\u0435\u043d\u0430 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e ConCert. \u041d\u0430 \u0440\u0438\u0441\u0443\u043d\u043a\u0435 \u043c\u044b \u0432\u0438\u0434\u0438\u043c \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044e \u044d\u0442\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0432\u043e \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a\u0435.<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w1560\/getpro\/habr\/upload_files\/a23\/97a\/51b\/a2397a51b356c4d86c566a5164650587.png\" alt=\"\u0420\u0438\u0441 4. \u0420\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438 iToken _internalTransferFrom, \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u0449\u0435\u0439 \u0431\u0430\u0433  \" title=\"\u0420\u0438\u0441 4. \u0420\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438 iToken _internalTransferFrom, \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u0449\u0435\u0439 \u0431\u0430\u0433  \" width=\"1509\" height=\"586\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/a23\/97a\/51b\/a2397a51b356c4d86c566a5164650587.png\"\/><\/p>\n<div><figcaption>\u0420\u0438\u0441 4. \u0420\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <code>iToken _internalTransferFrom<\/code>, \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u0449\u0435\u0439 \u0431\u0430\u0433  <\/figcaption><\/div>\n<\/figure>\n<p>\u042d\u0442\u0443 \u043e\u0448\u0438\u0431\u043a\u0443 \u043c\u043e\u0436\u043d\u043e \u043d\u0430\u0439\u0442\u0438 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a\u0430 PBT, \u043d\u0430\u043f\u0438\u0441\u0430\u0432 \u0442\u0435\u0441\u0442, \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u044e\u0449\u0438\u0439, \u0447\u0442\u043e \u0431\u0430\u043b\u0430\u043d\u0441 \u043e\u0441\u0442\u0430\u0435\u0442\u0441\u044f \u043d\u0435\u0438\u0437\u043c\u0435\u043d\u043d\u044b\u043c \u043f\u043e\u0441\u043b\u0435 \u043f\u0435\u0440\u0435\u0432\u043e\u0434\u0430 \u0441\u0430\u043c\u043e\u043c\u0443 \u0441\u0435\u0431\u0435. \u041e\u0434\u043d\u0430\u043a\u043e \u0442\u0430\u043a\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u0430\u0433\u0430\u0435\u0442, \u0447\u0442\u043e \u043c\u044b \u0437\u043d\u0430\u0435\u043c \u043e \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u043e\u0448\u0438\u0431\u043a\u0438 \u0432 \u044d\u0442\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435. \u0412\u043c\u0435\u0441\u0442\u043e \u044d\u0442\u043e\u0433\u043e \u043c\u043e\u0436\u043d\u043e \u0441\u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0431\u043e\u043b\u0435\u0435 \u043e\u0431\u0449\u0435\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e, \u0441\u043e\u0433\u043b\u0430\u0441\u043d\u043e \u043a\u043e\u0442\u043e\u0440\u043e\u043c\u0443 \u0441\u0443\u043c\u043c\u0430 \u0432\u0441\u0435\u0445 \u0431\u0430\u043b\u0430\u043d\u0441\u043e\u0432 \u0434\u043e\u043b\u0436\u043d\u0430 \u043e\u0441\u0442\u0430\u0432\u0430\u0442\u044c\u0441\u044f \u043d\u0435\u0438\u0437\u043c\u0435\u043d\u043d\u043e\u0439 \u043f\u043e\u0441\u043b\u0435 \u0432\u044b\u0437\u043e\u0432\u0430, \u0437\u0430 \u0438\u0441\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435\u043c \u0432\u044b\u0437\u043e\u0432\u043e\u0432 \u0444\u0443\u043d\u043a\u0446\u0438\u0439 <code>mint<\/code> \u0438 <code>burn<\/code>. \u0412 ConCert \u0442\u0430\u043a\u043e\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u0432\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c:<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w1560\/getpro\/habr\/upload_files\/f84\/eef\/ed4\/f84eefed4af17436887a51c1ca2f09c2.png\" alt=\"\u0420\u0438\u0441 5. \u041f\u0440\u0435\u0434\u0438\u043a\u0430\u0442 \u043e\u0431 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043d\u043e\u0441\u0442\u0438 \u0441\u0443\u043c\u043c\u044b \u0431\u0430\u043b\u0430\u043d\u0441\u043e\u0432 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u0435\u0439 iToken\" title=\"\u0420\u0438\u0441 5. \u041f\u0440\u0435\u0434\u0438\u043a\u0430\u0442 \u043e\u0431 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043d\u043e\u0441\u0442\u0438 \u0441\u0443\u043c\u043c\u044b \u0431\u0430\u043b\u0430\u043d\u0441\u043e\u0432 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u0435\u0439 iToken\" width=\"1272\" height=\"632\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/f84\/eef\/ed4\/f84eefed4af17436887a51c1ca2f09c2.png\"\/><\/p>\n<div><figcaption>\u0420\u0438\u0441 5. \u041f\u0440\u0435\u0434\u0438\u043a\u0430\u0442 \u043e\u0431 \u0438\u043d\u0432\u0430\u0440\u0438\u0430\u043d\u0442\u043d\u043e\u0441\u0442\u0438 \u0441\u0443\u043c\u043c\u044b \u0431\u0430\u043b\u0430\u043d\u0441\u043e\u0432 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u0435\u0439 iToken<\/figcaption><\/div>\n<\/figure>\n<pre><code>QuickChick ({{msg_is_not_mint_or_burn}} iTokenContract {{sum_balances_unchanged}})<\/code><\/pre>\n<p>\u0417\u0430\u043f\u0443\u0441\u0442\u0438\u0432 \u0442\u0430\u043a\u043e\u0439 \u0442\u0435\u0441\u0442, \u0431\u0443\u0434\u0435\u0442 \u043f\u043e\u043b\u0443\u0447\u0435\u043d \u043a\u043e\u043d\u0442\u0440\u043f\u0440\u0438\u043c\u0435\u0440, \u043a\u043e\u0433\u0434\u0430 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u043d\u0435 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f:<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w1560\/getpro\/habr\/upload_files\/03a\/044\/663\/03a0446637ad98cb8241e01d48fb7db4.png\" alt=\"\u0420\u0438\u0441 6. \u0420\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u044b \u0442\u0435\u0441\u0442\u043e\u0432. \u0421\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u043d\u0430\u0440\u0443\u0448\u0430\u0435\u0442\u0441\u044f \u043f\u0440\u0438 \u0432\u044b\u0437\u043e\u0432\u0435 transferFrom c \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u044b\u043c\u0438 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0430\u043c\u0438 _from \u0438 _to\" title=\"\u0420\u0438\u0441 6. \u0420\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u044b \u0442\u0435\u0441\u0442\u043e\u0432. \u0421\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u043d\u0430\u0440\u0443\u0448\u0430\u0435\u0442\u0441\u044f \u043f\u0440\u0438 \u0432\u044b\u0437\u043e\u0432\u0435 transferFrom c \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u044b\u043c\u0438 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0430\u043c\u0438 _from \u0438 _to\" width=\"1309\" height=\"550\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/03a\/044\/663\/03a0446637ad98cb8241e01d48fb7db4.png\"\/><\/p>\n<div><figcaption>\u0420\u0438\u0441 6. \u0420\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u044b \u0442\u0435\u0441\u0442\u043e\u0432. \u0421\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u043d\u0430\u0440\u0443\u0448\u0430\u0435\u0442\u0441\u044f \u043f\u0440\u0438 \u0432\u044b\u0437\u043e\u0432\u0435 <code>transferFrom<\/code> c \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u044b\u043c\u0438 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0430\u043c\u0438 <code>_from \u0438 _to<\/code><\/figcaption><\/div>\n<\/figure>\n<h2>\u041c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 AMM\/DEX \u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0441\u0432\u043e\u0439\u0441\u0442\u0432 \u0435\u0433\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u0439<\/h2>\n<p>\u041c\u044b \u043f\u043e\u043f\u0440\u043e\u0431\u043e\u0432\u0430\u043b\u0438 \u043f\u0440\u0438\u043c\u0435\u043d\u0438\u0442\u044c ConCert \u0434\u043b\u044f \u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 <a href=\"https:\/\/github.com\/partylikeits1983\/sberAMM\">\u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u043c\u0430\u0440\u043a\u0435\u0442-\u043c\u0435\u0439\u043a\u0435\u0440\u0430<\/a> \u0441 \u043e\u0434\u043d\u043e\u0433\u043e \u0440\u043e\u0441\u0441\u0438\u0439\u0441\u043a\u043e\u0433\u043e \u0445\u0430\u043a\u0430\u0442\u043e\u043d\u0430, \u043f\u0440\u043e\u0448\u0435\u0434\u0448\u0435\u0433\u043e \u043b\u0435\u0442\u043e\u043c 2023 \u0433\u043e\u0434\u0430 (\u0441\u043c. <a href=\"https:\/\/interface-sber-amm.vercel.app\/\">\u0444\u0440\u043e\u043d\u0442 \u043f\u0440\u043e\u0435\u043a\u0442\u0430<\/a>).<\/p>\n<p>\u0421\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 \u043d\u0430\u043f\u0438\u0441\u0430\u043d \u043d\u0430 Solidity. \u041f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u0438 \u043c\u043e\u0433\u0443\u0442 \u0441\u043e\u0437\u0434\u0430\u0432\u0430\u0442\u044c \u043f\u0443\u043b\u044b \u043b\u0438\u043a\u0432\u0438\u0434\u043d\u043e\u0441\u0442\u0438, \u0432\u043d\u043e\u0441\u0438\u0442\u044c \u0432 \u043d\u0438\u0445 \u0441\u0440\u0435\u0434\u0441\u0442\u0432\u0430 \u0432 \u0442\u043e\u043a\u0435\u043d\u0430\u0445, \u0437\u0430\u0440\u0430\u0431\u0430\u0442\u044b\u0432\u0430\u0442\u044c \u043a\u043e\u043c\u0438\u0441\u0441\u0438\u043e\u043d\u043d\u044b\u0435 \u043d\u0430 \u0432\u043d\u0435\u0441\u0435\u043d\u043d\u044b\u0445 \u0430\u043a\u0442\u0438\u0432\u0430\u0445 \u0438 \u0441\u043d\u0438\u043c\u0430\u0442\u044c \u0437\u0430\u0440\u0430\u0431\u043e\u0442\u0430\u043d\u043d\u043e\u0435. \u0421\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 \u0432\u0437\u0438\u043c\u0430\u0435\u0442 \u043a\u043e\u043c\u0438\u0441\u0441\u0438\u044e \u0437\u0430 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430.\u00a0<\/p>\n<p>\u0423 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u043f\u044f\u0442\u044c \u0432\u0445\u043e\u0434\u043d\u044b\u0445 \u0442\u043e\u0447\u0435\u043a: \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u0435 \u043f\u0443\u043b\u0430, \u0432\u043d\u0435\u0441\u0435\u043d\u0438\u0435 \u0441\u0440\u0435\u0434\u0441\u0442\u0432 \u0432 \u043f\u0443\u043b, \u0432\u044b\u0432\u043e\u0434 \u0441\u0440\u0435\u0434\u0441\u0442\u0432 \u0438\u0437 \u043f\u0443\u043b\u0430, \u0432\u044b\u0432\u043e\u0434 \u0437\u0430\u0440\u0430\u0431\u043e\u0442\u0430\u043d\u043d\u044b\u0445 \u043a\u043e\u043c\u0438\u0441\u0441\u0438\u043e\u043d\u043d\u044b\u0445, \u0430 \u0442\u0430\u043a\u0436\u0435 \u043e\u0431\u043c\u0435\u043d:<\/p>\n<pre><code> Inductive Msg :=   | createPair : Address -> Address -> N -> bool -> Msg   | deposit : N -> N -> N -> Msg   | withdrawFees : N -> Msg    | withdraw : N -> Msg   | swap : N -> Address -> Msg<\/code><\/pre>\n<p>\u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0438\u0441\u0445\u043e\u0434\u043d\u044b\u0439 \u043a\u043e\u0434 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u043f\u0443\u043b\u0430 createPair. \u0421\u043e\u0437\u0434\u0430\u0442\u044c \u043f\u0443\u043b \u043c\u043e\u0436\u0435\u0442 \u043b\u044e\u0431\u043e\u0439 \u0443\u0447\u0430\u0441\u0442\u043d\u0438\u043a \u0441\u0435\u0442\u0438 \u043f\u0440\u0438 \u0443\u0441\u043b\u043e\u0432\u0438\u0438, \u0447\u0442\u043e \u044d\u0442\u0430 \u043f\u0430\u0440\u0430 \u0435\u0449\u0435 \u043d\u0435 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0430 \u0432 DEX.\u00a0<\/p>\n<pre><code class=\"javascript\">function createPair(address token0, address token1, uint _fee, bool _isStable) external returns (uint) {         require(token0 != token1, \"two identical addresses\");         require(token0 != address(0), \"Zero Address tokenA\");         require(token1 != address(0), \"Zero Address tokenB\");         require(getPool[token0][token1][_fee][_isStable] == 0, \"Pair already exists\");          PIDs++;         uint PID = PIDs;          Pools[PID].token0 = token0;         Pools[PID].token1 = token1;         Pools[PID].feeRate = _fee;         Pools[PID].isStable = _isStable;          getPool[token0][token1][_fee][_isStable] = PIDs;         getPool[token1][token0][_fee][_isStable] = PIDs;          return PID;     } <\/code><\/pre>\n<p>\u0422\u0430\u043a\u0436\u0435 \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0444\u043e\u0440\u043c\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044e \u044d\u0442\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0432 ConCert:<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w1560\/getpro\/habr\/upload_files\/485\/f1d\/fcd\/485f1dfcd44fbf008cda6e7d2e2a21c7.png\" alt=\"\u0420\u0438\u0441 7. \u0420\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438 createPair \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 sberAMM  \" title=\"\u0420\u0438\u0441 7. \u0420\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438 createPair \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 sberAMM  \" width=\"1463\" height=\"564\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/485\/f1d\/fcd\/485f1dfcd44fbf008cda6e7d2e2a21c7.png\"\/><\/p>\n<div><figcaption>\u0420\u0438\u0441 7. \u0420\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <code>createPair<\/code> \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 sberAMM  <\/figcaption><\/div>\n<\/figure>\n<p>\u0422\u0430\u043a \u043a\u0430\u043a \u043c\u044b \u0443\u0436\u0435 \u043e\u0431\u0441\u0443\u0434\u0438\u043b\u0438 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0432 ConCert \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e PBT, \u043f\u043e\u0434\u0440\u043e\u0431\u043d\u0435\u0435 \u043e\u0441\u0442\u0430\u043d\u043e\u0432\u0438\u043c\u0441\u044f \u043d\u0430 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0435 \u0442\u0435\u043e\u0440\u0435\u043c \u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0435\u043c\u043e\u0433\u043e \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430.<\/p>\n<p>\u0412 \u043e\u0431\u0449\u0435\u043c \u0441\u043b\u0443\u0447\u0430\u0435 \u0434\u043b\u044f \u043e\u0442\u0434\u0435\u043b\u044c\u043d\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u043c\u043e\u0436\u043d\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u0442\u0440\u0438 \u0442\u0435\u043e\u0440\u0435\u043c\u044b: \u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u043c \u043e\u0431\u043d\u043e\u0432\u043b\u0435\u043d\u0438\u0438 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f, \u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0439 \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u043f\u043e\u0440\u043e\u0436\u0434\u0435\u043d\u043d\u044b\u0445 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439 \u0438 \u043e \u0442\u043e\u043c, \u0447\u0442\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u044f \u0443\u0441\u043f\u0435\u0448\u043d\u043e \u043e\u0442\u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u0442\u043e\u0433\u0434\u0430 \u0438 \u0442\u043e\u043b\u044c\u043a\u043e \u0442\u043e\u0433\u0434\u0430, \u043a\u043e\u0433\u0434\u0430 \u043e\u043d\u0430 \u0432\u044b\u0437\u0432\u0430\u043d\u0430 \u0441 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u044b\u043c \u043d\u0430\u0431\u043e\u0440\u043e\u043c \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u043e\u0432.<\/p>\n<p>\u0412 \u043a\u0430\u0447\u0435\u0441\u0442\u0432\u0435 \u043f\u0440\u0438\u043c\u0435\u0440\u0430 \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u043f\u0435\u0440\u0432\u043e\u0439 \u0442\u0435\u043e\u0440\u0435\u043c\u044b \u0434\u043b\u044f <code>createPair<\/code>. \u0421\u043d\u0430\u0447\u0430\u043b\u0430 \u0437\u0430\u0434\u0430\u0434\u0438\u043c \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u0434\u043b\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438, \u0442\u043e \u0435\u0441\u0442\u044c \u043f\u0440\u0435\u0434\u0438\u043a\u0430\u0442, \u0441\u0438\u0433\u043d\u0430\u043b\u0438\u0437\u0438\u0440\u0443\u044e\u0449\u0438\u0439 \u043e \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u043c \u043e\u0431\u043d\u043e\u0432\u043b\u0435\u043d\u0438\u0438 \u0435\u0435 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f. \u0421\u0444\u043e\u0440\u043c\u0443\u043b\u0438\u0440\u0443\u0435\u043c \u0442\u0435\u043e\u0440\u0435\u043c\u0443: \u0434\u043b\u044f \u043b\u044e\u0431\u043e\u0433\u043e \u043d\u0430\u0431\u043e\u0440\u0430 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u043e\u0432 \u0438 \u043b\u044e\u0431\u044b\u0445 \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u044b\u0445 \u0438 \u043a\u043e\u043d\u0435\u0447\u043d\u043e\u0433\u043e \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0439 \u0435\u0441\u043b\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u044f <code>createPair<\/code> \u0431\u044b\u043b\u0430 \u0432\u044b\u0437\u0432\u0430\u043d\u0430 \u0438 \u0443\u0441\u043f\u0435\u0448\u043d\u043e \u0437\u0430\u0432\u0435\u0440\u0448\u0438\u043b\u0430\u0441\u044c, \u0442\u043e \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0435 \u043e\u0431\u043d\u043e\u0432\u044f\u0442\u0441\u044f \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e. \u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u0442\u0441\u044f \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0442\u0430\u043a\u0442\u0438\u043a Coq (\u044d\u0442\u043e \u0442\u0435\u043c\u0430 \u0434\u043b\u044f \u043e\u0442\u0434\u0435\u043b\u044c\u043d\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0438, \u043d\u043e \u043e\u0442\u043c\u0435\u0447\u0443, \u0447\u0442\u043e \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u043a\u0430\u043a \u0432\u043d\u0443\u0442\u0440\u0435\u043d\u043d\u0438\u0435 \u0442\u0430\u043a\u0442\u0438\u043a\u0438, \u0442\u0430\u043a \u0438 \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043d\u044b\u0435 \u0441\u0430\u043c\u043e\u0441\u0442\u043e\u044f\u0442\u0435\u043b\u044c\u043d\u043e).<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/r\/w1560\/getpro\/habr\/upload_files\/446\/ccb\/869\/446ccb8693723069e8fafc026578a2c6.png\" alt=\"\u0420\u0438\u0441 8. \u041f\u0440\u0435\u0434\u0438\u043a\u0430\u0442 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u0438 \u0442\u0435\u043e\u0440\u0435\u043c\u0430 \u043e \u0444\u0443\u043d\u043a\u0446\u0438\u0438 createPair  \" title=\"\u0420\u0438\u0441 8. \u041f\u0440\u0435\u0434\u0438\u043a\u0430\u0442 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u0438 \u0442\u0435\u043e\u0440\u0435\u043c\u0430 \u043e \u0444\u0443\u043d\u043a\u0446\u0438\u0438 createPair  \" width=\"1474\" height=\"915\" data-src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/446\/ccb\/869\/446ccb8693723069e8fafc026578a2c6.png\"\/><\/p>\n<div><figcaption>\u0420\u0438\u0441 8. \u041f\u0440\u0435\u0434\u0438\u043a\u0430\u0442 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u0438 \u0442\u0435\u043e\u0440\u0435\u043c\u0430 \u043e \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <code>createPair<\/code>  <\/figcaption><\/div>\n<\/figure>\n<p>\u041a\u0430\u043a \u043c\u044b \u043e\u0442\u043c\u0435\u0442\u0438\u043b\u0438 \u0432\u044b\u0448\u0435, ConCert \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u0442\u0435\u043e\u0440\u0435\u043c\u044b \u043d\u0435 \u0442\u043e\u043b\u044c\u043a\u043e \u0434\u043b\u044f \u043e\u0442\u0434\u0435\u043b\u044c\u043d\u044b\u0445 \u0444\u0443\u043d\u043a\u0446\u0438\u0439, \u043d\u043e \u0438 \u0434\u043b\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439. \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0434\u043b\u044f \u0434\u0430\u043d\u043d\u043e\u0433\u043e \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u043c\u043e\u0436\u043d\u043e \u0431\u044b\u043b\u043e \u0431\u044b \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c, \u0447\u0442\u043e \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c \u0432\u0441\u0435\u0433\u0434\u0430 \u0441\u043c\u043e\u0436\u0435\u0442 \u0432\u044b\u0432\u0435\u0441\u0442\u0438 \u0441\u0432\u043e\u0438 \u0432\u043d\u0435\u0441\u0435\u043d\u043d\u044b\u0435 \u0441\u0440\u0435\u0434\u0441\u0442\u0432\u0430. \u041e\u0434\u043d\u0430\u043a\u043e \u0432 \u0445\u043e\u0434\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <code>swap<\/code>, \u0432\u043e\u0437\u043d\u0438\u043a\u043b\u0430 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u0430, \u0441\u0432\u044f\u0437\u0430\u043d\u043d\u0430\u044f \u0441 \u043f\u0435\u0440\u0435\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435\u043c \u0432 \u0438\u0441\u0445\u043e\u0434\u043d\u043e\u043c \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0435.  <\/p>\n<pre><code class=\"javascript\">function swap(uint PID, address tokenIn, uint amount) external pidExists(PID) PIDstatus(PID) returns (uint) {         require(tokenIn == Pools[PID].token0 || tokenIn == Pools[PID].token1, \"Wrong token address\");         require(IERC20(tokenIn).transferFrom(msg.sender, address(this), amount));          address tokenOut = _getOtherTokenAddr(PID, tokenIn);         uint fee = (ud(Pools[PID].feeRate) * ud(amount)).unwrap();         uint amountMinusFee = amount - fee;         uint amountOut = _calculateAmounts(PID, tokenIn, amountMinusFee);          _handleFees(PID, tokenIn, fee);         IERC20(tokenOut).safeTransfer(msg.sender, uint(amountOut));          return uint(amountOut);     }<\/code><\/pre>\n<p>\u041e\u0448\u0438\u0431\u043a\u0430 \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u0442\u0441\u044f \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u0432 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <code>createPair<\/code> \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430 \u043d\u0430 \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u043e\u0441\u0442\u044c \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 <code>feeRate<\/code>. \u042d\u0442\u0430 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u0430\u044f \u0445\u0440\u0430\u043d\u0438\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 (\u043f\u043e \u043b\u043e\u0433\u0438\u043a\u0435 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u2014 \u0432 \u043f\u0440\u043e\u0446\u0435\u043d\u0442\u0430\u0445) \u043a\u043e\u043c\u0438\u0441\u0441\u0438\u0438 \u0437\u0430 \u043e\u0431\u043c\u0435\u043d. \u041f\u043e\u043b\u0443\u0447\u0430\u0435\u0442\u0441\u044f, \u0447\u0442\u043e \u0432 \u0441\u0435\u0434\u044c\u043c\u043e\u0439 \u0441\u0442\u0440\u043e\u043a\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <code>swap<\/code> \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 <code>amountMinusFee<\/code> \u0442\u0438\u043f\u0430 <code>uint<\/code>, \u0440\u0430\u0432\u043d\u043e\u0435 amount \u2013 fee, \u043c\u043e\u0436\u0435\u0442 \u0441\u0442\u0430\u0442\u044c \u043e\u0442\u0440\u0438\u0446\u0430\u0442\u0435\u043b\u044c\u043d\u044b\u043c. \u0412 \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0435\u043c\u043e\u043c \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0435 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f Solidity \u0432\u0435\u0440\u0441\u0438\u0438 0.8.19, \u0430 \u0437\u043d\u0430\u0447\u0438\u0442, \u0432 \u0441\u043b\u0443\u0447\u0430\u0435 \u0442\u0430\u043a\u043e\u0433\u043e \u043f\u0435\u0440\u0435\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u043f\u0440\u043e\u0438\u0437\u043e\u0448\u0435\u043b \u0431\u044b <code>revert<\/code>, \u0438 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u044f <code>swap<\/code> \u043d\u0435 \u0431\u044b\u043b\u0430 \u0431\u044b \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0430. \u0422\u043e \u0435\u0441\u0442\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u044f swap \u043d\u0435 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u0438, \u043d\u043e \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0438\u0435 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043d\u0430 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 <code>_fee<\/code> \u0432 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <code>createPair<\/code> \u043c\u043e\u0436\u0435\u0442 \u043f\u0440\u0438\u0432\u0435\u0441\u0442\u0438 \u043a \u0442\u043e\u043c\u0443, \u0447\u0442\u043e \u043d\u0435\u0434\u043e\u0431\u0440\u043e\u0441\u043e\u0432\u0435\u0441\u0442\u043d\u044b\u0439 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c \u0441\u043f\u043e\u0441\u043e\u0431\u0435\u043d \u0443\u0441\u0442\u0430\u043d\u0430\u0432\u043b\u0438\u0432\u0430\u0442\u044c \u043d\u0435\u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u0443\u044e \u043a\u043e\u043c\u0438\u0441\u0441\u0438\u044e \u0437\u0430 \u043e\u0431\u043c\u0435\u043d \u043f\u0430\u0440\u044b, \u0432 \u0442\u043e \u0432\u0440\u0435\u043c\u044f \u043a\u0430\u043a \u0434\u0440\u0443\u0433\u0438\u0435 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u0438 \u043d\u0435 \u0441\u043c\u043e\u0433\u0443\u0442 \u0441\u043e\u0437\u0434\u0430\u0442\u044c \u043d\u043e\u0432\u044b\u0439 \u043f\u0443\u043b \u044d\u0442\u043e\u0439 \u043f\u0430\u0440\u044b.<\/p>\n<p>\u041a\u0430\u043a \u043c\u044b \u0443\u0436\u0435 \u043e\u0442\u043c\u0435\u0442\u0438\u043b\u0438, \u044d\u0442\u0430 \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u044c \u0431\u044b\u043b\u0430 \u0437\u0430\u043c\u0435\u0447\u0435\u043d\u0430 \u0432 \u0445\u043e\u0434\u0435 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <code>swap<\/code>, \u043a\u043e\u0433\u0434\u0430 \u0442\u0430\u043a\u0442\u0438\u043a\u0438 Coq \u043d\u0435 \u043c\u043e\u0433\u043b\u0438 \u0440\u0430\u0437\u0440\u0435\u0448\u0438\u0442\u044c \u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u043e \u0441 \u043f\u043e\u043b\u043e\u0436\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u043e\u0439 <code>amountMinusFee<\/code>, \u0442\u0430\u043a \u043a\u0430\u043a \u043e\u043d\u0430 \u043f\u0435\u0440\u0435\u0441\u0442\u0430\u0432\u0430\u043b\u0430 \u0431\u044b\u0442\u044c \u043f\u043e\u043b\u043e\u0436\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u0432 \u043e\u0431\u0449\u0435\u043c \u0441\u043b\u0443\u0447\u0430\u0435.<\/p>\n<h2>\u0417\u0430\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435<\/h2>\n<p>\u0418\u0442\u0430\u043a, \u043c\u044b \u0440\u0430\u0437\u043e\u0431\u0440\u0430\u043b\u0438 \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a ConCert. \u041d\u0435\u0441\u043c\u043e\u0442\u0440\u044f \u043d\u0430 \u0442\u043e \u0447\u0442\u043e ConCert \u043d\u0435 \u043c\u043e\u0436\u0435\u0442 \u043d\u0430\u043f\u0440\u044f\u043c\u0443\u044e \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u0438\u0441\u0445\u043e\u0434\u043d\u043e\u0433\u043e \u043a\u043e\u0434\u0430 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430, \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043d\u043e\u0433\u043e \u043d\u0430 Solidity, \u043c\u044b \u0443\u0431\u0435\u0434\u0438\u043b\u0438\u0441\u044c, \u0447\u0442\u043e \u043e\u043d \u0445\u043e\u0440\u043e\u0448\u043e \u043f\u043e\u0434\u0445\u043e\u0434\u0438\u0442 \u0434\u043b\u044f \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0438 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u043b\u043e\u0433\u0438\u043a\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430. ConCert \u043d\u0435 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0435\u0434\u0438\u043d\u0441\u0442\u0432\u0435\u043d\u043d\u044b\u043c \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u043e\u043c \u0432 \u044d\u0442\u043e\u0439 \u043e\u0431\u043b\u0430\u0441\u0442\u0438, \u0434\u0430\u0436\u0435 \u043d\u0430 Coq \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u043e \u0435\u0449\u0435 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u043f\u0440\u043e\u0435\u043a\u0442\u043e\u0432 \u0434\u043b\u044f \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432. \u0415\u0441\u043b\u0438 \u0432\u044b\u0439\u0442\u0438 \u0437\u0430 \u0440\u0430\u043c\u043a\u0438 Coq, \u0442\u043e \u043c\u043e\u0436\u043d\u043e \u043d\u0430\u0439\u0442\u0438 \u0442\u0430\u043a\u0438\u0435 \u043f\u0440\u043e\u0435\u043a\u0442\u044b, \u043a\u0430\u043a Certora (<a href=\"https:\/\/habr.com\/ru\/companies\/pt\/articles\/786078\/\">\u043e \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u0440\u0430\u0441\u0441\u043a\u0430\u0437\u044b\u0432\u0430\u043b \u043c\u043e\u0439 \u043a\u043e\u043b\u043b\u0435\u0433\u0430 \u0421\u0435\u0440\u0433\u0435\u0439<\/a>), Isabelle\/Solidity, Solidity SMTChecker, KEVM \u0438 \u0434\u0440\u0443\u0433\u0438\u0435.<\/p>\n<p>\u041d\u0430\u0448\u0430 \u0446\u0435\u043b\u044c \u2014 \u043d\u0435 \u043f\u0440\u043e\u0441\u0442\u043e \u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u044c \u0442\u0435\u043a\u0443\u0449\u0438\u043c \u0442\u0440\u0435\u043d\u0434\u0430\u043c, \u0430 \u0430\u043a\u0442\u0438\u0432\u043d\u043e \u0443\u0447\u0430\u0441\u0442\u0432\u043e\u0432\u0430\u0442\u044c \u0432 \u0440\u0430\u0437\u0432\u0438\u0442\u0438\u0438 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d-\u0442\u0435\u0445\u043d\u043e\u043b\u043e\u0433\u0438\u0439. \u041d\u0435\u0441\u043c\u043e\u0442\u0440\u044f \u043d\u0430 \u0442\u0440\u0443\u0434\u043e\u0435\u043c\u043a\u043e\u0441\u0442\u044c \u044d\u0442\u043e\u0433\u043e \u043c\u0435\u0442\u043e\u0434\u0430, \u043c\u044b \u0443\u0432\u0435\u0440\u0435\u043d\u044b, \u0447\u0442\u043e \u0441 \u0440\u0430\u0437\u0432\u0438\u0442\u0438\u0435\u043c \u0442\u0435\u043a\u0443\u0449\u0438\u0445 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u043e\u0432 \u0438 \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u0435\u043c \u043d\u043e\u0432\u044b\u0445, \u043f\u0440\u0438\u043c\u0435\u043d\u0435\u043d\u0438\u0435 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0445 \u043c\u0435\u0442\u043e\u0434\u043e\u0432 \u0431\u0443\u0434\u0435\u0442 \u0438\u0433\u0440\u0430\u0442\u044c \u043a\u043b\u044e\u0447\u0435\u0432\u0443\u044e \u0440\u043e\u043b\u044c \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d-\u0438\u043d\u0434\u0443\u0441\u0442\u0440\u0438\u0438.\u00a0<\/p>\n<p>\u041d\u0430\u0448\u0430 \u043a\u043e\u043c\u043f\u0430\u043d\u0438\u044f \u0430\u043a\u0442\u0438\u0432\u043d\u043e \u0438\u0437\u0443\u0447\u0430\u0435\u0442 \u0438 \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u0435\u0442 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0443\u044e \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044e \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0438 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d-\u043f\u0440\u0438\u043b\u043e\u0436\u0435\u043d\u0438\u0439; \u043c\u044b \u043f\u043e\u043d\u0438\u043c\u0430\u0435\u043c \u0438\u0445 \u0437\u043d\u0430\u0447\u0438\u043c\u043e\u0441\u0442\u044c \u0438 \u044d\u0444\u0444\u0435\u043a\u0442\u0438\u0432\u043d\u043e\u0441\u0442\u044c. \u041c\u044b \u0442\u0430\u043a\u0436\u0435 \u0430\u043a\u0442\u0438\u0432\u043d\u043e \u0438\u0441\u0441\u043b\u0435\u0434\u0443\u0435\u043c \u0438 \u0432\u043d\u0435\u0434\u0440\u044f\u0435\u043c \u0434\u0440\u0443\u0433\u0438\u0435 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u044b \u0438 \u043c\u0435\u0442\u043e\u0434\u0438\u043a\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0442 \u043f\u043e\u0432\u044b\u0441\u0438\u0442\u044c \u043a\u0430\u0447\u0435\u0441\u0442\u0432\u043e \u0438 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u044c \u0440\u0430\u0437\u0440\u0430\u0431\u0430\u0442\u044b\u0432\u0430\u0435\u043c\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c. \u041e\u043d\u0438 \u0432\u043a\u043b\u044e\u0447\u0430\u044e\u0442 \u0432 \u0441\u0435\u0431\u044f \u043a\u0430\u043a \u043d\u043e\u0432\u0435\u0439\u0448\u0438\u0435 \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u043a\u0438 \u0432 \u043e\u0431\u043b\u0430\u0441\u0442\u0438 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438, \u0442\u0430\u043a \u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u0435\u043d\u043d\u044b\u0435 \u0432\u0440\u0435\u043c\u0435\u043d\u0435\u043c \u043c\u0435\u0442\u043e\u0434\u0438\u043a\u0438 \u2014<a href=\"https:\/\/habr.com\/ru\/companies\/pt\/articles\/775074\/\"> \u0441\u0442\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438\u0439 \u0430\u043d\u0430\u043b\u0438\u0437<\/a>, \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0438 \u0444\u0430\u0437\u0437\u0438\u043d\u0433.\u00a0<\/p>\n<p><span class=\"habrahidden\">\u041f\u043e \u0432\u0441\u0435\u043c \u0432\u043e\u043f\u0440\u043e\u0441\u0430\u043c \u0438 \u043f\u0440\u0435\u0434\u043b\u043e\u0436\u0435\u043d\u0438\u044f\u043c \u043c\u043e\u0436\u0435\u0442\u0435 \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u043d\u0430 \u043d\u0430\u0448 \u0430\u0434\u0440\u0435\u0441 \u044d\u043b\u0435\u043a\u0442\u0440\u043e\u043d\u043d\u043e\u0439 \u043f\u043e\u0447\u0442\u044b: web3@ptsecurity.com.  <\/span><\/p>\n<\/p>\n<\/div>\n<\/div>\n<\/div>\n<p><!----><!----><\/div>\n<p><!----><!----><br \/> \u0441\u0441\u044b\u043b\u043a\u0430 \u043d\u0430 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b \u0441\u0442\u0430\u0442\u044c\u0438 <a href=\"https:\/\/habr.com\/ru\/articles\/804861\/\"> https:\/\/habr.com\/ru\/articles\/804861\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<div><!--[--><!--]--><\/div>\n<div id=\"post-content-body\">\n<div>\n<div class=\"article-formatted-body article-formatted-body article-formatted-body_version-2\">\n<div xmlns=\"http:\/\/www.w3.org\/1999\/xhtml\">\n<figure class=\"full-width\"><\/figure>\n<p>\u0414\u043e\u0431\u0440\u044b\u0439 \u0434\u0435\u043d\u044c! \u041c\u0435\u043d\u044f \u0437\u043e\u0432\u0443\u0442 \u041a\u0438\u0440\u0438\u043b\u043b \u0417\u0438\u0431\u043e\u0440\u043e\u0432, \u044f \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u044e \u043e\u0442\u0434\u0435\u043b \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 \u0440\u0430\u0441\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0445 \u0441\u0438\u0441\u0442\u0435\u043c Positive Technologies. \u0412 \u044d\u0442\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u043c\u044b <a href=\"https:\/\/habr.com\/ru\/companies\/pt\/articles\/786078\/\">\u043f\u0440\u043e\u0434\u043e\u043b\u0436\u0438\u043c \u043e\u0431\u0441\u0443\u0436\u0434\u0430\u0442\u044c <\/a>\u043c\u0435\u0442\u043e\u0434\u044b \u0438 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u044b \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0438 \u0438\u0445 \u043f\u0440\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0435 \u043f\u0440\u0438\u043c\u0435\u043d\u0435\u043d\u0438\u0435 \u0434\u043b\u044f \u043f\u0440\u0435\u0434\u043e\u0442\u0432\u0440\u0430\u0449\u0435\u043d\u0438\u044f \u0443\u044f\u0437\u0432\u0438\u043c\u043e\u0441\u0442\u0435\u0439. \u041c\u044b \u043f\u043e\u0434\u0440\u043e\u0431\u043d\u043e \u043f\u043e\u0433\u043e\u0432\u043e\u0440\u0438\u043c \u043e \u043c\u0435\u0442\u043e\u0434\u0435 \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438, \u0430 \u0442\u043e\u0447\u043d\u0435\u0435, \u043e \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a\u0435 \u0434\u043b\u044f \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u2014 ConCert.<\/p>\n<h2>\u0427\u0442\u043e \u0442\u0430\u043a\u043e\u0435 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f<\/h2>\n<p>\u0424\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u2014 \u044d\u0442\u043e \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438\u0435 \u043c\u0435\u0442\u043e\u0434\u044b \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u043e\u0433\u043e, \u0447\u0442\u043e \u043c\u043e\u0434\u0435\u043b\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0437\u0430\u0434\u0430\u043d\u043d\u043e\u0439 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438, \u0442\u043e \u0435\u0441\u0442\u044c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u043c\u0443 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u044e. \u0421\u0443\u0449\u0435\u0441\u0442\u0432\u0443\u0435\u0442 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0445 \u043f\u043e\u0434\u0445\u043e\u0434\u043e\u0432 \u043a \u043f\u043e\u0441\u0442\u0440\u043e\u0435\u043d\u0438\u044e \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0445 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432 \u0442\u043e\u0433\u043e, \u0447\u0442\u043e \u043c\u043e\u0434\u0435\u043b\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0438\u043b\u0438 \u043d\u0435 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0441\u0432\u043e\u0435\u0439 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438: model checking, \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u044b\u0439 \u043c\u0435\u0442\u043e\u0434 \u0441 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c \u0441\u0440\u0435\u0434\u0441\u0442\u0432 \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u043b\u0438\u0431\u043e \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c \u0438 \u0434\u0440\u0443\u0433\u0438\u0435.\u00a0<\/p>\n<p>\u041e\u0441\u043d\u043e\u0432\u043d\u043e\u0435 \u043f\u0440\u0435\u0438\u043c\u0443\u0449\u0435\u0441\u0442\u0432\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u044f \u0434\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u043c\u0435\u0442\u043e\u0434\u0430 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u043e \u0441\u0440\u0430\u0432\u043d\u0435\u043d\u0438\u044e \u0441 <abbr class=\"habraabbr\" title=\"model checking\" data-title=\"&lt;p>model checking  &lt;\/p>&#187; data-abbr=&#187;\u043f\u0440\u043e\u0432\u0435\u0440\u043a\u043e\u0439 \u043c\u043e\u0434\u0435\u043b\u0435\u0439 &#171;>\u043f\u0440\u043e\u0432\u0435\u0440\u043a\u043e\u0439 \u043c\u043e\u0434\u0435\u043b\u0435\u0439<\/abbr> \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u0443 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u043d\u044b\u0445 \u044f\u0437\u044b\u043a\u043e\u0432 <abbr class=\"habraabbr\" title=\"model checkers\" data-title=\"&lt;p>model checkers&lt;\/p>&#187; data-abbr=&#187;\u0441\u0440\u0435\u0434\u0441\u0442\u0432 \u0442\u0430\u043a\u043e\u0439 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438&#187;>\u0441\u0440\u0435\u0434\u0441\u0442\u0432 \u0442\u0430\u043a\u043e\u0439 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438<\/abbr> \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u044b\u0439 \u043d\u0430\u0431\u043e\u0440 \u043e\u043f\u0435\u0440\u0430\u0442\u043e\u0440\u043e\u0432. \u041e\u043d\u0438 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0442 \u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043b\u0438\u0448\u044c \u043d\u0435\u0431\u043e\u043b\u044c\u0448\u043e\u0435 \u043f\u043e\u0434\u043c\u043d\u043e\u0436\u0435\u0441\u0442\u0432\u043e \u044f\u0437\u044b\u043a\u0430, \u043d\u0430 \u043a\u043e\u0442\u043e\u0440\u043e\u043c \u043d\u0430\u043f\u0438\u0441\u0430\u043d \u0438\u0441\u0445\u043e\u0434\u043d\u044b\u0439 \u043a\u043e\u0434. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0432 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u0441\u043b\u0443\u0447\u0430\u044f\u0445 \u043c\u043e\u0434\u0435\u043b\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0442\u0440\u0430\u043d\u0441\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u0430 \u0432 \u044f\u0437\u044b\u043a, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0439 \u0432 \u0441\u0440\u0435\u0434\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c, \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u044b\u043c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u043c \u041f\u041e.<\/p>\n<p>\u0410\u043a\u0442\u0443\u0430\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u043f\u043e\u043f\u0443\u043b\u044f\u0440\u043d\u044b\u0435 \u0441\u0435\u0439\u0447\u0430\u0441 \u043f\u043e\u0434\u0445\u043e\u0434\u044b, \u0441\u0432\u044f\u0437\u0430\u043d\u043d\u044b\u0435 \u0441 \u0430\u0443\u0434\u0438\u0442\u043e\u043c \u0438 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435\u043c \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432, \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0442 \u043e\u0431\u043d\u0430\u0440\u0443\u0436\u0438\u0442\u044c \u043e\u0448\u0438\u0431\u043a\u0438, \u043d\u043e \u043d\u0435 \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u044e\u0442 \u0438\u0445 \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0438\u0435. \u0424\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u044b\u0435 \u043c\u0435\u0442\u043e\u0434\u044b \u0436\u0435 \u043c\u043e\u0433\u0443\u0442 \u043f\u043e\u043c\u043e\u0447\u044c \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0441\u0442\u0440\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b.<\/p>\n<h2>\u0421\u0440\u0435\u0434\u044b \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430<\/h2>\n<p>\u0414\u0435\u0434\u0443\u043a\u0442\u0438\u0432\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u041f\u041e \u043e\u0431\u044b\u0447\u043d\u043e \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u0434\u0438\u0442\u0441\u044f \u0432 \u0441\u0440\u0435\u0434\u0430\u0445 \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0438\u043b\u0438 \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c (\u0442\u0430\u043a\u0436\u0435 \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u043c\u044b\u0445 proof assistants). \u0412 \u0441\u0440\u0435\u0434\u0430\u0445 \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 (Why3, PVS, Z3 \u0438 \u0434\u0440\u0443\u0433\u0438\u0445) \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 (\u0438\u043b\u0438 \u043a\u043e\u043d\u0442\u0440\u043f\u0440\u0438\u043c\u0435\u0440\u044b) \u0433\u0435\u043d\u0435\u0440\u0438\u0440\u0443\u044e\u0442\u0441\u044f \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e SAT- \u0438 SMT-\u0440\u0435\u0448\u0430\u0442\u0435\u043b\u0435\u0439, \u0430 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c \u043d\u0435 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u043d\u0435\u043f\u043e\u0441\u0440\u0435\u0434\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0433\u043e \u0443\u0447\u0430\u0441\u0442\u0438\u044f \u0432 \u0434\u0435\u0434\u0443\u043a\u0446\u0438\u0438. \u041e\u0441\u043d\u043e\u0432\u043d\u043e\u0439 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u043e\u0439 \u0442\u0430\u043a\u043e\u0433\u043e \u043c\u0435\u0442\u043e\u0434\u0430 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u043e\u0441\u0442\u044c \u043a\u043b\u0430\u0441\u0441\u0430 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u0439, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043c\u043e\u0433\u0443\u0442 \u0431\u044b\u0442\u044c \u0434\u043e\u043a\u0430\u0437\u0430\u043d\u044b \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0432 \u0441\u043b\u0443\u0447\u0430\u0435 \u043d\u0435\u0443\u0434\u0430\u0447\u0438 \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0437\u0430\u0447\u0430\u0441\u0442\u0443\u044e \u0442\u0440\u0443\u0434\u043d\u043e \u043f\u043e\u043d\u044f\u0442\u044c, \u0447\u0442\u043e \u043f\u043e\u0448\u043b\u043e \u043d\u0435 \u0442\u0430\u043a \u0438 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043b\u0438 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u0434\u043e\u043a\u0430\u0437\u0443\u0435\u043c\u044b\u043c \u0432 \u043f\u0440\u0438\u043d\u0446\u0438\u043f\u0435.<\/p>\n<p>\u0427\u0442\u043e \u043a\u0430\u0441\u0430\u0435\u0442\u0441\u044f \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u044b\u0445 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432 \u0432 proof assistants (\u043d\u0430\u0438\u0431\u043e\u043b\u0435\u0435 \u043f\u043e\u043f\u0443\u043b\u044f\u0440\u043d\u044b\u043c\u0438 \u0438\u0437 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f Coq, Lean, Isabelle \u0438 \u0441\u0435\u043c\u0435\u0439\u0441\u0442\u0432\u043e HOL), \u0442\u043e \u0442\u0430\u043a\u0438\u0435 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0432\u044b\u0440\u0430\u0431\u0430\u0442\u044b\u0432\u0430\u044e\u0442\u0441\u044f \u0432 \u043f\u0440\u043e\u0446\u0435\u0441\u0441\u0435 \u0432\u0437\u0430\u0438\u043c\u043e\u0434\u0435\u0439\u0441\u0442\u0432\u0438\u044f \u0447\u0435\u043b\u043e\u0432\u0435\u043a\u0430 \u0441 \u043a\u043e\u043c\u043f\u044c\u044e\u0442\u0435\u0440\u043e\u043c (\u0437\u0430\u0447\u0430\u0441\u0442\u0443\u044e \u0447\u0435\u0440\u0435\u0437 IDE). \u041c\u0435\u0436\u0434\u0443 \u0441\u043e\u0431\u043e\u0439 \u0441\u0440\u0435\u0434\u044b \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0440\u0430\u0437\u043b\u0438\u0447\u0430\u044e\u0442\u0441\u044f \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u043c \u0432 \u043d\u0438\u0445 \u044f\u0437\u044b\u043a\u043e\u043c (\u043e\u0431\u044b\u0447\u043d\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u044b\u043c), \u0441\u0442\u0435\u043f\u0435\u043d\u044c\u044e \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0437\u0430\u0446\u0438\u0438, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c \u0438\u043b\u0438 \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0438\u0435\u043c \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432.<\/p>\n<h2>Coq  <\/h2>\n<p>\u0420\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0435\u043c\u044b\u0439 \u0432 \u044d\u0442\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0435 \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d \u0432 Coq. \u042d\u0442\u043e \u0441\u0440\u0435\u0434\u0430 \u0438\u043d\u0442\u0435\u0440\u0430\u043a\u0442\u0438\u0432\u043d\u043e\u0433\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0449\u0430\u044f Gallina \u2014 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e-\u0442\u0438\u043f\u0438\u0437\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u044b\u0439 \u044f\u0437\u044b\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f, \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0449\u0438\u0439 \u0432\u044b\u0440\u0430\u0436\u0430\u0442\u044c \u043a\u0430\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b, \u0442\u0430\u043a \u0438 \u0438\u0445 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430. \u0412 Coq \u0442\u0430\u043a\u0436\u0435 \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u0430 \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0437\u0430\u0446\u0438\u044f \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432 \u0447\u0435\u0440\u0435\u0437 \u0442\u0430\u043a\u0442\u0438\u043a\u0438 \u0438 \u043c\u0435\u0442\u0430\u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0441 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c MetaCoq. \u0412 \u0438\u043d\u0434\u0443\u0441\u0442\u0440\u0438\u0438 Coq \u0431\u044b\u043b \u0443\u0441\u043f\u0435\u0448\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d \u0432 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u043f\u0440\u043e\u0435\u043a\u0442\u0430\u0445, \u0432 \u0442\u043e\u043c \u0447\u0438\u0441\u043b\u0435:<\/p>\n<ul>\n<li>\n<p>\u0434\u043b\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 JavaCard;\u00a0<\/p>\n<\/li>\n<li>\n<p>\u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u0433\u043e \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0442\u043e\u0440\u0430 CompCert \u0434\u043b\u044f C;<\/p>\n<\/li>\n<li>\n<p>\u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0442\u0435\u043e\u0440\u0435\u043c\u044b \u043e \u0447\u0435\u0442\u044b\u0440\u0435\u0445 \u043a\u0440\u0430\u0441\u043a\u0430\u0445 \u0438 \u0442\u0435\u043e\u0440\u0435\u043c\u044b \u0424\u0435\u0439\u0442\u0430 \u2014 \u0422\u043e\u043c\u043f\u0441\u043e\u043d\u0430;<\/p>\n<\/li>\n<li>\n<p>\u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0432 \u043f\u0440\u043e\u0435\u043a\u0442\u0435 <a href=\"https:\/\/pruvendo.com\/\">Pruvendo<\/a> \u0438 \u0432 \u043f\u0440\u043e\u0435\u043a\u0442\u0430\u0445 <a href=\"https:\/\/formal.land\/\">Formal Land<\/a> (\u0434\u043b\u044f \u043d\u0435\u0435 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442 \u0442\u0430\u043a\u0436\u0435 \u0438 ConCert).<\/p>\n<\/li>\n<\/ul>\n<h2>\u0424\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a ConCert<\/h2>\n<h3>\u0410\u0440\u0445\u0438\u0442\u0435\u043a\u0442\u0443\u0440\u0430<\/h3>\n<p>\u0424\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u0431\u043e\u0439 \u0441\u043e\u0432\u043e\u043a\u0443\u043f\u043d\u043e\u0441\u0442\u044c \u043c\u043e\u0434\u0435\u043b\u0438 \u0441\u0440\u0435\u0434\u044b \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0432 Coq, \u0430 \u0442\u0430\u043a\u0436\u0435 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u043e\u0432 \u0434\u043b\u044f \u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0438 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0438 \u043a\u043e\u0434\u043e\u0433\u0435\u043d\u0435\u0440\u0430\u0446\u0438\u0438. ConCert \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0434\u0432\u0430 \u043f\u043e\u0434\u0445\u043e\u0434\u0430 \u0434\u043b\u044f \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u043a\u0438 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u044b\u0445 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432: \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u043a\u0430\u043a \u0441\u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u0438\u0441\u0445\u043e\u0434\u043d\u043e\u0433\u043e \u043a\u043e\u0434\u0430 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 \u0432 ConCert, \u0442\u0430\u043a \u0438 \u0438\u0437\u0432\u043b\u0435\u0447\u044c \u043a\u043e\u0434 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u0433\u043e \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0438\u0437 Coq.<\/p>\n<p>\u0421\u043d\u0430\u0447\u0430\u043b\u0430 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u044e\u0442\u0441\u044f \u043d\u0430 \u044f\u0437\u044b\u043a\u0435 Gallina. \u042d\u0442\u043e \u043e\u0431\u044b\u0447\u043d\u044b\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043f\u0440\u0435\u0434\u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u043d\u044b\u0435 \u043f\u0440\u0438\u043c\u0438\u0442\u0438\u0432\u044b \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430, \u043f\u0440\u0435\u0434\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u043c\u044b\u0435 \u0438\u043d\u0444\u0440\u0430\u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u043e\u0439 ConCert. \u0417\u0430\u0442\u0435\u043c \u043f\u0438\u0448\u0435\u0442\u0441\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0438 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0438\u043d\u0442\u0435\u0433\u0440\u0430\u0446\u0438\u0438<a href=\"https:\/\/github.com\/QuickChick\/QuickChick\"> QuickChick<\/a> \u043f\u043e\u043b\u0443\u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0442\u0435\u0441\u0442\u0438\u0440\u0443\u044e\u0442\u0441\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u043f\u043e \u043d\u0435\u0439. \u0411\u043e\u043b\u0435\u0435 \u0442\u043e\u0433\u043e, \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0438\u043d\u0444\u0440\u0430\u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u044b ConCert. \u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0430 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442 \u043c\u043e\u0434\u0435\u043b\u044c \u0441\u0440\u0435\u0434\u044b \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0434\u043b\u044f \u0440\u0430\u0441\u0441\u0443\u0436\u0434\u0435\u043d\u0438\u0439 \u043e \u0432\u0437\u0430\u0438\u043c\u043e\u0434\u0435\u0439\u0441\u0442\u0432\u0443\u044e\u0449\u0438\u0445 \u043c\u0435\u0436\u0434\u0443 \u0441\u043e\u0431\u043e\u0439 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430\u0445. \u042d\u0442\u043e \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0434\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0430, \u0432\u044b\u0445\u043e\u0434\u044f\u0449\u0438\u0435 \u0437\u0430 \u0440\u0430\u043c\u043a\u0438 \u043f\u0440\u043e\u0441\u0442\u043e\u0439 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u043e\u0442\u0434\u0435\u043b\u044c\u043d\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430.<\/p>\n<figure class=\"full-width\">\n<div><figcaption><a href=\"https:\/\/arxiv.org\/pdf\/2203.08016.pdf\">\u0420\u0438\u0441 1. \u0410\u0440\u0445\u0438\u0442\u0435\u043a\u0442\u0443\u0440\u0430 ConCert<\/a>  <\/figcaption><\/div>\n<\/figure>\n<p>\u041f\u043e\u0441\u043b\u0435 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043c\u043e\u0436\u043d\u043e \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0438\u0437\u0432\u043b\u0435\u0447\u0435\u043d\u0438\u044f \u043a\u043e\u0434\u0430 \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u0438\u0441\u043f\u043e\u043b\u043d\u044f\u0435\u043c\u0443\u044e \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044e \u043d\u0430 \u043e\u0434\u043d\u043e\u043c \u0438\u0437 \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u0438\u0432\u0430\u0435\u043c\u044b\u0445 \u044f\u0437\u044b\u043a\u043e\u0432 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432. \u0414\u043b\u044f \u044d\u0442\u043e\u0433\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442\u0441\u044f \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u044b MetaCoq \u0441 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u043c\u0438 \u043e\u043f\u0442\u0438\u043c\u0438\u0437\u0430\u0446\u0438\u044f\u043c\u0438 \u0438 \u043f\u0440\u0435\u0434\u0432\u0430\u0440\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u043e\u0431\u0440\u0430\u0431\u043e\u0442\u043a\u043e\u0439 \u0432 ConCert. \u042d\u0442\u043e \u043e\u0431\u0435\u0441\u043f\u0435\u0447\u0438\u0432\u0430\u0435\u0442 \u043f\u0440\u043e\u0446\u0435\u0434\u0443\u0440\u0443 \u043a\u043e\u0434\u043e\u0433\u0435\u043d\u0435\u0440\u0430\u0446\u0438\u0438 \u0441 \u0441\u0438\u043b\u044c\u043d\u044b\u043c\u0438 \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u044f\u043c\u0438 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438.<\/p>\n<h3>\u041d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0441\u043e\u0432\u0435\u0442\u043e\u0432 \u043f\u043e \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u0435<\/h3>\n<p>ConCert \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0430\u043d \u0432 Coq 8.17 \u0438 \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442 MetaCoq \u0438 std++. \u0414\u043b\u044f \u0440\u0430\u0431\u043e\u0442\u044b \u0441 \u0442\u0435\u0441\u0442\u0430\u043c\u0438 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u0430 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 QuickChick. \u0412\u0441\u0435 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0441\u0442\u0438 \u043c\u043e\u0436\u043d\u043e \u0443\u0441\u0442\u0430\u043d\u043e\u0432\u0438\u0442\u044c \u0447\u0435\u0440\u0435\u0437 opam, \u043c\u0435\u043d\u0435\u0434\u0436\u0435\u0440\u0430 \u043f\u0430\u043a\u0435\u0442\u043e\u0432 OCaml:<\/p>\n<p><code>sudo apt install opam<br \/>opam switch create . 4.10.2 --repositories default,coq-released=https:\/\/coq.inria.fr\/opam\/released<br \/> eval $(opam env)<\/code><\/p>\n<p>\u0423\u0441\u0442\u0430\u043d\u043e\u0432\u043a\u0430 ConCert \u0438 \u0435\u0433\u043e \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0441\u0442\u0435\u0439:<\/p>\n<p><code>git clone https:\/\/github.com\/AU-COBRA\/ConCert.git<br \/>cd ConCert<br \/>opam install .\/coq-concert.opam<\/code><\/p>\n<p>\u0421\u0431\u043e\u0440\u043a\u0430 \u043f\u0440\u0438\u043c\u0435\u0440\u043e\u0432 \u0438\u0437 \u0440\u0435\u043f\u043e\u0437\u0438\u0442\u043e\u0440\u0438\u044f:<\/p>\n<p><code>git clone https:\/\/github.com\/AU-COBRA\/ConCert.git<br \/>cd ConCert<br \/> opam install .\/coq-concert.opam --with-test<\/code><\/p>\n<h3>\u041c\u043e\u0434\u0435\u043b\u044c \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0438 \u0441\u0440\u0435\u0434\u044b \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f<\/h3>\n<p>\u041c\u043e\u0434\u0435\u043b\u044c \u0441\u0440\u0435\u0434\u044b \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u043e\u0431\u043b\u0435\u0433\u0447\u0430\u0435\u0442 \u0440\u0430\u0441\u0441\u0443\u0436\u0434\u0435\u043d\u0438\u044f \u043e \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0430\u0445 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u0432\u044b\u0437\u043e\u0432\u043e\u0432 (\u0442\u0440\u0430\u0441\u0441\u044b) \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432. \u0421\u0430\u043c \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 \u0432 \u043c\u043e\u0434\u0435\u043b\u0438 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043a\u0430\u043a \u043f\u0430\u0440\u0430 \u0444\u0443\u043d\u043a\u0446\u0438\u0439: <code>init<\/code> \u0438 <code>receive<\/code>.\u00a0<\/p>\n<pre><code>init : Chain -> ContractCallContext -> Setup -> option State<\/code><\/pre>\n<p>\u0424\u0443\u043d\u043a\u0446\u0438\u044f <code>init<\/code> \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u043f\u0440\u0438 \u0440\u0430\u0437\u0432\u0435\u0440\u0442\u044b\u0432\u0430\u043d\u0438\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0434\u043b\u044f \u0442\u043e\u0433\u043e, \u0447\u0442\u043e\u0431\u044b \u0437\u0430\u0434\u0430\u0442\u044c \u0435\u0433\u043e \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435. \u041f\u0435\u0440\u0432\u044b\u0439 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440 \u0442\u0438\u043f\u0430 <code>Chain<\/code> \u043f\u0435\u0440\u0435\u0434\u0430\u0435\u0442 \u0434\u0430\u043d\u043d\u044b\u0435 \u043e \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0435: \u043a\u043e\u043b\u0438\u0447\u0435\u0441\u0442\u0432\u043e \u0431\u043b\u043e\u043a\u043e\u0432 \u0438 \u043e\u0442\u043e\u0431\u0440\u0430\u0436\u0435\u043d\u0438\u0435 \u0438\u0437 \u0430\u0434\u0440\u0435\u0441\u043e\u0432 \u0432 \u0438\u0445 \u0431\u0430\u043b\u0430\u043d\u0441\u044b. \u041f\u0430\u0440\u0430\u043c\u0435\u0442\u0440 <code>ContractCallContext<\/code> \u043f\u0435\u0440\u0435\u0434\u0430\u0435\u0442 \u0434\u0430\u043d\u043d\u044b\u0435 \u043e \u0442\u0435\u043a\u0443\u0449\u0435\u043c \u0432\u044b\u0437\u043e\u0432\u0435: \u0430\u0434\u0440\u0435\u0441\u0430 \u0432\u044b\u0437\u044b\u0432\u0430\u044e\u0449\u0435\u0433\u043e \u0438 \u0432\u044b\u0437\u044b\u0432\u0430\u0435\u043c\u043e\u0433\u043e \u0438 \u0441\u0443\u043c\u043c\u0443, \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u0443\u044e \u0432 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442. <code>Setup<\/code> \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u0431\u043e\u0439 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u044b \u0438\u043d\u0438\u0446\u0438\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438.<\/p>\n<pre><code>receive : Chain -> ContractCallContext -> State -> option Msg -> option (State \u2217 list ActionBody)  <\/code><\/pre>\n<p>\u0424\u0443\u043d\u043a\u0446\u0438\u044f <code>receive<\/code> \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u0434\u043b\u044f \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u0438\u0445 \u0432\u044b\u0437\u043e\u0432\u043e\u0432 \u0438 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442\u0441\u044f \u043f\u0440\u0438 \u043a\u0430\u0436\u0434\u043e\u043c \u043e\u0431\u0440\u0430\u0449\u0435\u043d\u0438\u0438 \u043a \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0443. <code>State<\/code> \u2014 \u044d\u0442\u043e \u0442\u0435\u043a\u0443\u0449\u0435\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430. <code>Msg<\/code> \u2014 \u044d\u0442\u043e \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0435\u043c\u044b\u0439 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u0435\u043c \u0442\u0438\u043f \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442 (\u0435\u0433\u043e \u0442\u043e\u0447\u043a\u0438 \u0432\u0445\u043e\u0434\u0430). \u0420\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u043e\u043c \u0443\u0441\u043f\u0435\u0448\u043d\u043e\u0433\u043e \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043d\u043e\u0432\u043e\u0435 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0438 \u0441\u043f\u0438\u0441\u043e\u043a \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439, \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u043d\u044b\u0439 \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0442\u0438\u043f\u0430 <code>ActionBody<\/code>. \u0414\u0435\u0439\u0441\u0442\u0432\u0438\u044f \u043c\u043e\u0433\u0443\u0442 \u0431\u044b\u0442\u044c \u043f\u0435\u0440\u0435\u0432\u043e\u0434\u0430\u043c\u0438 \u0441\u0440\u0435\u0434\u0441\u0442\u0432, \u0432\u044b\u0437\u043e\u0432\u0430\u043c\u0438 \u0434\u0440\u0443\u0433\u0438\u0445 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432 \u0438 \u0440\u0430\u0437\u0432\u0435\u0440\u0442\u044b\u0432\u0430\u043d\u0438\u044f\u043c\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432.<\/p>\n<p>\u0422\u0438\u043f <code>Chain<\/code> \u043d\u0435 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u0438, \u0447\u0442\u043e\u0431\u044b \u0441\u043c\u043e\u0434\u0435\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0435 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439 \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0435. \u041d\u0430\u043c \u043d\u0443\u0436\u043d\u043e \u0438\u043c\u0435\u0442\u044c \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u043e\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0442\u044c \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044e \u043e \u0442\u0435\u043a\u0443\u0449\u0438\u0445 \u0440\u0430\u0437\u0432\u0435\u0440\u043d\u0443\u0442\u044b\u0445 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430\u0445, \u0430 \u0442\u043e\u0447\u043d\u0435\u0435, \u043e\u0431 \u0438\u0445 \u0444\u0443\u043d\u043a\u0446\u0438\u044f\u0445 \u0438 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u044f\u0445. \u0414\u043b\u044f \u044d\u0442\u043e\u0433\u043e \u0432\u0432\u043e\u0434\u0438\u0442\u0441\u044f \u0442\u0438\u043f <code>Environment<\/code>, \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u044e\u0449\u0438\u0439 \u0441\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u0432\u0441\u0435\u0433\u043e \u043e\u043a\u0440\u0443\u0436\u0435\u043d\u0438\u044f:<\/p>\n<pre><code>Record Environment :=     { env_chain :> Chain;       env_contracts : Address -> option WeakContract;       env_contract_states : Address -> option SerializedValue; }.<\/code><\/pre>\n<p>\u0421\u043e\u0441\u0442\u043e\u044f\u043d\u0438\u0435 \u043e\u043a\u0440\u0443\u0436\u0435\u043d\u0438\u044f \u0438\u0437\u043c\u0435\u043d\u044f\u0435\u0442\u0441\u044f \u0432 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0439, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u044e\u0442\u0441\u044f \u0432 ConCert \u0442\u0438\u043f\u043e\u043c <code>Action<\/code>:<\/p>\n<pre><code>Record Action := { act_from : Address; act_body : ActionBody; }.<\/code><\/pre>\n<p>\u041a\u043e\u0433\u0434\u0430 <code>receive<\/code> \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u043d\u043e\u0432\u044b\u0439 \u0441\u043f\u0438\u0441\u043e\u043a \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0439, \u0441\u0440\u0435\u0434\u0430 \u0438\u0441\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0434\u043e\u043b\u0436\u043d\u0430 \u0431\u0443\u0434\u0435\u0442 \u043e\u0446\u0435\u043d\u0438\u0442\u044c \u0438\u0445 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442. \u042d\u0442\u0430 \u043e\u0446\u0435\u043d\u043a\u0430 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0435\u0442\u0441\u044f \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043e\u0442\u043d\u043e\u0448\u0435\u043d\u0438\u044f <code>ActionEvaluation<\/code> \u0432 Coq \u0441 \u0442\u0438\u043f\u043e\u043c <code>Environment -> Action-> Environment -> list Action -> Type<\/code>. \u041e\u043d\u043e \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u0432 \u0441\u0435\u0431\u0435 \u0442\u0440\u0435\u0431\u043e\u0432\u0430\u043d\u0438\u044f \u0434\u043b\u044f \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0442\u0440\u0430\u043d\u0437\u0430\u043a\u0446\u0438\u0438 \u0432 \u043e\u043a\u0440\u0443\u0436\u0435\u043d\u0438\u0438 \u0438 \u0435\u0435 \u043f\u043e\u0441\u043b\u0435\u0434\u0441\u0442\u0432\u0438\u044f.<\/p>\n<p>\u0418 <code>receive<\/code>, \u0438 <code>init<\/code> \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u043e\u0431\u044b\u0447\u043d\u044b\u043c\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u044f\u043c\u0438 Coq, \u0447\u0442\u043e \u0434\u0435\u043b\u0430\u0435\u0442 \u0438\u0445 \u0443\u0434\u043e\u0431\u043d\u044b\u043c\u0438 \u0434\u043b\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438. \u041e\u0434\u043d\u0430\u043a\u043e \u043f\u0440\u043e\u0441\u0442\u043e \u0440\u0430\u0441\u0441\u0443\u0436\u0434\u0435\u043d\u0438\u044f \u043e \u0444\u0443\u043d\u043a\u0446\u0438\u044f\u0445 \u043e\u0442\u0434\u0435\u043b\u044c\u043d\u043e\u0433\u043e \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0437\u0430\u0447\u0430\u0441\u0442\u0443\u044e \u043d\u0435\u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e, \u043f\u043e\u0441\u043a\u043e\u043b\u044c\u043a\u0443 \u043c\u043d\u043e\u0433\u0438\u0435 \u0440\u0430\u0437\u0432\u0435\u0440\u043d\u0443\u0442\u044b\u0435 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u044b \u043f\u043e\u0434\u0440\u0430\u0437\u0443\u043c\u0435\u0432\u0430\u044e\u0442 \u0432\u0437\u0430\u0438\u043c\u043e\u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0435 \u0441 \u0434\u0440\u0443\u0433\u0438\u043c\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430\u043c\u0438. \u041e\u0434\u0438\u043d \u0432\u044b\u0437\u043e\u0432 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <code>receive<\/code> \u043f\u043e\u0442\u0435\u043d\u0446\u0438\u0430\u043b\u044c\u043d\u043e \u043f\u043e\u0440\u043e\u0436\u0434\u0430\u0435\u0442 \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0432\u044b\u0437\u043e\u0432\u043e\u0432, \u0430 \u044d\u0442\u043e \u043c\u043e\u0436\u0435\u0442 \u0441\u043e\u0437\u0434\u0430\u0432\u0430\u0442\u044c \u0441\u043b\u043e\u0436\u043d\u044b\u0435 \u0433\u0440\u0430\u0444\u044b \u0432\u044b\u0437\u043e\u0432\u043e\u0432 \u043c\u0435\u0436\u0434\u0443 \u0440\u0430\u0437\u0432\u0435\u0440\u043d\u0443\u0442\u044b\u043c\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430\u043c\u0438. \u041f\u043e\u044d\u0442\u043e\u043c\u0443 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0442\u044c \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0432\u044b\u0437\u043e\u0432\u043e\u0432 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f. \u0422\u0440\u0430\u0441\u0441\u0430 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f <code>ChainTrace<\/code> \u2014 \u044d\u0442\u043e \u0440\u0435\u0444\u043b\u0435\u043a\u0441\u0438\u0432\u043d\u043e\u0435, \u0442\u0440\u0430\u043d\u0437\u0438\u0442\u0438\u0432\u043d\u043e\u0435 \u0437\u0430\u043c\u044b\u043a\u0430\u043d\u0438\u0435 \u043e\u0442\u043d\u043e\u0448\u0435\u043d\u0438\u044f ChainStep, \u043a\u043e\u0442\u043e\u0440\u043e\u0435, \u043f\u043e \u0441\u0443\u0442\u0438, \u043e\u0442\u0440\u0430\u0436\u0430\u0435\u0442 \u0434\u043e\u0431\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u0431\u043b\u043e\u043a\u0430 \u0432 \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d, \u0430 \u0432 ConCert \u0438\u043c\u0435\u0435\u0442 \u0442\u0438\u043f<code>ChainState -> ChainState -> Type<\/code>, \u0433\u0434\u0435:\u00a0<\/p>\n<pre><code>Record ChainState := { chain_state_env :> Environment;                        chain_state_queue : list Action; }<\/code><\/pre>\n<h3>\u0422\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432<\/h3>\n<p><abbr class=\"habraabbr\" title=\"PBT, \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\" data-title=\"&lt;p>\u0439\u0441\u0442\u0432&#187; data-title=&lt;p>PBT, \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432&lt;\/p>&#187; data-abbr=&#187;Property-based testing&#187;>Property-based testing<\/abbr> \u2014 \u044d\u0442\u043e \u0442\u0435\u0445\u043d\u0438\u043a\u0430 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f, \u0432 \u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u0434\u0430\u043d\u043d\u044b\u0435 \u0433\u0435\u043d\u0435\u0440\u0438\u0440\u0443\u044e\u0442\u0441\u044f \u043f\u0441\u0435\u0432\u0434\u043e\u0441\u043b\u0443\u0447\u0430\u0439\u043d\u044b\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c \u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u044e\u0442\u0441\u044f \u043d\u0430 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0438\u0435 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u043e\u043c\u0443 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u0443. \u0412 ConCert \u0438\u043d\u0442\u0435\u0433\u0440\u0438\u0440\u043e\u0432\u0430\u043d\u0430 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 PBT QuickChick, \u0431\u043b\u0430\u0433\u043e\u0434\u0430\u0440\u044f \u044d\u0442\u043e\u043c\u0443 \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u0438\u0432\u0430\u0435\u0442\u0441\u044f \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u043e\u0439 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\u043d\u043e\u0441\u0442\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432, \u0430 \u0442\u0430\u043a\u0436\u0435 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432 \u0442\u0440\u0430\u0441\u0441 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f. \u041e\u0431\u0437\u043e\u0440 \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a\u0430 \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u043f\u0440\u0438\u0432\u0435\u0434\u0435\u043d \u043d\u0430 \u0440\u0438\u0441\u0443\u043d\u043a\u0435.<\/p>\n<figure class=\"full-width\">\n<div><figcaption><a href=\"https:\/\/arxiv.org\/pdf\/2208.00758.pdf\">\u0420\u0438\u0441 2. \u0421\u0445\u0435\u043c\u0430 PBT ConCert<\/a>  <\/figcaption><\/div>\n<\/figure>\n<p>\u0415\u0441\u043b\u0438 \u043a\u0440\u0430\u0442\u043a\u043e, \u0444\u0440\u0435\u0439\u043c\u0432\u043e\u0440\u043a PBT \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c. \u041f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c \u043f\u0438\u0448\u0435\u0442 \u0433\u0435\u043d\u0435\u0440\u0430\u0442\u043e\u0440\u044b \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439 \u0442\u0435\u0441\u0442\u0438\u0440\u0443\u0435\u043c\u044b\u0445 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432. \u0413\u0435\u043d\u0435\u0440\u0430\u0442\u043e\u0440\u044b \u2014 \u044d\u0442\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u0438, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0441\u043e\u0437\u0434\u0430\u044e\u0442 \u043f\u0441\u0435\u0432\u0434\u043e\u0441\u043b\u0443\u0447\u0430\u0439\u043d\u044b\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0437\u0430\u0434\u0430\u043d\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430. \u0420\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u043d\u044b\u0435 \u0433\u0435\u043d\u0435\u0440\u0430\u0442\u043e\u0440\u044b \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044e\u0442\u0441\u044f \u0434\u043b\u044f \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0441\u043b\u0443\u0447\u0430\u0439\u043d\u044b\u0445 \u0442\u0440\u0430\u0441\u0441 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f \u0441 \u043f\u0441\u0435\u0432\u0434\u043e\u0441\u043b\u0443\u0447\u0430\u0439\u043d\u044b\u043c\u0438 \u0432\u044b\u0437\u043e\u0432\u0430\u043c\u0438 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432. \u041f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c \u0442\u0430\u043a\u0436\u0435 \u043d\u0430\u0441\u0442\u0440\u0430\u0438\u0432\u0430\u0435\u0442 \u043d\u0430\u0447\u0430\u043b\u044c\u043d\u0443\u044e \u043a\u043e\u043d\u0444\u0438\u0433\u0443\u0440\u0430\u0446\u0438\u044e \u0431\u043b\u043e\u043a\u0447\u0435\u0439\u043d\u0430, \u0441\u043e\u0441\u0442\u043e\u044f\u0449\u0443\u044e \u0438\u0437 \u0431\u0430\u043b\u0430\u043d\u0441\u043e\u0432 \u0430\u0434\u0440\u0435\u0441\u043e\u0432 \u0438 \u0440\u0430\u0437\u0432\u0435\u0440\u043d\u0443\u0442\u044b\u0445 \u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u043e\u0432.\u00a0<\/p>\n<p>\u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043f\u0440\u0438\u043c\u0435\u0440 \u0441\u043c\u0430\u0440\u0442-\u043a\u043e\u043d\u0442\u0440\u0430\u043a\u0442\u0430 \u0442\u043e\u043a\u0435\u043d\u0430 \u0441 \u0442\u0438\u043f\u043e\u043c \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u044b\u0445 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439:<\/p>\n<pre><code>Inductive Msg :=     transfer of (address * address * nat)   | approve of (address * address * nat).<\/code><\/pre>\n<p>\u0422\u043e \u0435\u0441\u0442\u044c \u0443 \u043d\u0435\u0433\u043e \u0435\u0441\u0442\u044c \u0434\u0432\u0435 \u0442\u043e\u0447\u043a\u0438 \u0432\u0445\u043e\u0434\u0430: \u043e\u0434\u043d\u0430 \u0434\u043b\u044f \u043f\u0435\u0440\u0435\u0434\u0430\u0447\u0438 \u0442\u043e\u043a\u0435\u043d\u043e\u0432 \u043c\u0435\u0436\u0434\u0443 \u0434\u0432\u0443\u043c\u044f \u0437\u0430\u0434\u0430\u043d\u043d\u044b\u043c\u0438 \u0430\u0434\u0440\u0435\u0441\u0430\u043c\u0438 \u0438 \u043e\u0434\u043d\u0430 <\/p>\n<\/div>\n<\/div>\n<\/div>\n<\/div>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"class_list":["post-372559","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/372559","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=372559"}],"version-history":[{"count":0,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/372559\/revisions"}],"wp:attachment":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=372559"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=372559"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=372559"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}