Система доказательного программирования
Описаны методы доказательства правильности программ в системе инсерционного моделирования, ее архитектура и функциональные возможности, даны основные сведения о нем. Рассмотрена инсерционная машина метода Флойда, методы проверки выполнимости формул и их использование при доказательстве правильности...
Gespeichert in:
| Veröffentlicht in: | Управляющие системы и машины |
|---|---|
| Datum: | 2012 |
| Hauptverfasser: | , , |
| Format: | Artikel |
| Sprache: | Russian |
| Veröffentlicht: |
Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
2012
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/83110 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Система доказательного программирования / А.А. Летичевский (мл.), М.К. Мороховец, В.С. Песчаненко // Управляющие системы и машины. — 2012. — № 6. — С. 64-71. — Бібліогр.: 18 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-83110 |
|---|---|
| record_format |
dspace |
| spelling |
Летичевский, А.А. (мл.) Мороховец, М.К. Песчаненко, В.С. 2015-06-14T19:22:49Z 2015-06-14T19:22:49Z 2012 Система доказательного программирования / А.А. Летичевский (мл.), М.К. Мороховец, В.С. Песчаненко // Управляющие системы и машины. — 2012. — № 6. — С. 64-71. — Бібліогр.: 18 назв. — рос. 0130-5395 https://nasplib.isofts.kiev.ua/handle/123456789/83110 519.686.2 Описаны методы доказательства правильности программ в системе инсерционного моделирования, ее архитектура и функциональные возможности, даны основные сведения о нем. Рассмотрена инсерционная машина метода Флойда, методы проверки выполнимости формул и их использование при доказательстве правильности программ. The methods are described of proving the programs correctness within the Insertion Modeling System. The architecture of the system and its functional possibilities are described, the basic notions of insertion modeling are presented. An insertion machine for Floyd’s method is presented, the methods of the satisfiability checking of the formulae, and their usage for proving the program correctness are described. Описано методи доведення правильності програм у системі інсерційного моделювання, її архітектура та функціональні можливості, подано основні відомості про нього. Розглянуто інсерційну машину методу Флойда, методи перевірки виконуваності формул та їх використання у доведенні правильності програм. Работа выполнена при поддержке ДФФД в рамках проекта Ф40.1/004. ru Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України Управляющие системы и машины Дедуктивные методы Система доказательного программирования System for Provable Programming Система доказового програмування Article published earlier |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Система доказательного программирования |
| spellingShingle |
Система доказательного программирования Летичевский, А.А. (мл.) Мороховец, М.К. Песчаненко, В.С. Дедуктивные методы |
| title_short |
Система доказательного программирования |
| title_full |
Система доказательного программирования |
| title_fullStr |
Система доказательного программирования |
| title_full_unstemmed |
Система доказательного программирования |
| title_sort |
система доказательного программирования |
| author |
Летичевский, А.А. (мл.) Мороховец, М.К. Песчаненко, В.С. |
| author_facet |
Летичевский, А.А. (мл.) Мороховец, М.К. Песчаненко, В.С. |
| topic |
Дедуктивные методы |
| topic_facet |
Дедуктивные методы |
| publishDate |
2012 |
| language |
Russian |
| container_title |
Управляющие системы и машины |
| publisher |
Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України |
| format |
Article |
| title_alt |
System for Provable Programming Система доказового програмування |
| description |
Описаны методы доказательства правильности программ в системе инсерционного моделирования, ее архитектура и функциональные возможности, даны основные сведения о нем. Рассмотрена инсерционная машина метода Флойда, методы проверки выполнимости формул и их использование при доказательстве правильности программ.
The methods are described of proving the programs correctness within the Insertion Modeling System. The architecture of the system and its functional possibilities are described, the basic notions of insertion modeling are presented. An insertion machine for Floyd’s method is presented, the methods of the satisfiability checking of the formulae, and their usage for proving the program correctness are described.
Описано методи доведення правильності програм у системі інсерційного моделювання, її архітектура та функціональні можливості, подано основні відомості про нього. Розглянуто інсерційну машину методу Флойда, методи перевірки виконуваності формул та їх використання у доведенні правильності програм.
|
| issn |
0130-5395 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/83110 |
| citation_txt |
Система доказательного программирования / А.А. Летичевский (мл.), М.К. Мороховец, В.С. Песчаненко // Управляющие системы и машины. — 2012. — № 6. — С. 64-71. — Бібліогр.: 18 назв. — рос. |
| work_keys_str_mv |
AT letičevskiiaaml sistemadokazatelʹnogoprogrammirovaniâ AT morohovecmk sistemadokazatelʹnogoprogrammirovaniâ AT pesčanenkovs sistemadokazatelʹnogoprogrammirovaniâ AT letičevskiiaaml systemforprovableprogramming AT morohovecmk systemforprovableprogramming AT pesčanenkovs systemforprovableprogramming AT letičevskiiaaml sistemadokazovogoprogramuvannâ AT morohovecmk sistemadokazovogoprogramuvannâ AT pesčanenkovs sistemadokazovogoprogramuvannâ |
| first_indexed |
2025-12-07T15:38:22Z |
| last_indexed |
2025-12-07T15:38:22Z |
| _version_ |
1850864464192077824 |