Изучение необходимости поиска семантических свойств предметной области, который возникает в связи с тем, что простой информации, извлеченной из текста алгоритма или программного обеспечения, как правило, недостаточно для обоснования их правильности.
Аннотация к работе
РАЗРАБОТКА И ОБОСНОВАНИЕ АЛГОРИТМОВ НА ОСНОВЕ СЕМАНТИЧЕСКИХ СВОЙСТВ Приводятся примеры разработки и обоснования алгоритмов на основе использования свойств предметной области. Эти свойства формулируются в виде семантических соотношений, характеризующих предметную область разрабатываемого алгоритма.Использование АТД позволяет разрабатывать алгоритмы и программы, базируясь на свойствах их операций и предикатов с последующим выбором наиболее эффективного способа их реализации. Из приведенной на рисунке схемы следует, что процесс разработки состоит из двух этапов: на первом строится алгоритм, а на втором - программа по этому алгоритму. Под семантическим свойством предметной области D = D ?D2 ???Dn будем понимать соотношение R(x, y,?,z) ? D, которое выполняется (возможно при некоторых ограничениях) для любых значений переменных x, y,?,z из области D (удовлетворяющих этим ограничениям) и которое согласовано с семантикой реализации АТД, с помощью которых представлено это свойство. Тогда топологическая сортировка сводится к линейному упорядочению вершин ациклического орграфа таким образом: если существует дуга из вершины v в вершину u в графе G , то в искомом линейно упорядоченном списке вершин орграфа вершина v предшествует вершине u . Для доказательства правильности алгоритма необходимо показать: а) что когда v ?1 u (т. е. из вершины v к вершине u существует путь в графе G ), то в множестве V?? вершина v предшествует вершине u ;Отметим, что необходимость поиска семантических свойств предметной области возникает в связи с тем, что информации, извлеченной из текста алгоритма или программы (например, в виде инвариантных соотношений), как правило, недостаточно для обоснования их правильности. Многие свойства, особенно семантического характера, явно не фигурируют в алгоритме и тем более в программе его реализации. Поиск семантических свойств сопряжен с трудностями как теоретического, так и практического характера и его успех зависит прежде всего от индивидуальных качеств разработчика программного обеспечения. В этом, наверное, и состоит главная сложность проблемы построения качественного и надежного програмного обеспечения. Abstract Interpretation Based Formal Methods and Future Challenges. http://www.di.ens.fr/ cousot/.